seL4

Wir berichten über die formale, maschinengeprüfte Verifikation des seL4-Mikrokernels von einer abstrakten Spezifikation bis hin zu seiner C-Implementierung. Wir gehen von der Korrektheit des Compilers, des Assembliercodes, der Hardware und des Bootcodes aus. seL4 ist ein Mikrokernel der dritten Generation aus der L4-Familie, der 8700 Zeilen C und 600 Zeilen Assembler umfasst. Seine Leistung ist vergleichbar mit anderen Hochleistungs-L4-Kernen. Wir beweisen, dass die Implementierung stets strikt unserer hochabstrakten Spezifikation des Kernverhaltens folgt. Dies umfasst traditionelle Sicherheitsmerkmale von Design und Implementierung, wie dass der Kernel niemals abstürzt und niemals eine unsichere Operation ausführt. Es impliziert auch viel mehr: Wir können genau vorhersagen, wie der Kernel in jeder möglichen Situation reagieren wird.