JavaScript is currently disabled.Please enable it for a better experience of Jumi.
Guidelines for contributing Technical Papers: download PDF
Embedded expert 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.
embexOK 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).
ANNONS:

Oktoberchansen

Vill du ha en Raspberry Pi – den populära enkortsdatorn från Farnell element14?
    Vi delar ut tio Raspberry Pi 3 Model B+ bland de som tecknar en ny prenumeration på Elektroniktidningen under september och oktober. Även trogna prenumeranter som förnyar sina uppgifter kan delta i kampanjen.
    Farnell element14 sponsrar kampanjen, som pågår fram till midnatt den 31 oktober.
    OBS glöm inte att kryssa i rutan för nyhetsbrev för att kunna vara med i utdelningen!
Prenumerera och delta!
MER LÄSNING:
 
SENASTE KOMMENTARER
Kommentarer via Disqus

Vi gör Elektroniktidningen

Anne-Charlotte Sparrvik

Anne-Charlotte
Sparrvik

+46(0)734-171099 ac@etn.se
(sälj och marknads­föring)
Per Henricsson

Per
Henricsson
+46(0)734-171303 per@etn.se
(redaktion)

Anna Wennberg

Anna
Wennberg
+46(0)734-171311 anna@etn.se
(redaktion)

Jan Tångring

Jan
Tångring
+46(0)734-171309 jan@etn.se
(redaktion)