OK Labs kommer erbjuda en kommersiell version av den bevisat korrekta mikrokärnan SEL4. Redan idag anser OK Labs att dess mikrokärna är den effektivaste på marknaden för inbyggda system. Den används bland annat i hundra miljoner mobiltelefoner, och företaget hoppas att kombinationen säker och effektiv ska kunna ge ännu fler användare.

Avlyssningssäker kommunikation, finansiella transaktioner och säkerhetskritiska system inom rymd och fordon. Det är några av de tillämpningsområden företaget tittar på.

En liten del av beviset

Beviset består av 200 000 rader, cirka 3500 A4-sidor. Det är skrivet för hand och därefter verifierat av dator. Bevisprocessen tog mellan 25 och 30 personår i anspråk. Med de kunskaper som vanns i processen skulle jobbet idag kunna göras om på mindre än 10 personår.

Bevisat korrekt programvara är ingen nyhet. Flera bevisat korrekta programmoduler används i flygplan från Airbus. Men de är mindre än SEL4 och komplexiteten i bevisen växer exponentiellt med storleken på programvaran.

Också det tyska forskningsprojekt Verisoft har bevisat programvaras korrekthet för tillämpningar inom bland annat medicin och fordon. Där finns bevis som är ännu längre än beviset för SEL4, men i C-kodrader räknat är SEL4 den största bevisade programvaran idag.

Prickar är C-funktioner i SEL4. Strecken är fuktionsanrop. Nätet är komplext och därmed även beviset. Klicka på bilden för större version.

Man skulle kanske gissa att SEL4 är enkelt konstruerad för att vara enkel att göra bevis kring. Men så är inte fallet. Den är optimerad för prestanda, och har ett nätverk av beroende mellan sina beståndsdelar, vilket gör beviset komplext.

OK Labs ska nu använda samma teknik för att bevisa korrektheten hos syskonoperativsystemet OKL4. De två kärnorna har mycket gemensamt och därmed tror företaget att mycket av bevisföringen kommer att kunna återanvändas.

Det som bevisats är att den C-programkod som implementerar SEL4 är ekvivalent med en formell specificering av mikrokärnan. Eller närmare bestämt att C-kodens beteende ligger inom det möjliga beteendet för den formella kärnans beteende.

Det faktum att ekvivalensen nu är bevisad öppnar nya möjligheter till att göra ytterligare bevis kring specifikationen som är giltiga även för C-koden.

Att SEL4 i och med detta faktiskt verkligen är korrekt, är avhängigt ett antal antaganden, till exempel att den formella specifikation i sig är korrekt, att kompilatorn är korrekt och att hårdvaran är korrekt. OK Labs påpekar till och med skämtsamt att beviset förutsätter att formell logik är korrekt, "men om så inte är fallet står matematiken inför betydligt större problem än att bevisa en mikrokärna".

Det fina med beviset är det ger som konsekvens att ett stort antal vanliga programfel omöjligen kan finnas i SEL4, som exempelvis minnesreferenser via ickeinitierade variabler, referenser utanför reserverad minnesadress (ett vanligt virusknep), att minne går förlorat genom att det reserveras men aldrig avbokas och division med noll.

Under det att beviset genomfördes genomgick programvaran några mindre omskrivningar och en lite större revidering, och bevisen måste delvis skrivas om. Det här var delvis planerade komplikationer i syfte för att lära forskarna hur mycket beviset påverkas av revideringar.

Dessutom upptäcktes och rättades 144 buggar. Man hade med flit avstått från att granska koden enligt konventionella metoder. OK Labs förväntar sig att hitta betydligt färre buggar i OKL4, eftersom den konstruerats mer omsorgsfullt.

C-koden till mikrokärnan SEL4 består av 8700 rader C-kod och 600 rader assemblerkod. Av dessa bevisades 7500 av C-kodraderna vara korrekta. Assemblern och de obevisade C-kodraderna är bland annat bootkod och anses ligga utanför själva kärnan.

Kod som används i kritiska tillämpningar idag är typiskt inte bevisat korrekt. Istället har den genomgått en granskningsprocess. Som tumregel kostar det, enligt OK Labs, 10 000 dollar att granska en rad C-kod enligt standarden Common Criteria 6. OK Labs bevis genomfördes till en tiondel av den kostnaden. En klassisk granskning ger dessutom inget äkta bevis, utan "bara" en stark trovärdighet för att koden sannolikt är korrekt.

OK Labs hoppas kunna argumentera inför certifieringsinstitutioner att ett korrekthetsbevis borde vara lika mycket värt som en hög sannolikhet för korrekthet.

Det ligger inget magiskt genombrott bakom det faktum att detta bevis kunde genomföras. Enligt OK Labs handlar det om en kombination av aktuell kunskap i forskningsfronten, och att det fanns expertis på verifiering och mikrokärnor i forskargruppen.

Här (länk) finns mer information om beviset, både för lekmän och matematiker.