Formula-V hat sich zum Ziel gesetzt, ein vollständig formal verifiziertes System zu schaffen, das den höchsten Standards in Bezug auf Sicherheit, Datenschutz und Vertrauenswürdigkeit entspricht. Um dies zu erreichen, integriert das Projekt sowohl Software- als auch Hardware-Verifikation und legt damit ein solides Fundament für die digitalen Technologien von morgen.

Die Projektmitglieder sind:

• Barkhausen Institut gGmbH
• Kernkonzept GmbH,
• Ferrous Systems GmbH,
• Fraunhofer AISEC,
• TU Dresden,
• TU Berlin

Formula-V verwendet formale Methoden, um sicherzustellen, dass sich Systeme genau wie spezifiziert verhalten. Dies geht über herkömmliche Tests hinaus, indem ein mathematischer Beweis für die Korrektheit geliefert wird und ganze Klassen von Fehlern und Schwachstellen beseitigt werden bevor ein System eingesetzt wird. Das Projekt integriert Sicherheit und Korrektheit bereits in der Entwurfsphase und befürwortet die gemeinsame Entwicklung von Hardware und Software unter Berücksichtigung von formaler Verifikation von Anfang an.

Ein Hauptziel des Projekts ist die Entwicklung eines Unikernels, eine minimalistische Betriebssystemarchitektur, die für die Ausführung einer einzigen Anwendung ausgelegt ist. Durch die Beschränkung auf die notwendigen Komponenten, wie z. B. minimaler Dateisystemunterstützung und Netzwerkfunktionen, reduziert das Design die Angriffsfläche und optimiert die Leistung. Jede Schicht des Unikernels wird der formalen Verifikation unterzogen, wodurch starke Garantien für die Korrektheit und Robustheit des gesamten Systems ermöglicht werden.

Verifizierte Teile des Unikernels:

• Dateisystem und Netzwerkstack, einschließlich Treiber
• CHERI-basierte Speicherisolierung für nicht verifizierten Code
• RISC-V-Prozessor, verifiziert auf Basis der SAIL-Semantik
• Compiler für verifizierte Unikernel-Komposition

Zwischenziele von Formula-V:

• Verifizierte Unikernel-Plattform in Rust und Rocq: Entwicklung eines in Rust geschriebenen Unikernels, um hohen Leistungsanforderungen gerecht zu werden, wobei die formale Verifikation hauptsächlich in Rocq durchgeführt wird. Zu den Verifikationszielen gehören Kernkomponenten wie das Dateisystem und der Netzwerkstack sowie deren Treiber. Dies bildet eine robuste Grundlage für sichere, minimalistische Anwendungsumgebungen.
• CHERI-basierte Isolierung für nicht verifizierten Code: Unterstützung der sicheren Ausführung von nicht verifiziertem Code durch Integration von CHERI-Funktionen. Diese werden verwendet, um eine fein abgestufte Speichersicherheit durchzusetzen, sodass nicht verifizierte Komponenten isoliert ausgeführt werden können. Die RISC-V-Basis wird formal auf der Grundlage der in SAIL definierten Semantik verifiziert.
• Sicherheit auf Hardwareebene mit formalen Gegenmaßnahmen: Einführung formal verifizierter Gegenmaßnahmen gegen Seitenkanal- und transiente Ausführungsangriffe auf Prozessorebene. Diese sind direkt in das Hardware-Design eingebettet und nachweislich sicher, was die Gesamtintegrität des Systems weiter stärkt.
• Automatisierte Tools für die Unikernel-Komposition: Fokuas auf automatisierte Tools zur Vereinfachung der Unikernel-Entwicklung. Ein formal verifizierter Compiler sorgt für zusätzliche Isolierung für nicht verifizierte Komponenten, bei denen formale Speichersicherheitsgarantien fehlen.
• Beschreibung der wichtigsten erwarteten Ergebnisse des Projekts: Die wichtigste Innovation von Formula-V ist ein lückenloser formaler Beweis, der das gesamte System von der Hardware bis zur Anwendungsebene umfasst. Es bietet einen einzigartigen Ende-zu-Ende-Ansatz für die sichere Systementwicklung.