Microkernel seL4: beweisbar fehlerfrei
SeL4 soll laut den Entwicklern der erste Allzweck-Kernel sein, dessen Korrektheit formal bewiesen ist. Der Microkernel läuft auf ARM- und x86-Hardware.
Der vor allem für das Militär tätige Netzwerktechnik-Hersteller General Dynamics C4 Systems und das australische IT-Forschungszentrum NICTA haben den gemeinsam entwickelten Microkernel seL4 als Open Source unter GPL 2 veröffentlicht. Das Besondere an seL4: Die Entwickler wollen formal bewiesen haben, dass die ARM-Variante des Microkernels seine Spezifikation vollständig erfüllt. Das impliziert auch, dass seL4 keine Bugs wie Buffer Overflows, Speicherlecks oder Null Pointer Exceptions enthält. Laut den Entwicklern ist seL4 der einzige Allzweck-Kernel, dessen Korrektheit bewiesen ist.
SeL4 läuft auf den ARM-Plattformen ARMv6 (ARM11) und ARMv7 (Cortex A8, A9, A15) sowie auf x86-Prozessoren bis zu Intels aktueller Haswell-Generation. Gedacht ist der Microkernel vor allem für Embedded Systems; auf x86-Hardware mit VT-x-Erweiterung kann seL4 aber auch einen Linux-Kernel in einer virtuellen Maschine ausführen. Zusätzlich zum Microkernel selbst haben die Entwickler Bibliotheken und Userland-Tools unter BSD-Lizenz veröffentlicht.
[Update 29,7, 17:05] SeL4 basiert auf dem in den 1990er Jahren entwickelten Microkernel L4. Als Microkernel bietet L4 lediglich grundlegende Funktionen zur Speicher-, Thread-, Interrupt- und IPC-Verwaltung; Hardwaretreiber gehören nicht zum Kernel. L4 läuft auf einer Vielzahl von Prozessorplattformen. Weitere Informationen zu L4-Implementierungen und -Betriebssystemen findet man auf L4HQ. [/Update] (odi)
