Formeel geverifieerde microkernel is nu opensource

SEL4, ‘s werelds enige volledig formeel geverifieerde microkernel, is als opensource vrijgegeven. Het Australische onderzoekscentrum Nicta en het Amerikaanse General Dynamics hebben de broncode en de bewijzen van de kernel en aanvullende software beschikbaar gemaakt onder verschillende licenties: de kernel zelf valt onder de GPL versie 2, de drivers hebben een BSD-gebaseerde licentie meegekregen. SEL4 draait op X86 en de belangrijkste Arm-architecturen.

SEL4 is gebaseerd op de L4-familie van microkernels, die hoge prestaties najagen en tegelijkertijd aan de ontwerpfilosofie van microkernels voldoen: alles wat niet met de hoogste hardwarepermissies hoeft te draaien, wordt uit de kernel geweerd. Nicta en haar spin-off Open Kernel Labs bewezen in 2009 formeel dat de C-code en de gecompileerde versie van hun SEL4-kernel volledig voldoen aan de specificaties. Open Kernel Labs werd in 2012 overgenomen door General Dynamics.

De ontwikkelaars claimen dat de microkernel door de formele verificatie vrij is van bugs; althans, zolang aan de randvoorwaarden wat betreft hardware voldaan wordt én zolang er geen onverhoopte bugs in de specificaties zitten. Drivers en applicatiesoftware wordt hiermee niet automatisch veiliger, maar doordat ze niet in de kernel draaien, zijn ze beter van elkaar geïsoleerd. Daarom is de microkernel uitermate geschikt om veiligheids- en missiekritieke systemen te bouwen.