Cyber-physikalische Systeme kombinieren elektronische und mechanische Elemente mit Software. Sie kommen in technischen Systemen jeglicher Art – Autos, Zügen oder Flugzeugen bis hin zu Smart-Home-Systemen – zum Einsatz. Die Entwicklung dieser Systeme ist hochkomplex, da es viele Abhängigkeiten zwischen den einzelnen Komponenten gibt. Der Sonderforschungsbereich „Konsistenz in der sichtenbasierten Entwicklung Cyber-Physikalischer Systeme“ fokussiert sich auf die Konsistenz der Integration verschiedener disziplinärer Sichtweisen bei der Entwicklung von Cyber-Physikalischen Systemen. Damit adressiert er die zentrale Herausforderung der steigenden Komplexität beim Entwurf und der Entwicklung technischer Systeme.

SFB 1608: CONVIDE – Konsistenz in der sichtenbasierten Entwicklung Cyber-Physikalischer Systeme

HGF-Pilotprogramm Kern-Informatik (KiKIT) ist der Inkubator eines Forschungsprojektes in der Helmholtz-Gemeinschaft mit dem Ziel der Verstetigung ab 2026. KiKIT umfasst dabei drei Teilbereiche: Algorithmen- und Software-Engineering; Data Science, KI, und Mensch-Computer-Interaktion, sowie Hardware und Netzwerke.

Die Gruppe von Prof. Beckert beteiligt sich mit zwei Projekten: Algorithm-Refinement und Integration von KeY und KeYmaeraX (https://keymaerax.org) an KiKIT.

KiKIT

Intelligente Infrastrukturen, Cloud Computing und öffentliche Sicherheit stellen große Herausforderungen an die IT-Sicherheit der Zukunft. Zusätzlich zum klassischen Schutz der Peripherie muss mit Bedrohungen von innen umgegangen werden. Es genügt nicht mehr, die Sicherheit von Teilsystemen zu betrachten. Dabei bedarf es disziplinenübergreifender Methoden. Das Kompetenzzentrum für Angewandte Sicherheits-TEchnoLogie (KASTEL) bündelt die Kompetenzen verschiedener Teildisziplinen der IT-Sicherheit und der Anwender.

KASTEL Projekt

Das KIT bietet derzeit die Möglichkeit, Online-Abstimmungen durchzuführen. Dabei sind offene Abstimmungen bspw. im Rahmen von Video-Sitzungen der Gremien recht einfach durchzuführen. Geheime Online-Abstimmungen und -Wahlen stellen aber eine ungleich größere Herausforderung dar – wegen den gegensätzlichen Anforderungen, die sich aus dem Wahlgeheimnis auf der einen Seite und dem Erfordernis nachvollziehbarer Korrektheit und Sicherheit der Wahl auf der anderen Seite ergeben.

Ziel dieses Projektes ist die Konzeption und die prototypische Umsetzung eines Online-Wahlsystems für Ende-zu-Ende-verifizierbare, geheime Wahlen am KIT. Der Prototyp wird zu einer KIT-weiten Testabstimmung eingesetzt. Ziel ist es insbesondere nicht, die Entscheidungshoheit zu verändern, sondern komplexe technische Sachverhalte zu erklären. Zum einen entwickelt sich ohnehin eine Dynamik in Richtung Online-Wahlen an Hochschulen, derzeit in der Regel aber als Blackbox-System, bei denen starke Sicherheitsannahmen getroffen werden.

Projekt für E2E-Wahlen am KIT

KeY wurde erfolgreich in verschiedenen Forschungsprojekten verwendet, die nicht vom KeY-Team initiiert wurden. Das zeigt einerseits das Potential von KeY als Forschungswerkzeug. Auf der anderen Seite wurden allerdings die meisten dieser Projekte in enger Zusammenarbeit mit Mitgliedern der Kern- KeY-Teams durchgeführt.

Ziel dieses Projekts is es, KeY so zugänglich und robust zu machen, dass es erfolgreich für die Forschung außerhalb des KeY-Teams eingesetzt werden kann. Wir stellen KeY als Plattform für Experimente im Bereich formaler Methoden sowie zum Testen neuer Ansätze und Methoden, die Zuverlässigkeit von Forschungssoftware zu analysieren und sicherzustellen, zur Verfügung.

Das Projekt wird von der DFG gefördert.

Online-Wahlsysteme werden seit Beginn der Pandemie immer häufiger bei geheimen Wahlen und Abstimmungen diskutiert und auch eingesetzt. Einerseits stellt sich bei den eingesetzten Systemen die Frage nach der technisch-organisatorischen Vertrauenswürdigkeit (d. h. wie die Sicherheit dieser Systeme im Zuge einer Evaluierung ihrer Eigenschaften bewertet wird) und anderseits die Frage, wodurch das Vertrauen der Wähler:innen in diese Systeme (und letztendlich das Ergebnis) beeinflusst wird und welche Rolle dabei die Erklärbarkeit spielt (d. h. inwieweit Wähler:innen die Funktionalität und/oder Eigenschaften verstehen).

Die Ziele des Projektes sind eine Vernetzung der beiden Topics Engineering Secure Systems und Knowledge for Action im Helmholtz-Programm Engineering Digital Futures (innerhalb des Forschungsbereichs Information) sowie ein Anschub für besondere Forschungsfragen im Kontext technisch-organisatorischer Vertrauenswürdigkeit und Einflüssen auf Vertrauen in Online-Wahl-Systeme, insbesondere hinsichtlich der Rolle von Erklärbarkeit.

Vernetzungsprojekt für erklärbare Online-Wahlen

Ziel des Projekts „SofDCar“ ist es, die digitale Nachhaltigkeit im Automotive-Bereich zu erhöhen. Dies soll unter Anderem durch Verbesserung der Regeln, Prozesse und Infrastruktur im Bereich von Software-Updates und -Upgrades umgesetzt werden. Dabei sollen die Updates kontrollierbarer werden mit einem starken Fokus auf Safety und Security. Dies ermöglicht, dass neue Funktionen in und um das Fahrzeug künftig schneller entwickelt werden können und sicher zu den Fahrerinnen und Fahrern kommen.

SofDCar Projekt

Das KeY-System ist ein Werkzeug zur formalen Softwareentwicklung, das darauf ausgerichtet ist, Entwurf, Implementierung, formale Spezifikation und formale Verifikation objekt-orientierter Software möglichst nahtlos miteinander zu vereinen. Im Zentrum des Systems steht ein neuartiger Theorembeweiser für dynamische Logik erster Ordnung für Java mit einer anwendungsfreundlichen Oberfläche.

Das Projekt begann im November 1998 an der Universität Karlsruhe. Inzwischen ist es ein gemeinsames Projekt des KIT, Chalmers University of Technology in Göteborg und der TU Darmstadt und wird von der DFG gefördert.

KeY Projekt

Die rechenbetonte Sozialwahltheorie (Computational Social Choice) ist ein sich rapide weiterentwickelnder Forschungszweig, der sich mit dem Design und der Analyse von Methoden der kollektiven Entscheidungsfindung beschäftigt. Er kombiniert Methoden der Informatik mit Erkenntnissen der Wirtschaftstheorie. Die COST Action IC1205 zu Computational Social Choice ist ein europäisches Forschungsnetzwerk, das aufgebaut wurde, um eine gemeinsame Plattform zur Forschung in diesem Feld europaübergreifend und darüber hinaus herzustellen.

Innerhalb dieses Projekts konzentrieren wir uns auf die Spezifikation und Verifikation von Wahlverfahren. Ein Wahlverfahren, als eine Methode individuelle Präferenzen zu einer aggregierten Wahlentscheidung zu kombinieren, ist Teil des grundsätzlichen demokratischen Verfahrens. Es ist also unerlässlich, dass Wahlverfahren wie vorgesehen funktionieren. Das Ziel des Projektes ist die Entwicklung formaler Verifikationstechniken, die es erlauben, Eigenschaften von Wahlverfahren ohne den riesigen Overhead einer für eine voll-funktionale Verifikation notwendigen Nutzer-Interaktion zu überprüfen. Die resultierende Methodik könnte dann in einem iterativen Design- und Implementierungsprozess neuer Wahlverfahren eingesetzt werden.

COST Action

Das Hauptziel des Projekts Lehre^Forschung-PLUS ist die Verbesserung der Studienbedingungen und kontinuierliche Steigerung der Lehrqualität durch eine flächendeckende Weiterentwicklung der Studiengänge.

Unser Teilprojekt umfasst hierbei drei wesentliche Maßnahmen, die alle das Ziel verfolgen, projekt- und forschungsorientierte, sowie interdisziplinäre Lehre in den Informatik-Studiengängen umzusetzen und zu stärken.

Diese beinhalten die Weiterentwicklung und Verbesserung des projekt- und forschungsorientierten Master-Moduls "Praxis der Forschung", des projektorientierten Bachelor-Moduls "Praxis der Softwareentwicklung", sowie die Einführung des interdisziplinären und forschungsorientierten Studienprofils "Internet und Gesellschaft" [PDF].

Teilprojekt "Lehre^Forschung-PLUS – Problemorientierte, forschungsorientierte und interdisziplinäre Lehre in der Informatik"

Um als Erwachsene die Herausforderungen der Digitalisierung zu bewältigen, brauchen Schülerinnen und Schüler eine breite Grundbildung in Informatik. Im Open-Source-Lehrsoftware-Labor sollen Studentinnen und Studenten praktische Erfahrung in der Entwicklung von Open-Source-Software sammeln und gleichzeitig Materialien für den Informatikunterricht entwickeln.

OSLSL Projekt

Die Vision dieses Projektes besteht darin, die Technologie voranzubringen, sodass Methodiken der Regression Verification verfügbar sind, die routinemäßig verwendet werden, Korrektheit im Evolutionsprozess langlebiger verlässlicher Systeme, die eine regelmäßige Re-Validierung erfordern, zu garantieren. Das Ziel von Regression Verification ist es, formal zu beweisen, dass die Korrektheit von Software während ihres Evolutionsprozesses erhalten bleibt, Änderungen den gewünschten Effekt haben, und keine neuen Bugs eingeführt werden.

Regression Verification umgeht den Haupt-Flaschenhals zur routinemäßigen praktischen Verwendung formaler Verifikation, nämlich die Notwendigkeit voll-funktionale Spezifikationen zu schreiben (was einen enormen Aufwand darstellt). Außerdem, gegeben zwei gleichermaßen komplexe aber ähnliche Programm-Versionen oder -Varianten, hängt der Aufwand, den Zusammenhang zwischen ihnen zu verifizieren, hauptsächlich vom Unterschied zwischen den Programmen und nicht von ihrer gesamten Größe und Komplexität ab.

IMPROVE-APS Projekt

Ziel dieses Projekts ist es, Wege für die Spezifikation und formale Verifikation von Smart Contracts zu schaffen. Aufbauend auf existierenden Technologien und Werkzeugen der formalen Verifikation soll eine Basis geschaffen werden, die es ermöglicht, funktionale Eigenschaften von Smart Contracts zu beschreiben und zu beweisen, sodass die Blockchain-/Smart-Contract-Technologie mit all ihren Vorteilen sicher und zuverlässig verwendet werden kann.

VeriSmart Projekt

In den letzten Jahren wurde ein deutlicher Fortschritt in der formalen Verifikation funktionaler Eigenschaften von Programmen erzielt. Gleichzeitig wurden zukunftsweisende Papiere veröffentlicht, die zeigen, dass es grundsätzlich möglich ist, Informationsfluss-Eigenschaften als Beweisverpflichtungen in Programm-Logik zu formulieren.

Das Gesamtziel des Projektes ist es diese Fortschritte — zusammen mit unseren eigenen Erfahrungen im Bereich der formalen Methoden für funktionale Eigenschaften — einzusetzen um Sicherheitseigenschaften zu spezifizieren und verifizieren.

DeduSec Projekt

Ziel des Software Campus Programmes ist es, die IT-Führungskräfte von morgen auszubilden. Die Projekte im Rahmen des Software Campus werden in Kooperation mit einem Forschungspartner und einem Industriepartner durchgeführt.

Das Projekt "Formale Informations-Fluss Analyse für komponenten-basierte Systeme" ist ein Projekt in Zusammenarbeit mit DHL IT-Services in Bonn.

Das Ziel ist es, Sicherheitsanalysen von komponenten-basierten Systemen während des System-Designs durchzuführen.

FIfAKS Projekt

Das Hauptziel des Projekts "Lehre hoch Forschung" ist die Verbesserung von Studienbedingungen und Lehrqualität, sowie die frühe Einbindung von Forschung in das Bachelor- und Master-Studienprogramm.

Des Weiteren ist es Ziel von „Lehre hoch Forschung“, künftig flächendeckend problemorientierte, forschungsorientierte Praktika und Projekte anzubieten, zu denen Studierende bereits in frühen Fachsemestern Zugang erhalten. Dabei geht es um einen breiten Einblick in relevante Aspekte der Grundlagen- und angewandten Forschung, genauso wie um überfachliche und transdisziplinäre Kompetenzen.

Unsere Arbeitsgruppe ist verantwortlich dafür, das Master-Modul "Praxis der Forschung" zu etablieren und zu koordinieren. Studierende lernen hier, ein Forschungsprojekt durchzuführen: angefangen vom Schreiben des Projektantrags, über die Durchführung des Projekts bis hin zur wissenschaftlichen Publikation der Ergebnisse. Die Projekte behandeln Themen aktueller Forschungsprojekte.

Teilprojekt "Lehre hoch Forschung – Problemorientierte Lehre"

Das Ziel dieses Projekts ist es, die Fortschritte in der deduktiven Programm-Verifikation zu nutzen, um Regression Verification zu ermöglichen. Mit der Hilfe von Regression Verification ist es möglich zu beweisen, dass  die Korrektheit von Software während ihres Evolutionsprozesses erhalten bleibt und keine neuen Bugs eingeführt werden. In diesem Projekt wird eine Regression Verification Methodik für Java entwickelt, die mächtig genug ist, um auf Beispiele aus der Praxis angewandt zu werden.

IMPROVE Projekt

In diesem Projekt werden Testverfahren und formale Methoden kombiniert um die Zuverlässigkeit von evolvierender Software zu gewährleisten. Mit dem Fokus auf evolvierende Software behandeln wir eine wichtige Phase im Lebenszyklus eines Softwaresystems und heben die inkrementelle Natur von Softwareänderungen hervor.

GIF Projekt

Ziel des Software Campus Programmes ist es, die IT-Führungskräfte von morgen auszubilden. Die Projekte im Rahmen des Software Campus werden in Kooperation mit einem Forschungspartner und einem Industriepartner durchgeführt.

Das Projekt "Usability von Software-Verifikationssystemen: Evaluierung und Verbesserung (USV)" ist ein Projekt in Zusammenarbeit mit der DATEV eG in Nürnberg. Das Ziel ist es, die Usability von Software-Verifikationssystemen zu evaluieren und auf der Basis der Evaluationsergebnisse Mechanismen zu entwickeln, um die Produktivität solcher Systeme zu verbessern.

USV Projekt

COST steht für "European Cooperation in the Field of Scientific and Technical Research". Es ist ein internationales Netzwerk zur Förderung der Zusammenarbeit europäischer Forscher als Basis. Mehr Information über COST befindet sich auf der allgemeinen COST Webseite. COST ist in "Actions" gegliedert. Das Ziel dieser Action ist, eine Verifikationstechnologie zu entwickeln, die weitreichend und stark genug ist, um die Zuverlässigkeit objekt-orientierter Software in industrieller Größe zu garantieren.

COST Action

Die Integration von deduktiver Programmverifikation und Bounded Model Checking (BMC) ist Gegenstand aktueller Arbeiten in Zusammenarbeit mit der Arbeitsgruppe von Dr. C. Sinz

Während die Verfahren zur deduktiven Verifikation neben der Anforderungsspezifikation eines Programms eine Vielzahl an Hilfen durch den Benutzer erfordert (Schleifeninvarianten, Spezifikationen von Hilfsfunctionen etc.), kommt BMC weitgehend ohne solchge Hilfen aus. Der Vorteil von deduktiver Verifikationis ist die höhere Präzision und die ausdrucksstärkeren Spezifikationsprachen.

Ein erstes Ziel der Arbeiten zur Kombination dieser Stärken ist es, BMC dazu einzusetzen, die iterative Interaktion zwischen Benutzer und deduktivem Verifikationswerkzeug zu verbessern: die Anbindung eines BMC-Werkzeugs soll es erlauben, Teile der Spezifikation eines Programms zu überprüfen bevor mit dem deduktiven Beweis begonnen wird.

Die korrekte Funktionalität von Systemen, wie sie beispielsweise im Automobilbau und Bereich der Sicherheitstechnik verwandt werden, werden formal-mathematisch überprüft.

Szenarios

• Anwendung im Automobil-Bereich
• Anwendung im Bereich Avionik
• Betriebssysteme, Hypervisors

Korrektheitsbeweis eines eingebetteten Betriebssystemkernels

In unserer Forschungsgruppe untersuchen wir schwerpunktmäßig die Spezifikation und Verifikation eines Microkernels mit Partitionierungsschicht, der in der Avionik industriell Einsatz findet.

Dabei verwenden wir das Verifikationstool VCC von Microsoft Research, um funktionale Eigenschaften des von der Firma SYSGO AG entwickelten Kernels PikeOS auf Implementierungsebene zu beweisen.

Verisoft Projekt