Unser open-source L4Re Operating System Framework gibt es bereits seit mehr als einem Jahrzehnt, aber unsere Systemingenieure arbeiten stetig daran, es zu verbessern. Eines unserer wichtigsten Zukunftsprojekte ist die formale Verifizierung des L4Re Operating System Framework. Mit formalen Methoden wollen wir die Qualität von L4Re für den Einsatz in sicherheitskritischen Systemen verbessern.
An dieser Stelle möchten wir unseren Kollegen Hendrik Tews vorstellen, der seit 2017 bei uns ist. Er hat lange wissenschaftlich auf dem Gebiet der formalen Methoden gearbeitet; sowohl als Forscher als auch in der freien Wirtschaft hat er sich mit dem Thema beschäftigt und für mehrere Softwarehersteller gearbeitet.
Bei Kernkonzept arbeitet Hendrik hauptsächlich an der Vorbereitung und Durchführung von Sicherheitszertifizierungen für unser quelloffenes L4Re Operating System und Hypervisor Framework. Zertifizierung und formale Verifizierung sind eng miteinander verbunden: Beide zielen darauf ab zu beweisen, dass eine bestimmte Software zuverlässig das tut, was sie tun soll.
Hendrik hilft uns, einen langfristigen Plan umzusetzen: die formale Spezifizierung der Eigenschaften des L4Re Operating System Framework und der formale Beweis seiner Korrektheit. Die formale Verifizierung einer realen Software ist teuer und zeitaufwendig, selbst bei einem Mikrokern mit einer minimalen Codebasis. Viele Unternehmen scheuen den Aufwand, und so ist formale Verifizierung im Softwaremarkt bis heute sehr selten.
Wir glauben dennoch, dass es zukünftig einen Unterschied machen kann - vor allem, weil L4Re in vielen sicherheitskritischen Anwendungen mit höchsten Qualitätsanforderungen eingesetzt wird. Mit Hilfe formaler Methoden können wir die Qualität und Sicherheit des L4Re Operating System Framework weiter verbessern.
Was lässt sich mit formalen Methoden beweisen - und was nicht?
Als formale Methoden bezeichnet man eine Sammlung von Techniken, mit denen sich die Korrektheit einer Software im mathematischen Sinn beweisen lässt. Genauso, wie jedes Dreieck eine Winkelsumme von 180° hat, ist jede formal bewiesene Software fehlerfrei.
Natürlich gibt es auch viele Dreiecke, deren Winkelsumme größer ist als 180°, zum Beispiel auf der Oberfläche einer Kugel in der nicht-Euklidischen Geometrie. Und so kann auch ein formal bewiesenes Programm Fehler aufweisen. Zum Beispiel, weil die Spezifikation das falsche Verhalten nicht ausgeschlossen hat oder weil das Programm auf einer nicht formal verifizierten Hardware läuft oder weil Teile des Programms nicht formal verifiziert wurden.
Dennoch zeigt die Erfahrung, dass die formal verifizierten Teile eines Programms bezüglich der Eigenschaften, die bei der formalen Verifizierung berücksichtigt wurden, fehlerfrei sind.
So wollen wir L4Re formal verifizieren
Unser langfristiges Ziel, eine formal verifizierte Variante von L4Re, erfordert einen riesigen Aufwand. Daher gehen wir in kleinen Schritten vor: Zuerst wollen wir ein abstraktes Modell des L4Re-Kerns entwickeln, um die Separationseigenschaft dieses Modells zu beweisen und um den Nachweis zu erbringen, dass sich das echte L4Re so verhält wie vom Modell spezifiziert.
Wir werden L4Re durch modellbasiertes Testen prüfen und die Gleichwertigkeit von L4Re und dem abstrakten Modell mit einer 6-stelligen Anzahl von Tests nachweisen. Modellbasiertes Testen kann viel unerwartetes und fehlerhaftes Verhalten enthüllen, sogar in den Systemteilen, die weg-abstrahiert wurden und daher im Modell gar nicht enthalten sind.
Das Ergebnis kann als formal verifiziertes Design von L4Re verstanden werden, vergleichbar mit dem, was das Common-Criteria-Schema für höhere Sicherheitsstufen verlangt.
Brauchen wir formale Verifizierung?
Noch nicht! Die meisten Software-Firmen investieren bisher nicht in formale Verifizierung. Aber bestimmte Marktsegmente könnten tatsächlich in Zukunft formale Verifizierung verlangen; es ist durchaus denkbar, dass formale Methoden eines Tages für Software-Zertifizierung und Zulassung offiziell vorgeschrieben sein können.
Kernkonzept möchte auf diese Zukunft vorbereitet sein, dafür sprechen wir bereits heute mit entsprechenden Stakeholdern und regen diese Entwicklung an. Aktuelle Trends in der Software-Industrie ermutigen uns, den von uns eingeschlagenen Pfad weiterzuverfolgen.
