Formellt verifierad OS-kärna

Open Kernel Labs, välkända för sina virtualiserade OS-lösningar i bland annat mobiltelefoner från Motorola, visar nu upp en lösning som är helt konstruerad/verifierad med formella metoder.

Operativsystemet är första resultatet av ett fyraårigt samarbete med NICTA, University of New South Wales i Australien och den hundraprocentiga formella verifieringen innebär att operativsystemet kan certifieras i högsta säkerhetsklass under t ex Common Criteria (EAL).
– Att ha en så här hög säkerhet och tillförlitlighet i grunden ger stora fördelar för till exempel mobiltelefoner, säger Gernot Heiser, CTO för Open Kernel Labs. Man kan lägga in säkra betalningssystem, utan att riskera att de påverkas av annan programvara. Och på samma sätt kan operativsystemet och virtualiseringsfunktionerna användas i kritiska industritillämpningar.
Det nya operativsystemet är nyskrivet från grunden, men har mycket stora likheter med OK Labs nuvarande operativsystem. Det är alltså fullt möjligt att på sikt helt gå över till det nya systemet, men ännu är inga sådana beslut tagna.

Comments are closed.