“:( Your PC ran into a problem and needs to restart” – Der Blue-Screen ist Stellvertreter für Bugs aller Art und wenn er auftritt, hofft man einfach auf das Beste. Die Macher von seL4 aber haben es geschafft, Blue-Screens völlig zu verhindern: Mit Formaler Verifikation (FV) können sie Fehler in ihrem OS-Kernel im vornherein ausschliessen.
Was ist seL4?
seL4 ist ein OS-Kernel (Operating System Kernel), der mit einem Fokus auf Sicherheit, Leistung und Korrektheit konzipiert wurde. Er wurde von Trustworthy Systems (TS) an der Australian National University entwickelt und ist weltweit der erste formell verifizierte und garantiert absturzsichere OS-Kernel. seL4 gehört zu den Real Time OS‘ und ist damit nicht nur sicher, sondern auch schnell.
Seine Anwendungsgebiete sind sicherheitskritische Systeme, bei denen es von entscheidender Bedeutung ist, dass das Betriebssystem fehlerfrei arbeitet, wie etwa:
- Flug- und Raumfahrtssysteme
- Medizinische Geräte
- kritische Infrastruktur
Was ist der Unterschied zwischen seL4 und Windows?
seL4 beherrscht die grundlegenden Aufgaben eines Betriebssystems: Er verwaltet welche Prozesse aktiv sind, handhabt Kommunikation zwischen Prozessen (IPC), interrupts und weist ihnen RAM und CPU-Zeit zu. Man kann seL4 auch als „Hypervisor“ benutzen, was bedeutet, dass er als Host von virtualisierten OS eingesetzt werden kann.
Da seL4 allerdings „nur“ ein OS-Kernel ist, sind die meisten Features wie File Explorer oder Systemeinstellungen, die man von Windows kennt, nicht dabei. Für seL4 sind diese einfach separate Applikationen, welche der User erst installieren muss.
seL4 sorgt dafür, dass diese Applikationen isoliert voneinander laufen, weswegen ein Crash in der einen keine Auswirkungen hat auf die andere. Dies ist anders als in Windows, in welchem sehr viele verschiedene Dienste miteinander verknüpft sind. Ein Crash in einer Komponente legt im schlimmsten Fall das ganze System lahm und verursacht einen Blue-Screen.
seL4 ist beschränkt auf Single-Core support und die FV wurde auch nur auf ARM64 und RISC-V CPU-Architekturen durchgeführt. Entsprechend läuft seL4 nur auf ausgewählter Hardware, während Windows fast überall installiert werden kann.
Wie wurde FV bei seL4 eingesetzt?
TS haben den seL4 in mehrere Konzeptebenen unterteilt. Grob benannt sind diese: die Spezifikation, die Implementation und die Binary. Die Spezifikation ist die abstrakteste Ebene und die Binary als Gegenstück dazu ist die detailreichste.
FV bei seL4 wird aber auf der Implementations-Ebene gemacht. Dazu nimmt man die Post-Conditions einer Funktion und erstellt einen mathematischen Beweis, dass diese stimmen, vorausgesetzt die Pre-Conditions sind erfüllt. Damit der Beweis stichhaltig ist, muss der Code als Beweisgrundlage genommen werden.
Bei seL4 wird die Implementation geparst und die Beweise für die Post-Conditions werden automatisch von dem Tool Isabelle erzeugt.
Diese Beweise sind dann der Garant dafür, dass keine Implementationsfehler vorhanden sind und der Code sich gemäss Spezifikation verhält. Für den Endnutzer bedeutet dies, dass der Kernel nie crasht.
Video: Kurzübersicht über Formale Verifikation
Wieso ist Windows nicht ebenfalls formal verifiziert?
Tatsächlich sind Teile von Windows formal verifiziert, etwa die Hypervisor-Technologie und einige Kernel-Komponenten. Allerdings ist Windows viel umfangreicher als seL4: seL4 hat etwa 10’000 Zeilen Code, während Windows über 50 Mio. hat. Dies macht eine formelle Verifikation allein vom Aufwand her beinahe unmöglich.
Dazu kommt, dass seL4 auf einige Features verzichten muss, damit die Beweisführung mit Isabelle gelingt – Features, auf die Windows nicht verzichten kann: Dies fängt bei Multi-Core support an und hört bei Function-Pointers im Source Code auf.
Windows wird darum wohl nicht so schnell ganz verifiziert sein und wir werden weiterhin dem Blue-Screen begegnen.
