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 eine lange wissenschaftliche Geschichte auf dem Gebiet der formalen Methoden; er hat sich sowohl als Forscher als auch in der freien Wirtschaft 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 unsere Open-Source L4Re-Technologie. 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 Frameworks und der formale Beweis seiner Korrektheit. Die formale Verifizierung einer realen Software ist teuer und zeitaufwendig, selbst bei einem Mikrokernel mit einer minimalen Codebasis. Viele Unternehmen scheuen den Aufwand, zumal formale Verifizierung im Softwaremarkt noch kaum eine Rolle spielt.
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 Frameworks weiter verbessern.
Was beweisen formale Methoden - und was nicht?
Formale Methoden bezeichnen eine Sammlung von Techniken, mit denen sich die Korrektheit einer Software im mathematischen Sinn beweisen lässt. Genauso, wie es keine Dreiecke mit einer Winkelsumme von mehr als zwei rechten Winkeln gibt, kann eine formal bewiesene Software nicht versagen.
Natürlich können Dreiecke größere Winkelsummen haben, etwa auf der Oberfläche einer Kugel (in der nicht-euklidischen Geometrie). Genauso kann ein formal bewiesenes Programm Fehler haben. So könnte die Spezifizierung das falsche Verhalten nicht ausgeschlossen haben, weil das Programm auf einer nicht formal verifizierten Hardware läuft oder weil Teile des Programms bei der formalen Verifizierung weggelassen 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, benötigt sehr viel Einsatz. 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 und sein abstraktes Modell durch modellbasiertes Testen untersuchen und die Gleichwertigkeit beider mit einer 6-stelligen Anzahl von Tests überprüfen. 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 entsprechende Stakeholder an. Aktuelle Trends in der Software-Industrie ermutigen uns, auf dem von uns eingeschlagenen Pfad zu bleiben.
