Das australische IT-Forschungszentrum NICTA und der vor allem für das Militär tätige Netzwerktechnik-Hersteller General Dynamics C4 Systems haben den gemeinsam entwickelten Microkernel seL4 unter GPL 2 als Open Source veröffentlicht. Dass die ARM-Variante des Microkernels seine Spezifikation vollständig erfüllt, wollen die Entwickler zudem formal bewiesen haben, was auch impliziert, dass seL4 keine Bugs wie Speicherlecks, Null Pointer Exceptions oder Buffer Overflows enthält. seL4 ist der einzige Allzweck-Kernel, dessen Korrektheit laut den Entwicklern bewiesen ist.

SeL4 läuft bis zu Intels aktueller Haswell-Generation auf x86-Prozessoren sowie auf den ARM-Plattformen ARMv6 (ARM11) und ARMv7 (Cortex A8, A9, A15). Der Microkernel ist vor allem für Embedded Systems gedacht, kann auf x86-Hardware mit VT-x-Erweiterung aber auch in einer virtuellen Maschine einen Linux-Kernel ausführen. Die Entwickler haben zusätzlich zum Microkernel selbst Userland-Tools und Bibliotheken unter der BSD-Lizenz veröffentlicht.

SeL4 basiert auf dem Microkernel L4, der in den 1990er Jahren entwickelt wurde. L4 bietet als Microkernel lediglich grundlegende Funktionen zur Thread-, Interrupt-, Speicher- und IPC-Verwaltung; Hardwaretreiber gehören nicht dazu. Auf L4HQ findet man weitere Informationen zu L4-Betriebssystemen und -Implementierungen.

(mt, hannover)

(siehe auch Heise-News-Ticker:)

Hannover · EDV-Beratung · Linux · Novell · Microsoft · Seminar · IT-Consult · Netzwerk · LPIC · CLE