Der Microkernel Sel4 soll laut Webseite Open Source werden.
Die Macher des Secure-Microkernel-Projekts, die den Sel4-Microkernel entwickeln, wollen Ende Juli den Quellcode veröffentlichen. Die ARM-Version des Kernel soll mathematisch fehlerfrei und sicher sein.
Wie die Macher des Microkernel auf ihrer neuen Webseite schreiben, gibt es einen mathematischen Beweis, laut dem die C-Implementierung mit der Spezifikation überein stimme und daher fehlerfrei sei. Zudem gebe es einen weiteren Beweis, nach dem das auf der Hardware ausgeführte Binary eine korrekte Übersetzung des ursprünglichen C-Codes darstelle.
Der Microkernel Sel4 soll laut Webseite Open Source werden.
Als Konsequenz aus den beiden Beweisen bezeichnen die Macher ihren OS-Kernel auch als in einem starken Sinne sicher. Auf ihm würden sich keine Buffer-Overflows oder Null-Pointer-Exceptions ausnutzen lassen. Nicht zuletzt sei der Kernel der erste Protected-Mode-Kernel mit einer gesunden und kompletten Pünktlichkeitsanalyse: Der Kernel könne dem Entwickler harte Echtzeit-Garantien geben.
Während die Webseite für die Open-Source-Veröffentlichung bereits existiert, ist noch unklar, unter welche Lizenz die Macher ihren sicheren Kernel stellen wollen. Entwickelt wurde dieser unter dem Dach des australischen IKT-Forschungszentrums NICTA, eine binäre Version lässt sich bereits heute herunterladen. Mit zum Paket gehören eine formale Spezifikation, User-Level-Bibliotheken, Beispielcode sowie ein paravirtualisiertes Linux. Aktuell arbeiten die Entwickler an Multiprozessor-Support.
