{"id":13086,"date":"2023-03-23T11:15:25","date_gmt":"2023-03-23T10:15:25","guid":{"rendered":"https:\/\/www.kernkonzept.com\/kk-staging\/?post_type=10_years&p=13086"},"modified":"2025-12-22T10:47:37","modified_gmt":"2025-12-22T09:47:37","slug":"looking-further-getting-formal-verification-for-l4re","status":"publish","type":"10_years","link":"https:\/\/www.kernkonzept.com\/de\/kk_10_years\/looking-further-getting-formal-verification-for-l4re\/","title":{"rendered":"Blick in die Zukunft: formale Verifizierung f\u00fcr L4Re"},"content":{"rendered":"

Unser open-source L4Re Operating System Framework gibt es bereits seit mehr als einem Jahrzehnt<\/a>, 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\u00e4t von L4Re f\u00fcr den Einsatz in sicherheitskritischen Systemen verbessern.<\/em><\/p>\n

An dieser Stelle m\u00f6chten 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\u00e4ftigt und f\u00fcr mehrere Softwarehersteller gearbeitet.<\/p>\n

Bei Kernkonzept arbeitet Hendrik haupts\u00e4chlich an der Vorbereitung und Durchf\u00fchrung von Sicherheitszertifizierungen f\u00fcr unser quelloffenes L4Re Operating System und Hypervisor Framework<\/a>. Zertifizierung und formale Verifizierung sind eng miteinander verbunden: Beide zielen darauf ab zu beweisen, dass eine bestimmte Software zuverl\u00e4ssig das tut, was sie tun soll.<\/p>\n

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.<\/p>\n

Wir glauben dennoch, dass es zuk\u00fcnftig einen Unterschied machen kann - vor allem, weil L4Re in vielen sicherheitskritischen Anwendungen mit h\u00f6chsten Qualit\u00e4tsanforderungen eingesetzt wird. Mit Hilfe formaler Methoden k\u00f6nnen wir die Qualit\u00e4t und Sicherheit des L4Re Operating System Framework weiter verbessern.<\/p>\n

Was l\u00e4sst sich mit formalen Methoden beweisen - und was nicht?<\/h2>\n

Als formale Methoden bezeichnet man eine Sammlung von Techniken, mit denen sich die Korrektheit einer Software im mathematischen Sinn beweisen l\u00e4sst. Genauso, wie jedes Dreieck eine Winkelsumme von 180\u00b0 hat, ist jede formal bewiesene Software fehlerfrei.<\/p>\n

Nat\u00fcrlich gibt es auch viele Dreiecke, deren Winkelsumme gr\u00f6\u00dfer ist als 180\u00b0, zum Beispiel auf der Oberfl\u00e4che 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\u00e4uft oder weil Teile des Programms nicht formal verifiziert wurden.<\/p>\n

Dennoch zeigt die Erfahrung, dass die formal verifizierten Teile eines Programms bez\u00fcglich der Eigenschaften, die bei der formalen Verifizierung ber\u00fccksichtigt wurden, fehlerfrei sind.<\/p>\n

So wollen wir L4Re formal verifizieren<\/h2>\n

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\u00e4lt wie vom Modell spezifiziert.<\/p>\n

Wir werden L4Re durch modellbasiertes Testen pr\u00fcfen und die Gleichwertigkeit von L4Re und dem abstrakten Modell mit einer 6-stelligen Anzahl von Tests nachweisen. Modellbasiertes Testen<\/a> kann viel unerwartetes und fehlerhaftes Verhalten enth\u00fcllen, sogar in den Systemteilen, die weg-abstrahiert wurden und daher im Modell gar nicht enthalten sind.<\/p>\n

Das Ergebnis kann als formal verifiziertes Design von L4Re verstanden werden, vergleichbar mit dem, was das Common-Criteria-Schema<\/a> f\u00fcr h\u00f6here Sicherheitsstufen verlangt.<\/p>\n

Brauchen wir formale Verifizierung?<\/h2>\n

Noch nicht! Die meisten Software-Firmen investieren bisher nicht in formale Verifizierung. Aber bestimmte Marktsegmente k\u00f6nnten tats\u00e4chlich in Zukunft formale Verifizierung verlangen; es ist durchaus denkbar, dass formale Methoden eines Tages f\u00fcr Software-Zertifizierung und Zulassung offiziell vorgeschrieben sein k\u00f6nnen.<\/p>\n

Kernkonzept m\u00f6chte auf diese Zukunft vorbereitet sein, daf\u00fcr sprechen wir bereits heute mit entsprechenden Stakeholdern und regen diese Entwicklung an. Aktuelle Trends in der Software-Industrie<\/a> ermutigen uns, den von uns eingeschlagenen Pfad weiterzuverfolgen.<\/p>","protected":false},"excerpt":{"rendered":"

While our open-source L4Re Operating System Framework was originally developed more than a decade ago, our system engineers are steadily working to improve it. One of our most important future projects is formal verification of the correctness of the L4Re Operating System Framework. With formal methods, we aim to improve the quality of L4Re for […]<\/p>\n","protected":false},"featured_media":1698,"template":"","format":"standard","meta":{"_acf_changed":false},"class_list":["post-13086","10_years","type-10_years","status-publish","format-standard","has-post-thumbnail","hentry"],"acf":[],"_links":{"self":[{"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/10_years\/13086","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/10_years"}],"about":[{"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/types\/10_years"}],"version-history":[{"count":3,"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/10_years\/13086\/revisions"}],"predecessor-version":[{"id":18628,"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/10_years\/13086\/revisions\/18628"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/media\/1698"}],"wp:attachment":[{"href":"https:\/\/www.kernkonzept.com\/de\/wp-json\/wp\/v2\/media?parent=13086"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}