- Status: Projektphase
Hintergrund
IT-Systeme werden immer komplexer und dadurch anfälliger für sicherheitskritische Fehler. Viele der gefährlichsten Verwundbarkeiten von IT-Systemen sind auf wenige grundsätzliche Probleme zurückzuführen. Gängige Programmier- und Testmethoden können dabei viele Fehler in Hardware und Software vermeiden und finden, aber nicht alle.
Hier kommt die sogenannte formale Verifikation zum Einsatz: Das sind mathematisch-logische Methoden, mit denen sich beweisen lässt, dass ein IT-System vollständig frei von Sicherheitslücken ist, die zuvor definierte Sicherheitseigenschaften verletzen würden. Dafür werden die gewünschten Sicherheitseigenschaften formal festgehalten und Hardware und Software durchgängig so erstellt, dass die Eigenschaften mathematisch beweisbar erfüllt sind.
Die verwendeten Verfahren erfordern jedoch selbst von Informatikerinnen und Informatikern Spezialkenntnisse. Zudem sind die Verfahren für Hard- und Software der heutigen Komplexität nicht einfach oder automatisiert anzuwenden. Aktuell werden formale Methoden getrennt für Hardware und Software durchgeführt, und auch oft nur für einzelne Aspekte. Derzeit existiert kein ganzheitliches Verfahren, das eine korrekte Implementierung eines gesamten IT-Ökosystems nachweisen kann.
Zielstellung
Das Programm „Ökosystem vertrauenswürdige IT – beweisbare Cybersicherheit“ (ÖvIT) hat das Ziel, Technologien, Methoden und Tools für durchgängig formal verifizierte Software- und Hardwarekomponenten zu erforschen und zu entwickeln sowie ein Ökosystem von Entwicklerinnen und Entwicklern bei kommerziellen Anbieterinnen sowie von Nutzerinnen und Nutzern zu etablieren.
Dafür sollen Forscherinnen und Forscher die formale Verifikation für komplexere Systeme perspektivisch automatisiert einsetzbar machen. Die nötige Grundlagenforschung wird sich über einen Zeitraum von fünf bis zehn Jahren erstrecken und erst in einem Folgeprojekt abgeschlossen werden können.
Disruptive Risikoforschung
Der neue, durchgängige Ansatz soll größere Verbreitung finden, indem ein hohes Augenmerk auf einfacher zu nutzende, automatisierte und modulare Methoden und Werkzeuge gelegt wird. Ein wichtiger Aspekt ist das aktive Community-Building als Teil des Programms.
Das Forschungsprogramm ist aus wissenschaftlich-technologischer Perspektive höchst ambitioniert und wagnisbehaftet. Ein Projekt zur ganzheitlichen Verifikation komplexer Hard- und Software wurde bisher noch nicht erfolgreich realisiert.
Bei Erfolg können gängige Sicherheitslücken in vielen IT-Systemen bereits in der Entwicklung geschlossen werden, unabhängig davon, ob es sich bei der zu entwickelnden Software und Hardware um Standard-Bürosysteme oder um gehärtete IT für kritische Infrastrukturen oder für die nationale Sicherheit handelt.
Durch die Ergebnisse sollen Systeme mit beweisbarer Cybersicherheit in die breite Anwendung kommen, bei denen Sicherheitslücken gar nicht erst auftreten. Gleichzeitig soll der Ansatz „Cybersicherheit by Design“ stärker verbreitet werden. Das neue Wissen und das entstehende Ökosystem stärken die technologische Souveränität Deutschlands unmittelbar. Eine Beschaffungspolitik des Bundes, die einen solchen Ansatz als Anforderung formuliert, wäre flankierend ein starker Anreiz für IT-Anbieter, die Ergebnisse rasch in Anwendungen und Produkte zu transferieren.
Projekte
Los 1: Software-Verifikation
Auftragnehmer: FZI Forschungszentrum Informatik (Bernhard Beckert, Oliver Denninger, Jonas Klamroth, Max Scheerer, Jörg Henß)
Formale Software-Verifikationsmethoden können sowohl funktionale als auch nicht-funktionale Eigenschaften von Softwaresystemen nachweisen. Im Gegensatz zu Methoden wie Testen oder Debugging können sie garantieren, dass ein Softwaresystem kein Verhalten zeigt, das eine bestimmte Eigenschaft verletzt. Dadurch erreichen sie ein höheres Maß an Vertrauen. Die formale Verifikation von Software hat eine lange Geschichte in der Forschung, hat aber nie den Übergang zu einer breiten industriellen Anwendung geschafft. Diese Studie stellt den Stand der Forschung im Bereich der formalen Verifikation von Softwaresystemen dar und gibt Empfehlungen zur Verbesserung des Stands der Technik und der industriellen Anwendung.
Los 2: Hardware-Verifikation
Auftragnehmer: Rheinland-Pfälzische Technische Universität (Wolfgang Kunz, Dominik Stoffel, Johannes Müller, Mohammad R. Fadiheh)
Diese Studie gibt einen Überblick über Methoden der formalen Hardware-Verifikation im Hinblick auf relevante Sicherheitsziele für die grundlegenden IT-Elemente in der Hardware auf der Ebene der Mikroarchitektur. Aus einer Analyse gängiger Hardware-Schwächen und der relevanten Sicherheitsanforderungen für Mikroarchitekturen leiten wir die Ziele der sign-off Sicherheitsverifikation ab. Die Studie setzt diese Ziele in Beziehung zum Stand der Technik in der formalen Hardwareverifikation und beschreibt Stärken und Schwächen verschiedener Methoden und Methodiken. Dies führt zu Forschungsempfehlungen für die formale Sicherheitsverifikation von Hardware.
Los 3: Verifikation von Software-Hardware-Schnittstellen
Auftragnehmer: Deutsches Forschungszentrum für Künstliche Intelligenz GmbH (Christoph Lüth, Dieter Hutter, Milan Funck, Jan Zielasko)
Wir berichten über den Stand der Technik auf dem Gebiet der formalen Verifikation an der Schnittstelle zwischen Hardware und Software. Nach einer systematischen Durchsicht der Literatur der letzten zehn Jahre können wir eine Übersicht über die bestehenden verifizierten Systeme und Verifikationswerkzeuge geben. Die Verifikationsmethoden sind mit verifizierten Betriebssystemkernen, Compilern und Hardware ausgereift, aber es gibt immer noch erhebliche Lücken, insbesondere im Hinblick auf die Sicherheit; wir beschreiben diesen Forschungsbedarf und schlagen Richtungen für zukünftige Forschungsanstrengungen vor.
Los 4: Formale Sicherheitsgarantien für Hardware-Lieferketten
Auftragnehmer: Hensoldt Cyber GmbH (Dominik Sisejkovic, Lennart M. Reimann, Maja Malenko, Rainer Leupers)
Los 5: Community- und Ökosystem-Aufbau zu formaler Verifikation von Basis-IT
Auftragnehmer: Hensoldt Cyber GmbH, ESMT Berlin
Für die digitale technologische Souveränität der Bundesrepublik Deutschland ist es wichtig beweisbar sichere, leistungsfähige Alternativen zu bestehenden Basis-IT-Systemen von Drittanbietern zur Verfügung zu haben, um cyber-resiliente komplexe IT-Systeme in sicherheitskritischen Bereichen implementieren zu können. Die Entwicklung beweisbar sicherer Basis-IT und deren Anwendung muss durch ein entsprechendes zu etablierendes Ökosystem gefördert werden.
Auf dem Weg zu einem „Ökosystem vertrauenswürdiger IT“ mit formal verifizierter Hard- und Software ist der Aufbau und das Management einer geeigneten Entwickler- und Anwender-Community ein wichtiger Teilschritt. Die vorliegende Arbeit betrachtet dazu die Frage, wie sich eine entsprechende Community „Formale Verifikation von Basis-IT“ aufbauen und managen lässt. Dazu werden in einer Literaturrecherche die Erfolgsfaktoren und Misserfolgsfaktoren und der State of the Art des Aufbaus und Managements einer solchen Community betrachtet. Die gewonnen Erkenntnisse – ergänzt durch Aussagen einer Expertenbefragung und Betrachtungen von Fallstudien – dienen als Grundlage zur Erarbeitung eines möglichen Vorgehens zum Aufbau und Management einer Entwickler- und Anwendercommunity für „Formale Verifikation von Basis-IT“ (Roadmap) und einer Vision für ein zukünftiges daraus erwachsendes Ökosystem.
Wenn Sie Interesse an den Dokumenten zu den Vorstudien haben, wenden Sie sich bitte direkt an unsere Bibliothek: bibliothek@cyberagentur.de.