SeL4 kan onderscheid maken tussen betrouwbare en onbetrouwbare software. De software is de afgelopen zeven jaar ontwikkeld door National ICT Australia (NICTA) samen met Open Kernel Labs (OK Labs).

De software is nu beschikbaar voor fabrikanten en onderzoekers om te testen. Volgens onderzoeker Gerwin Klein werd vorig jaar door de Universiteit van New South Wales (UNSW) voor het eerst bewezen dat een "general-purpose operating system kernel" mogellijk was, de seL4.

Heilige graal

"Onze seL4 microkernel is de evolutie van het vorig jaar geleverde bewijs", aldus Klein in een verklaring. "Het is de enige besturingssysteem kernel ter wereld waarvan de code mathematisch heeft bewezen de specificatie correct te implementeren. Door dit bewijs zal de seL4 ARM11 kernel altijd precies doen wat zijn specificatie zegt wat het zal doen." Hierdoor kan de software niet falen, aldus de onderzoekers.

Al sinds de jaren '70 is er gezocht naar zulke software. "Naar gecontroleerde operating-system kernels is gezocht sinds de jaren '70, en ons is het gelukt", aldus Gernot Heiser, oprichter van OK Labs.

Complete bescherming

Volgens NICTA is het mogelijk om financiële software helemaal veilig te houden en tegelijkertijd "onbetrouwbare software" op dezelfde computer te draaien. Ook zou seL4 bedrijfskritische defensiegegevens helemaal veilig kunnen opslaan, terwijl op hetzelfde systeem gebruik wordt gemaakt van aplicaties als e-mail. Ook kan het gebruikt worden om bijvoorbeeld levens ondersteunende apparaten van medische aard te beschermen tegen hackers.