Diese Woche vermeldete Heise eine kryptische Botschaft: Microkernel seL4 ist beweisbar, fehlerfrei und unter Open Source gestellt. Für Einige ist das wohl eine nichtssagende oder völlig unverständliche Nachricht - für Menschen aber, die sich mit Betriebssystemen und deren kleinen Macken beschäftigen, ist es ein Grund zur Freude.

Bei einem Kernel handelt es sich um das zentrale Element eines Betriebssystems - auf ihm bauen sozusagen alle weiteren Softwarebestandteile auf. Der Beweis, dass der Kern fehlerfrei ist, ist demnach eine kleine Sensation: "Alle Spezifikationen sind vollständig erfüllt", heißt es.
Warum das wiederum so außergewöhnlich ist, darüber sprechen wir mit dem Hacker und IT-Experten Andreas Bogk, der uns erklärt, wie das korrekte Funktionieren eines Betriebssystems mathematisch bewiesen werden kann und was dies für Auswirkungen hat.
Foto: "ATC" von Sarah, CC BY-SA.20