- 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
Formula-V (A foundational platform for fully-formally-verified systems design)
Auftragnehmer: Barkhausen Institut (Dresden), TU Dresden, TU Berlin, Kernkonzept GmbH, Ferrous Systems GmbH, Fraunhofer AISEC
Projektlaufzeit: 12/2024-12/2028
Das Ziel von Formula-V ist ein vollständig formal verifiziertes IT-System auf Grundlage eines Unikernel-Betriebssystems. Software und Hardware sollen dabei in einem durchgängigen Beweissystem verifiziert werden. Die Verifikation des Unikernels umfasst das Dateisystem und den Netzwerkstack mit den jeweiligen Treibern. Das System soll auf einem RISC-V-Prozessor laufen. Die Spezifikation des Prozessors und der Unikernel sollen nach der Überführung der Implementierungen in den Beweisassistenten Rocq (ehemals Coq) lückenlos formal verifiziert werden. Außerdem werden Gegenmaßnahmen gegen Seitenkanal- und transient-execution-Attacken eingeführt. Um eine einfachere Unikernel-Entwicklung zu ermöglichen, liegt ein besonderer Fokus auf Tools, die eine größere Automatisierung der Verifikation ermöglichen.
PROTECT (Proving Next-Generation Secure Systems)
Auftragnehmer: DFKI (Bremen), RWTH, Cryspen SARL, Lubis EDA GmbH, Gesellschaft für Informatik, RPTU Kaiserslautern, Universität zu Lübeck
Projektlaufzeit: 12/2024-12/2028
Projektwebseiten: DFKI, Gesellschaft für Informatik
Der Schwerpunkt von PROTECT liegt auf einer kompositionalen “Bottom-up”-Strategie, bei der verschiedene Ansätze zu einem einheitlichen System kombiniert werden sollen. Das Referenzsystem des Projekts soll auf einem RISC-V-Prozessor basieren. Dieser wird mithilfe von virtuellen Prototypen modelliert, um frühzeitig ein Ko-Design von sicherer Hardware und darauf abgestimmter sicherer Software zu ermöglichen. Neue formale Verifikationstechniken für die Hardware und die Hardware-Software-Schnittstelle sollen transient-execution- und Seitenkanal-Angriffe verhindern. Zuerst soll ein Referenzsystem mit geringer Komplexität (RISC-V 32 Bit, ohne Betriebssystem) zu einem mittelgroßen System weiterentwickelt werden (RISC-V 32 Bit, Unikernel- oder Micro-Kernel-basiertes Betriebssystem mit Crypto-Modul). Bestenfalls werden die Ansätze (zumindest teilweise) die Verifikation eines komplexen Systems ermöglichen (RISC-V 64 Bit, Multi-Core, Betriebssystem der Linux-Klasse). Ein wichtiger Teil dieses Projekts ist das aktive Community-Building, bei dem ein intensiver Austausch von Forschenden, Hardware- und Softwareentwicklern sowie Anwendern aus der Industrie etabliert werden soll.
Dynamism, performance, and proof for complex cyber-physical systems
Auftragnehmer: Kry10 (Wellington, NZ), Proofcraft (Sydney)
Projektlaufzeit: 08/2024-08/2028
Das Projekt entwickelt ein dynamisch aktualisierbares Mehrkernsystem, das mithilfe von formaler Verifikation hohe Sicherheitsstandards erfüllt. Ziel des Projekts ist die Entwicklung einer Referenzplattform auf der Grundlage des seL4-Mikrokernels, einschließlich eines Software Development Kits, einer unterstützten Hardwarekonfiguration und eines Demonstrators zur Überführung in Industrieanwendungen. Zusätzlich sollen zur Unterstützung der Entwicklung und Bewertung kritischer cyber-physischer Systemdesigns verschiedene Tools und Techniken entwickelt werden.
Clash Formal (Provably Secure and Safe System Design with Clash)
Auftragnehmer: QBayLogic (Enschede, NL)
Projektlaufzeit: 07/2024-07/2028
Projektwebseite: QBayLogic
Clash Formal setzt auf die funktionale Hardware-Beschreibungssprache Clash in Kombination mit der funktionalen Programmiersprache Haskell. Damit soll die Erstellung von sicherer correct-by-design Hardware und Software, sowie den Schnittstellen zwischen Hardware und Software in einer einzigen Beschreibungssprache und Entwicklungsumgebung gelingen. Ein Ziel ist die direkte Integration von formalen Verifikations-Frameworks in die Compiler von Clash und Haskell. Dazu zählen z.B. Schnittstellen für Beweisassistenten wie Rocq, Agda oder Isabelle sowie die Sprache SAIL, zur Beschreibung der Semantiken von Befehlssatzarchitekturen. Auf Basis der Ergebnisse soll ein Security-Token und ein Smartcard-System mit formal verifizierten Sicherheitseigenschaften entwickelt werden.
PISTIs-V (Protected Integrity and Security of Transmissions Integrating seL4 and RISC-V)
Auftragnehmer: PlanV GmbH (München), UNSW Sydney, Universität Göteborg
Projektlaufzeit: 09/2024-09/2027
Projektwebseite: PISTIs-V
Im Projekt PISTIs-V wird ein eingebettetes Referenzsystem entwickelt, das Ende-zu-Ende-Sicherheitsnachweise erbringt. Es soll den Ausgangspunkt für Industrie-Anwendungen darstellen. Grundlage ist das neue Betriebssystem LionsOS, das auf dem formal verifizierten Mikrokern seL4 aufbaut. Das Projekt soll einen Ansatz zur Entwicklung von Treibern für Lions-OS liefern. Die Treiber werden gegenüber der verifizierten Implementierung der Gerätehardware verifiziert. Weitere kritische Hardware-Komponenten sollen formal verifiziert werden. Darunter z.B. fence.t, ein Hardware-Mechanismus, der einen vollständigen Zeitschutz von RISC-V-Prozessoren gegen Seitenkanalattacken ermöglicht. Die verifizierten Eigenschaften von LionsOS beinhalten den Beweis, dass nicht vertrauenswürdige Komponenten eingeschränkt werden. Dadurch werden keine geschützten Informationen preisgegeben, auch nicht durch mikroarchitektonische Timing-Kanäle. Weiterhin sind Echtzeitsysteme mit gemischter Kritikalität planbar. Ein Hauptziel von PISTIs-V ist die einfache Re-Verifikation neuer Treiber und Policy- Module, die für die Portierung des Systems auf neue Plattformen oder die Anpassung an neue Use-Cases erforderlich sind. Dies wird durch den Einsatz von Push-Button-Verifikationstechniken ermöglicht.
Vorstudien
Grundlage der ÖvIT-Ausschreibung waren die ÖvIT-Vorstudien, die in fünf Losen die Forschungsbedarfe im Themenfeld untersucht haben.
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.