About / Advertise
Australiska Open Kernel Labs har formellt bevisat att dess hypervisor seL4 innehåller noll buggar. I en artikel i Elektroniktidningens rapportserie Embedded Expert, berättar företagets teknikchef Gernot Heiser hur man gick till väga och de konsekvenser som existensen av beviset kan få för hur säkerhetskritiska system konstrueras i framtiden.
|
OK Labs rapport kan kostnadsfritt tankas hem här (pdf 418 KB). Fler kostnadsfria rapporter finns på etn.se/expert |
Australiska Open Kernel Labs hypervisor OKL4 har haft extrema framgångar som mobilplattform. Elektroniktidningen skrev om mikrokärnan för första gången år 2005. Då hoppades Gernot Heiser att den skulle "revolutionera användandet av inbyggda system".
Han fick rätt. OK Labs kärna har sedan dess hamnat i en halv miljard mobiltelefoner — som har blivit företagets primära nisch.
Orsaken till framgången är att OKL4 har mycket bra prestanda jämfört med tidigare mikrokärnor. Den är en kommersialisering av ett forskningsgenombrott från 90-talet.
Mikrokärnor — minimala operativsystem — kan användas till mycket. I mobilerna fungerar den som ett extra kontrollskikt nära hårdvaran för bland annat säkerhet och resurskontroll. Ett växande användningsområde är för virtualisering, som så kallade hypervisor, att låta flera operativsystem dela på en och samma fysiska processor med illusion av ensam access. OK Labs kan idag bygga smartmobiler som exekverar på enkelkärnor -- ingen separat dsp behövs för basbandshanteringen.
Nu har Open Kernel Labs, som är en avknoppning från det australiska forskningsinstitutet Nicta, gjort ett nytt stort genombrott som återigen bär potentialen att revolutionera inbyggnadsmarknaden: Man har bevisat att en version av OKL4 är formellt korrekt, det vill säga att den motsvarar sin specifikation och är helt fri från buggar.
Projektet har funnits ända sedan företagets starts. Men det har tagit sin tid att fullborda. Det skedde i höstas och sedan dess har Elektroniktidningen tjatat på Open Kernel Labs att skriva en artikel om sin bragd för Elektroniktidningens läsare.
Nu är artikeln äntligen redo för publicering och översatt till svenska.
Vårt maskinrättade bevis är ett av de största som någonsin slutförts. Det finns andra formellt bevisade kärnor, men vårt projekt saknar motsvarighet för mjukvaror av motsvarande storlek och komplexitet.
Så skriver professor Gernot Heiser, teknikchef och drivande kraft bakom Open Kernel Labs.
Formella bevis går långt över de krav som idag ställs för exempelvis certifiering av säkerhetskritisk programvara. Professor Gernot Heiser berättar i artikeln vad som menas med att ett program är bevisat och hur man gick tillväga för att ta fram beviset.
Vår metod var att göra stegvis förfining med hjälp av en interaktiv teorembevisare. Förfiningen leder i bevis att en abstrakt högnivåmodell och en konkret lågnivåmodell motsvarar varandra — alla tänkbara beteenden hos den konkreta modellen fångas av den abstrakta modellen.
Det bevisade operativsystemet heter seL4 och är en så kallad hypervisor — ett program som implementerar så kallad virtualisering, tekniken att spalta upp en fysisk processor till flera virtuella processorer som arbetar oberoende av varandra.
Ett användningsområde för seL4 skulle kunna vara som en extremt pålitlig övervakare av system där exempelvis banktranskationer och helt öppna operativsystem ska samsas på en och samma processor.
Artikeln publiceras exklusivt på svenska av Elektroniktidningen och kan kostnadsfritt tankas hem här, som en pdf (400 kB).
