Formula-V
Das Ziel des Projekts Formula-V ist die Entwicklung eines vollständig formal-verifizierten Systems, das höchste Anforderungen an Sicherheit, Datenschutz und Vertrauenswürdigkeit erfüllt. Mit Hilfe mathematisch-logischer Beweise wird sichergestellt, dass Systeme korrekt funktionieren. Im Projekt werden Software- und Hardware-Verifikation kombiniert, um eine zuverlässige Basis für Anwendungen zu schaffen.
Dies ist besonders relevant für das Internet der Dinge (IoT), das Geräte wie autonome Fahrzeuge oder medizinische Geräte vernetzt. Dessen Komplexität führt zu Sicherheitsrisiken: Angreifer können private Daten auslesen oder ganze Systeme manipulieren.
Das Barkhausen Institut (BI) übernimmt die Projektleitung und koordiniert die Zusammenarbeit mit akademischen und industriellen Partnern.
Außerdem trägt das BI maßgeblich zur Erforschung und Entwicklung der im Projekt notwendigen Verifikationsmethoden bei. Durch die Verifikation von Software und Hardware mittels mathematischer Beweise wird das Ziel eines vertrauenswürdigen IoT-Ökosystems angestrebt. Schwachstellen im System werden dadurch schon während des Systemdesigns erkannt und können behoben werden. Ein solcher mathematischer Beweis über ein vollständiges System ist hochkomplex. Formula-V untersucht daher, inwiefern aktuelle Innovationen aus dem Bereich der formalen Verifikation diese Komplexität reduzieren können. Außerdem wird ein System entwickelt, in dem die formalen Annahmen der Software durch formale Beweise über die Hardware erbracht werden.
Im Projekt wird ein Unikernel-System entwickelt - eine Kombination aus einer einzigen Anwendung und einem minimalen, maßgeschneiderten Betriebssystem. Dieses schlanke Design steigert die Effizienz und Sicherheit des Systems, da es nur die notwendigsten Komponenten wie Dateisystem und Netzwerkfunktionen enthält. Dadurch wird das System effizienter und sicherer. Ergänzt wird es durch robuste Sicherheitsmechanismen. Ein besonderer Schwerpunkt liegt auf der formalen Verifizierung, die die Zuverlässigkeit auf höchstem Niveau gewährleistet.
Die Ergebnisse von Formula-V sollen in IoT, Cloud-Systemen, Smartphones und anderen Technologien eingesetzt werden können. Ziel ist es, formale Verifikation als festen Bestandteil moderner Systementwicklung zu etablieren und so eine vertrauenswürdige digitale Zukunft zu fördern.
Projektlaufzeit: 02.12.2024 - 01.12.2028
Kontakt: Sebastian Ertel (Sebastian.Ertel@barkhauseninstitut.org), Verified System Design Automation
Partner: Technische Universität Dresden, Technische Universität Berlin, Kernkonzept GmbH, Ferrous Systems GmbH, Fraunhofer-Institut für Angewandte und Integrierte Sicherheit (AISEC)
Das Projekt wird finanziert von der Agentur für Innovation in der Cybersicherheit GmbH (Cyberagentur) im Rahmen des Programms „Ökosystem vertrauenswürdige IT – Beweisbare Cybersicherheit (ÖvIT)“.