Forskere ved den australske forskningsinstitusjonen Nicta kunngjorde i forrige uke at de har levert verden første formelle, maskinsjekkede bevis på en operativsystem-kjerne for generell bruk. Dette gir løfter helt nye nivåer av pålitelighet for sikkerhetskritisk programvare.
Ifølge Nicta kan det nå matematisk bevises at programvare som brukes sikkerhetsrelaterte systemer i blant annet fly og motorkjøretøyer er uten en omfattende klasse med feil.
Forskerne har laget en mikrokjerne, Secure Embedded L4 (seL4), som er designet for virkelig bruk, og som skal ha potensial for både militære og sivile bruksområder hvor feilfri drift av komplekse, integrerte systemer er ekstremt viktig.
- Det er vanskelig å kommentere denne bragden uten å ty til klisjeer, sier Lawrence C. Paulson, professor i matematisk logikk ved Cambridge Universitys Computer Laboratory, i en pressemelding.
- Det å bevise korrektheten til 7500 linjer med C-kode i et operativsystems kjerne er en unik bragd, som etter hvert bør føre til at programvare oppnår pålitelighetsgrader som i dag er utenkelige, sier Paulson.
- Formelle bevis for spesifikke egenskaper har blitt utført for mindre kjerner, men det vi har utført er et bevis for generell, funksjonell korrekthet, noe som aldri tidligere har blitt oppnådd for høy-ytelses programvare for virkelig bruk med en slik kompleksitet eller størrelse, forklarer Gerwin Klein, forskningsleder ved Nicta og leder for forskningsgruppen som står bak beviset.
En del av beviset demonstrerer at mange typer angrep ikke vil fungere mot seL4-kjernen. Dette inkluderer angrep som utnytter bufferoverflytsfeil.
seL4 og pålitelighetsbeviset er resultatet av fire års forskning som har blitt utført av Kleins forskningsgruppe på 12 medlemmer. Blant medlemmene av forskningsgruppen var det forskere fra Nicta, samt doktorgradsstudenter og ansatte ved University of New South Wales.
Sammen har disse verifisert 7500 linjer med C-kode og bevist mer enn 10 000 hjelpesetninger i mer enn 200 000 linjer med formelt bevis. Beviset er maskinsjekket ved hjelp av Isabelle, et interaktivt program for bevis av teoremer. Ifølge Nicta er dette ett av de største maskinsjekkede bevisene som noensinne har blitt gjort.
- Arbeidet går ut over den vanlige sjekkingen etter mangel på visse, spesifikke feil. I stedet verifiserer det full overensstemmelse med systemspesifikasjonen. Prosjektet har resulterte ikke bare i en verifisert mikrokjerne, men også en samling av teknikker som kan bli brukt til å utvikle annen verifisert programvare, sier Paulson.
Dette inkluderer nye teknikker for formell maskinsjekking av bevis, framskritt innen den matematiske forståelsen av virkelige programmeringsspråk, samt metoder for raskt prototyping av operativsystem-kjerner.
- Dette er en oppsiktsvekkende bragd, sier Zhong Shaim, professor i informatikk ved Yale University, i en pressemelding.
- Det utgjør et betydelig skritt i retning av å bygge fullt verifisert systemprogramvare med relevante driftssikkerhet-garantier, sier Shaim.
Nicta skal om kort til overføre åndsretten for teknikkene til den tilknyttede selskapet Open Kernel Labs (OK Labs), som blant annet tilbyr hypervisor-programvare for integrerte enheter. Denne skal være i bruk store mengder konsumentelektronikk i dag, blant annet mange avanserte mobiltelefoner.
- Arbeidet tilbyr avgjørende bevis på at feilfri programvare er mulig, og at intet mindre bør bli ansett som akseptabelt på områder hvor kritiske aktiva står på spill, sier Gernot Heiser, teknologisjef ved OK Labs og leder for ERTOS-gruppen ved Nicta, i en pressemelding.
Forskerne skal legge fram en vitenskapelig rapport om forskningen i forbindelse med ACM Symposium on Operating Systems Principles i oktober.
Flere detaljer om forskningsprosjektet finnes her.
Les også:
- [10.01.2008] Skal finne flere feil i åpen kildekode
- [05.04.2006] Stor innsats for å fjerne programvarefeil
