Open Source im professionellen Einsatz

Sicherer Microkernel soll Open Source werden

25.06.2014

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.

177

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.

Ähnliche Artikel

comments powered by Disqus

Stellenmarkt

Artikelserien und interessante Workshops aus dem Magazin können Sie hier als Bundle erwerben.