About / Advertise
Efter fyra års hårt arbete finns nu ett komplett bevis för att den australiska mikrokärnan SEL4 är helt fri från buggar. SEL4 kommer att revolutionera hur säkra system konstrueras, enligt australiska OK Labs, som ska kommersialisera resultaten.
Klassiskt byggs säkerhetskritiska system av komponenter där man uppskattat att risken för buggar ligger under en bestämd nivå. Nu finns ett operativsystem där risken för buggar är noll – det är formellt bevisat att operativsystemet fungerar exakt enligt specifkationen.Det handlar om en australiska mikrokärnan L4 i en version som kallas SEL4 (Secure Embedded L4). Beviset har utförts av forskningsinstitutet Nicta – en ungefärlig australiensisk motsvarighet till svenska Sics – i samarbete med OK Labs och universitetet i New South Wales i Sydney.
Det finns inga redovisade planer på att SEL4 i sig ska användas kommersiellt. Däremot tänker avknopparen OK Labs nu använda samma formella metoder för att bevisa korrektheten hos sitt syskon-operativsystem OKL4. Och detta kommer enligt OK Labs att öppna helt nya möjligheter för att konstruera säkerhets-, verksamhets- och sekretesskritiska system.
OK Labs teknikchef Gernot Heiser skräder – som vanligt – inte orden.
– Det här är det slutgiltiga beviset på att det faktiskt är möjligt att konstruera buggfri programvara. I framtiden borde ingen nöja sig med mindre när avgörande värden står på spel.
Projektet att bevisa korrektheten hos SEL4 har pågått i fyra år. Elektroniktidningen nämnde projektet för första gången i november 2005.
OK Labs ska använda tekniken för göra sin mikrokärna OKL4 mer attraktiv för affärskritiska applikationer inom mobiltelefoni, affärssekretess och finanstransaktioner.
OKL4 används för virtualisering, det vill säga för att köra separata applikationer på en och samma hårdvara. När OKL4 bevisats enligt modellen som användes för SEL4, betyder det att det inte finns några säkerhetshål i OKL4 och att det därmed är omöjligt för två applikationer som körs på samma processor att exempelvis spionera på varandra via OKL4.
I Windows upptäcks dagligen säkerhetshål som beror av fel i programkoden. I Linux upptäcktes nyligen ett åtta år gammalt säkerhetshål. I SEL4 kommer det aldrig att upptäckas några säkerhetshål.
En grundläggande orsak till att beviset är möjligt att göra är att SEL4 är ett betydligt mindre operativsystem än Linux och Windows. SEL4 består av 7500 programrader, vilket är ungefär vad Linux, som består av cirka sex miljoner rader, växer med i veckan.
Forskarna bevisade 10 000 satser och beviset består av över 200 000 härledningssteg.
Sök på OK Labs i Elektroniktidningens arkiv.
