Forskere fra det australske NICTA, Information and Communications Technology Research Centre of Excellence, har som de første i verden bevist korrektheden af en styresystemkerne.
Forskerne fra NICTA har beskrevet kravene til styresystemkernen i en formaliseret kravspecifikation.
Korrekthedsbeviset betyder, at man kan være sikker på, at selve koden for styresystemkernen overholder kravspecifikationen.
Beviset sikrer med andre ord, at programkoden ikke introducerer fejl eller sideeffekter, der strider imod den oprindelige kravspecifikation.
Når man går fra en kravspecifikation til programkode, kan der normalt i systemudvikling blive introduceret mange fejl i forhold til de oprindelige krav.
Som forskerne selv beskriver det:
"Ideen er, at det er nemmere og hurtigere at specificere hvad du ønsker i specifikationen, fordi sproget er mere udtryksfuldt, og fordi du kan udelade detaljer, som du ikke er interesseret i; specifikationen behøver kun at sige hvad softwaren skal gøre, ikke hvordan det skal gøres."
Stort skridt mod pålidelige styresystemer
En styresystemkerne er det centrale i en computer og korrekthedsbeviset er et stort skridt mod sikre og pålidelige styresystemer.
"Formelle beviser for specifikke egenskaber er blevet udført for mindre kerner, men det, vi har gjort, er et generelt, funktionelt korrekthedbevis, som ikke før er opnået for rigtige højt-performende software af den her kompleksitet og størrelse," forklarer Dr. Gerwin Klein, som leder NICTA's formelle verifikationsforskerhold.
Arbejdet vinder anerkendelse.
"Det er svært at kommentere denne bedrift uden at anvende klicheer. At bevise korrektheden af 7.500 linjers C-kode er en enestående præstation, som vil føre til software af hidtil utænkelig høje standarder for pålidelighed," siger professor i Computational Logic ved Cambridge University, Lawrence C Paulson.
NICTA-forskerne har brugt 20-25 mandeår på at bevise, at implementeringen af Secure Embedded L4 (seL4)-mikrokernen overholder alle specifikationer.
seL4-mikrokernen er en styresystemkerne som er tiltænkt anvendelse i mobiltelefoner, håndholdte computere og andre apparater med brug for et lille og pålideligt styresystem.
Korrekthedsbeviset markerer afslutningen på L4.verified-projektet, som startede for fire år siden.
Usårlig overfor klassiske angreb
Beviset for seL4-korrektheden viser også, at mange almindelige angrebsformer ikke virker på seL4 kernen. Eksempelvis vil kernen ikke kunne blive udsat for buffer- overflows, hvilket ellers er en ofte set angrebsform, hvor hackere forsøger at overtage kontrollen med computere.
"Vores seL4 kerne kan ikke blive ødelagt af den slags angreb," siger Dr. Klein.
"Arbejdet går videre end de sædvanlige check for specifikke fejl," bemærker professor Lawrence C Paulson.
"I stedet for verificerer det fuld overholdelse af systemspecifikationen. Projektet har ikke kun givet en verificeret mikrokerne, men et sæt teknikker som kan anvendes til at udvikle anden verificeret software."
Ikke fejlfri
Selvom det nu er bevist, at implementeringen af seL4 overholder alle specifikationerne, kan forskerne ikke udelukke eventuelle fejl.
Hvis man har glemt at specificere nogle krav i kravspecifikationen, så vil koden heller ikke indeholde funktionalitet, der honorerer de glemte krav, ligesom nogle forkerte krav vil blive afspejlet i koden.
"En kyniker vil nok sige: beviser som det her viser kun, at enhver fejl i specifikationen er blevet præcist implementeret i C. Det er sandt...Men på et tidspunkt må man sige hvad man ønsker (den "abstrakte specifikation") og det er hvad du får."
"Vores bevis viser, at hvis forudsætningerne for beviset holder, så afviger seL4-kernen ikke fra specifikationen. Der kan være uforudsete features i specifikationen og en eller flere af forudsætningerne er måske ikke gældende.
Specielt kan implementeringsdetaljerne under niveauet for C programmeringssproget indeholde ligeså mange eller få defekter som anden software," lyder det på projektets spørgsmål og svar-side
1.200 linjers assembler- og boot-kode er ikke verificeret i seL4. Der er en nærmere beskrivelse af korrekthedsbeviset og antagelserne på projektets website.
Hvornår i mainstream styresystemer?
Selvom NICTA-forskerne nu har vist, at det kan lade sig gøre at bevise korrektheden for styresystemet, den centrale del af en computers software, så vil der formentlig gå lang tid, inden vi ser formelt verificerede styresystemkerner i mainstream styresystemer som Windows, Linux og Mac OSX.
seL4 er nemlig en mikrokerne med kun 8.700 linjers kode, hvorimod Windows og Linux er såkaldte monolitiske kerner, der består af flere millioner linjers kode.
Det vil tage tid at bevise korrektheden for dem.
