Vorstudien zum Projekt ÖvIT

Ökosystem vertrauenswürdige IT: Beweisbare Cybersicherheit (ÖvIT)

Das Forschungsprojekt ÖvIT hat das Ziel, die technologische Souveränität der Bundesrepublik Deutschland zu stärken. Dafür soll eine leistungsfähige Alternative zu bestehender IT-Hardware und Software geschaffen werden, deren Cybersicherheit sich mit Hilfe sogenannter formaler Methoden beweisen lässt. Denn das Vertrauen in die korrekte und sichere Ausführung in einer zugesicherten Spezifikation ist ein wesentliches Merkmal vertrauenswürdiger IT-Systeme, insbesondere im Kontext von Anwendungen und Nutzungsszenarien der Inneren und Äußeren Sicherheit.Formale Methoden sind mathematische und logische Techniken, mit denen sich beweisen lässt, dass in Software oder Hardware bestimmte Sicherheitslücken nicht vorkommen. Leider ist es sehr anspruchsvoll und zeitintensiv, Cybersicherheits-Anforderungen so aufzuschreiben, dass diese Beweistechniken anwendbar werden. Moderne Systeme sind zudem so umfangreich, dass formale Methoden derzeit selbst mit maschineller Unterstützung einen sehr hohen Aufwand verursachen und oft in der Praxis nicht anwendbar sind.Das Forschungsprojekt ÖvIT soll vor diesem Hintergrund folgende Forschungsfragen klären:

• Lässt sich ein ganzheitliches Verifikationsverfahren für ein beweisbar sicheres IT-System – bestehend aus Hardware und Software – entwickeln, dessen garantierte Sicherheitseigenschaften sich zur Entwicklung hochsicherer komplexer Systeme nutzen lassen?
• Lässt sich das Verfahren so praktikabel umsetzen, dass Hardware- und Software-Entwicklerinnen und ‑Entwickler es leicht erlernen können, sodass es breit eingesetzt werden kann?
• Wie lässt sich eine Community von Forscherinnen und Forschern und Anwenderinnen und Anwendern aufbauen, um schließlich ein Ökosystem auf Anwendungsebene zu etablieren, das IT-Systemen mit beweisbarer Cybersicherheit für Anwendungen im Bereich Innerer und Äußerer Sicherheit bereitstellt?

Um dieses Forschungsprojekt auszugestalten, hat die Cyberagentur Vorstudien beauftragt, die den Stand der Technik darstellen und Forschungsprioritäten empfehlen. Die Ergebnisse stellen wir hier zur Verfügung. Die Vorstudien wurden in 5 Lose aufgeteilt; Berichtssprache für Lose 1-4 ist Englisch, für Los 5 Deutsch.

Zu den Vorstudien

• ÖvIT-Vorstudie Los 1 Software-Verifikation:
  • Formal Verification of Complex Software Systems – A Study [abstract, html]
• ÖvIT-Vorstudie Los 2 Hardware-Verifikation:
  • Formal Verification of Hardware – A Study [abstract, html]
• ÖvIT-Vorstudie Los 3 Verifikation von Software-Hardware-Schnittstellen:
  • Formal Verification of Hardware-Software-Interfaces – A Study [abstract, html]
• ÖvIT-Vorstudie Los 4 Formale Sicherheitsgarantien für Hardware-Lieferketten:
  • Formal Security Guarantees for Trustworthy Hardware Supply Chains – A Study [abstract, html]
• ÖvIT-Vorstudie Los 5: Community- und Ökosystem-Aufbau zu formaler Verifikation von Basis-IT:
  • Vorstudie Community- und Ökosystem-Aufbau zu formaler Verifikation von Basis-IT [abstract, html]

Kontakt

oevit@cyberagentur.de / evit@cyberagentur.de