Een besturingssysteem dat volgens de ontwikkelaars tot één van de veiligste ter wereld behoort gaat verder als opensourcesoftware. Dat hebben het Australische NICTA en General Dynamics C4 Systems laten weten. Het besturingssysteem in kwestie is de secure embedded L4 (seL4) microkernel.

Het zou de eerste kernel van een besturingssysteem zijn waarbij wiskundig kan worden aangetoond dat die correct werkt. Daardoor zou de kernel betrouwbare van onbetrouwbare software kunnen scheiden om belangrijke diensten tegen fouten of kwaadaardige aanvallen te beschermen. De kernel zou ook niet kunnen werken op een manier die niet door de ontwikkelaars is bedoeld.

"seL4 brengt softwareafhankelijkheid naar een nieuw niveau en zal de ontwikkeling van echt betrouwbare systemen ondersteunen", zegt Gernot Heiser, onderzoeksleider van het NICTA. Volgens hem is een oplossing als seL4 dringend nodig. "Er zijn genoeg voorbeelden van de fundamentele tekortkomingen in de hedendaagse kritieke software."

Door het opensource maken van seL4 hoopt Heiser dat er een wereldwijde gemeenschap van ontwikkelaars ontstaat die zich bezighouden met toepassingen voor de nationale veiligheid, luchtvaart, auto-industrie, medische implantaten, industriële automatisering en BYOD in zakelijke omgevingen. De broncode van het besturingssysteem en de software om de wiskundige correctheid van het systeem te bepalen zijn onder een standaard opensourcelicentie uitgebracht.