Ökosystem Vertrauenswürdige IT -
Beweisbare Cybersicherheit (ÖvIT)
IT-Systeme werden komplexer und anfälliger für sicherheitskritische Fehler. Viele Schwachstellen gehen auf wenige grundsätzliche Fehler zurück. Gängige Programmier- und Testmethoden können viele Fehler in Hardware und Software vermeiden und finden, aber nicht alle.
Hier setzt ÖvIT an: Wir verwenden mit formaler Verifikation mathematisch-logische Methoden. So können wir beweisen, dass ein IT-System vollständig frei von Sicherheitslücken ist, die zuvor definierte Sicherheitseigenschaften verletzen würden. Die gewünschten Sicherheitseigenschaften werden formal festgehalten und Hardware und Software durchgängig so erstellt, dass die Eigenschaften mathematisch beweisbar erfüllt sind. Formal verifizierte Software und Hardware sind im Rahmen der Spezifikationen beweisbar sicher und fehlerfrei. Damit sind sie besonders geeignet für den Einsatz in KRITIS-Systemen wie IKT, Mobilität oder militärischen Systemen.
ÖvIT will ein Netzwerk für Forschung, Anwendung und Entwicklung im Bereich formale Verifikation sein. Beim Aufbau einer wissenschaftlichen Community sollen Expertinnen und Experten sich mit Nachwuchsfachkräften und Interessenten aus der Industrie verbinden und die Anwendbarkeit formaler Verifikation zielgerichtet voranbringen. Wir laden Interessierte ein, Mitglied in unserem Ökosystem zu werden.
„Testing shows the presence, not the absence of bugs" (Dijkstra, 1969). Formale Verifikation setzt auf einer anderen Ebene als Tests an: Sie durchleuchtet den Source Code vollständig und auf der grundlegendsten Ebene. Damit werden Fehler und Schwachstellen von Beginn an ausgeschlossen.
Das Programm „Ökosystem vertrauenswürdige IT – beweisbare Cybersicherheit“ (ÖvIT) will Technologien, Methoden und Tools für durchgängig formal verifizierte Software- und Hardwarekomponenten erforschen und entwickeln. Formale Verifikation soll auch für komplexere Systeme automatisiert einsetzbar werden. Die dafür benötigte Grundlagenforschung erstreckt sich über die nächsten fünf bis zehn Jahre. Formale Verifikation setzt tiefgehendes Expertenwissen voraus, belohnt aber mit der Sicherheit von Bug-freier Software und Hardware: Zuverlässige Systeme schützen vor gefährlichen Fehlern und bösartigen Fremdzugriffen. Damit die Übertragung vom Prototyp zum Beispiel in die Steuerung kritischer Infrastruktur oder in Industrieanlagen gelingt, entsteht ein Ökosystem, in dem sich Entwickler*innen mit kommerziellen Anbieter*innen sowie Nutzer*innen in einem Ökosystem austauschen und vernetzen können.
Verifizierte Sicherheit: Durch formale Beweise lässt sich nachweisen, dass Code im Rahmen der Spezifikationen fehlerfrei ist. Dies ermöglicht sowohl Security als auch Safety für das Endprodukt. Schon der Vorgang, Spezifikationen und Annahmen explizit (formal) niederzuschreiben, bedeutet einen Sicherheitsgewinn.
Kosten senken: Verifizierte Software und Hardware muss nicht erneut gewartet werden. Prüfzyklen entfallen damit, ebenso Rückrufaktionen, wenn Bugs entdeckt werden. Der Arbeitsaufwand in diesem Feld wird gesenkt.
Fremdzugriff ausgeschlossen: Die Abwesenheit von Fehlern bezogen auf die Spezifikation bedeutet ein Fehlen von Schwachstellen, über die ein Angriff von außerhalb möglich wäre – vorausgesetzt natürlich, die Spezifikation erfasst die relevanten Angriffswege und Isolationseigenschaften. Die amerikanische DARPA beispielsweise hat zusammen mit Trustworthy Systems (seL4-Team der UNSW) eine fernbediente, im Praxisversuch unhackbare Drohne gebaut.
ÖvIT setzt sich aus fünf verschiedenen Projekten zusammen, jedes mit einem eigenen Schwerpunkt in formaler Verifikation. Abgedeckt sind Hardware- und Software-Verifikation, SoC-Design, Multikernelkonfiguration und die Weiterentwicklung von Verifikationstools.
Formula-V
Vollständige Verifikation eines IT-Systems mit Hardware und Software in einem durchgängigen Beweissystem. Das Alleinstellungsmerkmal von Formula-V ist ein lückenloser Beweis, welcher sich von der Hardware über das Betriebssystem bis hin zum Programm erstreckt.
PROTECT
Durchgängig verifiziertes IT-System mit Hardware und Software aus verifizierten Einzelbestandteilen und dem Nachweis von Sicherheitseigenschaften bei deren Zusammensetzung (kompositionaler „bottom-up“-Ansatz). Ein besonderes Augenmerk liegt auf dem Schutz gegen Seitenkanal-Attacken. Die Umsetzung erfolgt durch Virtual Prototyping und folgt dem Ansatz „Security by Design“.
Dyvercon
Erweiterung des zertifizierten seL4-Mikrokernels zu einer dynamisch updatebaren Multikernel-Konfiguration mit praxistauglicher Performance.
Clash Formal
Erweiterung von formalen Verifikationswerkzeugen in einer funktionalen Programmiersprache für Schaltkreisdesigns auf die durchgängige Verifikation gemeinsam mit der Software.
PISTIs-V
Erweiterung und durchgängige formale Verifikation des hochmodularen Betriebssystems LionsOS (einsetzbar in Automobilen, Flugzeugen, automatisierte Maschinen), Schutz vor Timing-Angriffen, verifiziertes Echtzeitverhalten und Isolation von nicht-vertrauenswürdigen Anwendungen im System.