Sicherer Microkernel seL4 jetzt Open Source

Auf der seLE4-Homepage ist ab sofort der Quellcode eines Microkernels zu finden, dessen Korrektheit formal verifiziert wurde. Mit Hilfe des Theorembeweisers Isabelle/HOL haben die Entwickler bewiesen, dass die Implementierung der Spezifikation des Systems entspricht. seL4 basiert auf dem L4 Microkernel, der auch die Basis für den OKL4-Microkernel ist, der in mehr als einer Milliarde Mobilgeräten eingesetzt wird.

In seL4 sind nur die nötigsten Features als Kernel-Code umgesetzt, der mit höherer Priorität läuft, etwa Prozessorzugriff, Timer und Interrupt-Handling. Andere Betriebssystemfunktionen sind im Userspace implementiert und mit entsprechend weniger Rechten ausgestattet, beispielsweise auch die Device-Treiber. seL4 kann zur Virtualisierung auch als Hypervisor verwendet werden, auf dem beispielsweise Linux als Gastsystem zum Einsatz kommt. 

Nach Meinung der Entwickler ist seL4 nicht auf einen spezifischen Einsatzzweck beschränkt, sondern eignet sich für alle Anwendungen, die Subsysteme voneinander isolieren möchten. Der Schwerpunkt liegt dabei zwar auf Embedded-Systemen, etwa im Automobil- oder Luftfahrt-Sektor, denkbar sind aber beispielsweise auch Finanzanwendungen.

Auch die formale Verifikation des Systems garantiert letztlich keine hundertprozentige Sicherheit oder Zuverlässigkeit, denn sie stellt nur sicher, dass die Implementation des Kernels der Spezifikation entspricht. Bugs etwa im Compiler könnten dennoch noch zu Fehlern im resultierenden Kernelcode führen. Außerdem ist nicht gesichert, dass die Spezifikation als solche fehlerfrei ist.

seL4 läuft x86- und ARM-Prozessoren (v6/7), um die Device-Treiber müssen sich Anwender des Betriebssystems selber kümmern. Freigegeben wurde der Code vom australischen Forschungszentrum NICTA und der Rüstungsfirma General Dynamics C4 Systems. Der Kernel und die Beweise sind unter der GPLv2-Lizenz verfügbar, die User-Libraries unter einer BSD-Lizenz.