Open Kernel Labs (OKL) heeft een microkernel voor zijn embedded hypervisor ontwikkeld die formeel wiskundig gevalideerd is. Daarmee is gegarandeerd dat de software zich gedraagt zoals beschreven. Het Australische bedrijf gaat deze SEL4-kernel inzetten in de toekomstige generaties van zijn embedded hypervisor, die daardoor geschikt wordt voor veiligheidskritieke systemen. Het is het resultaat van een vier jaar durend researchproject samen met onder meer de universiteit van New South Wales.
Wiskundige verificatie kijkt naar de code en algoritmes zelf, in plaats van dat het het gedrag vergelijkt met de verwachte resultaten. Dit elimineert veel voorkomende problemen zoals ontwerpfouten, buffer overflows, nullpointer-derefereties en geheugenlekken. De kernel is een afsplitsing van het opensource L4-project, dat ook ten grondslag ligt aan de OKL4-hypervisor van het bedrijf. De software beslaat zo‘n 8700 regels C-code plus nog zo‘n 600 assembly-regels.
De OKL4-hypervisor draait de gast-OS‘en volledig in userspace en kan onder meer Linux, Symbian en Windows CE en Mobile aan.
This article is exclusively available to premium members of Bits&Chips. Already a premium member? Please log in. Not yet a premium member? Become one for just €20 for the first year and enjoy all the benefits.