Status: aktiv (Okt. 2020 - Sep. 2023)
Gefördert durch: Bayerisches Staatsministerium für Wirtschaft, Landesentwicklung und Energie
Partner:
- Hensoldt Cyber GmbH (Taufkirchen)
- TU München
- CSIRO Data 61 (Canberra, Australien)
Erweiterung der Grundlagen für formale Verifikation von Software und deren Anwendung
Informationen zum Projekt
Das Projekt SW_GruVe baut auf den Ergebnissen des Projekts HoBIT auf. Die dort entwickelten Konzepte und Demonstratoren werden in Richtung auf praktisch anwendbare Werkzeuge weiter entwickelt.
Das Werkzeug Gencot
Zentrale Komponente der Projektanteile bei CODE ist das Werkzeug Gencot. Es soll eine möglichst weit automatisierte Übersetzung von C-Programmen in die Sprache Cogent ermöglichen. Cogent wurde von Data61 entwickelt und ermöglicht neben der Erzeugung von ausführbarem Maschinencode die automatische Generierung eines Refinement-Beweises, mit dem verifizierbar ist, dass sich der Maschinencode gemäß der Semantik des Quellprogramms verhält. Cogent ist eine rein funktionale Programmiersprache mit zusätzlichen Einschränkungen ähnlich wie bei Rust.
Das Ziel von Gencot ist es, diese Sprache und die zugehörige Verifikationsmethode für C-Entwickler zugänglich zu machen, indem es C-Programme nach Cogent übersetzt. Das Ergebnis erfüllt nicht immer alle erforderlichen Einschränkungen und erfordert dann Nachbearbeitung, die sich aber normalerweise auf wenige kritische Anteile beschränkt. Dadurch sollte der Einstieg in die Nutzung von Cogent deutlich erleichtert werden.
Gencot ist open Source Software und verfügbar auf der GitHub-Seite von CODE unter https://github.com/F1-C0D3/.
Anwendung: TRENTOS
Um die Praxisrelevanz von Gencot sicher zu stellen wird die Entwicklung ständig begleitet durch die Anwendung auf TRENTOS-Komponenten. TRENTOS ist das vom Projektpartner Hensoldt Cyber entwickelte Betriebssystem für hochsichere Anwendungen und basiert auf dem Mikrokern seL4. Im Projekt wird Gencot auf zwei ausgewählte Komponenten angewendet, die im Projekt entwickelt und parallel manuell verifiziert werden. Auf diese Weise ist ein Vergleich des erforderlichen Aufwands und Know-How für beide Vorgehensweisen möglich.
Als dritte Komponente wird Gencot auf die unabhängig entwickelte open-Source-Bibliothek mbedTLS angewendet, eine Implementierung des TLS-Protokolls im Umfang von ca. 100.000 LoC für eingebettete Systeme. Damit soll erprobt werden, wie weit der Ansatz geeignet ist, auch Programmcode einer formalen Verifikation zugänglich zu machen, der für eine manuelle Bearbeitung zu umfangreich ist.
Sowohl die manuellen Verifikationen als auch die durch Cogent und Gencot generierten Beweise verwenden das interaktive Beweiswerkzeug Isabelle, dessen Entwicklerteam an der TU München ebenfalls als Partner am Projekt SW_GruVe beteiligt ist.