Arbejder mod bug-fri, sikker software

Forskere fra NICTA (National ICT Australia), Australiens center for fremragende informations- og kommunikationsteknologi, forsøger at fjerne fejl fra softwaren:

"Næsten hvert papir om formel verifikation starter med den iagttagelse af, at softwarekompleksiteten øges, at dette fører til fejl, og at dette er et problem for mission og sikkerhedskritisk software. Vi er enige om det, som de fleste gør."

Min første tanke: Ingen måde. Hvordan kan du eliminere hver eneste fejl? Nogle af de mere komplekse softwarepakker skal mindst have en zillion kodelinjer.

NICTA-folk er godt klar over kompleksiteten. Derfor fokuserer de på små indlejrede systemsoftware til at begynde med.

Som biler

Hver gang min far ringer til et computerproblem påpeger han, at det er kriminelt, hvordan vi accepterer buggy-software: "Det vil være en kold dag i helvede, før jeg køber en sådan bil."

Spol frem til et nyligt telefonopkald fra min far. Jeg vidste ikke, om jeg skulle grine eller græde. Hans bil blev tilbagekaldt for en softwareopdatering.

NICTA's søgen

NICTA-forskere nævnte:

"Det behøver ikke være sådan. Din virksomhed igangsætter en ny salgssoftware .... Du skriver i en kontrakt nøjagtigt, hvad softwaren skal gøre.

Og så - det gør det. Altid. Og udviklerne kan bevise det for dig - med et faktisk matematisk maskinkontrolleret bevis. "

Lyder for godt til at være sandt, ikke sandt? Stadig fremsætter akademikere ikke nogen underbyggede påstande. Så hvad har NICTA-teammedlemmerne deres kollektive ærmer op? Jeg kontaktede NICTA, og Dr. June Andronick meldte sig frivilligt til at forklare, hvad de havde lært.

Kassner : Hvordan blev du først interesseret i kodeverifikation? Og er det så skræmmende, som det ser ud til? Andronick : Jeg kommer fra en matematisk baggrund. Jeg begyndte at skrive kode med tankegangen, hvor du tænker over, hvorfor dit program skal opføre sig som du forventer. For eksempel "Hvorfor skal det nøjagtigt afsluttes?"

Jeg fandt formel kodeverifikation en fascinerende måde at kombinere de to verdener på ... at skrive præcist, hvad du forventer af programmet ... og derefter bevise, at det gør det.

Noget af dette er intuitivt: Programmerere har normalt magefølelsen af, hvorfor deres program gør, hvad de vil. Kodeverifikation formaliserer netop denne ræsonnement og får den til at blive maskinkontrolleret og efterlader intet sted for tvivl.

Det lyder måske skræmmende, men det er faktisk meget sjovt og vanedannende. Det er som et spil mellem dig og bevisværktøjet - du prøver at overbevise det, hvorfor du mener, at noget er sandt.

Kassner : Du brugte noget, der hedder seL4-mikrokernel, til at teste dine teorier. Hvorfor valgte du denne kerne? Andronick : Målet med L4.-verificeret projekt, ledet af professor Gerwin Klein, var formelt at verificere seL4, en ny mikrokernel designet af Dr. Kevin Elphinstone. Det er det første skridt hen imod den langsigtede vision for vores gruppe, ledet af professor Gernot Heiser, til at producere virkelig pålidelig software, som du kan yde en stærk garanti om dens sikkerhed, sikkerhed og pålidelighed.

Valget om først at tackle kernen er drevet af en hovedårsag: Det er den mest kritiske del af systemet, der ligger mellem hardware og resten af ​​softwaren. Det har fuld adgang til alle ressourcer og kontrollerer, hvad anden software kan få adgang til.

Enhver opførsel af systemet vil stole på alle aspekter af kernefunktionalitet. Så enhver garanti om systemet bliver nødt til at starte med, at kernen fungerer korrekt.

Da der ikke er nogen beskyttelse mod fejl, der forekommer i kernen, kan enhver bug der potentielt forårsage vilkårlig skade. Begrebet mikrokernel kommer fra at reducere mængden af ​​sådan en kritisk kode til et minimum, reducere den "betroede computerbase".

Resultatet af projektet var et formelt bevis på seL4s funktionelle korrekthed . Dette betyder, at kernen under antagelsen af ​​beviset aldrig kan gå ned eller på anden måde opføre sig uventet.

Dette var det første formelle bevis for funktionel korrekthed af en operativsystemkerne til generelle formål og mere generelt for enhver reel anvendelse af betydelig størrelse.

Kassner : 8700 linjer med C og 600 linjer samler synes som en masse kode at kontrollere. Er det, hvad nedenstående lysbillede afbilder? Kan du forklare, hvad vi ser på?

Andronick: Dette billede viser seL4's såkaldte funktionsopkaldsgraf. Hver C-funktion i kernen er en prik. Hvis funktion A kalder funktion B, er der en pil fra A til B.

Grafen viser, at seL4 er meget kompleks software med stærkt sammenkoblede dele. Dette er typisk for ydelsesoptimerede mikrokerner.

Veludviklet applikationsniveau-software ville have grupper eller øer med stærkt beslægtede prikker forbundet med et lille antal pile, der bygger mellem øerne.

Kassner : Du bruger udtrykkene formel verifikation og funktionel korrekthed. Kunne du beskrive, hvad de hver især betyder, og hvilke roller de spiller? Andronick : Formel verifikation henviser til anvendelse af matematiske bevisteknikker til at etablere egenskaber om programmer. Det kan ikke kun dække alle kodelinjer eller alle beslutninger i et program, men alle mulige opførsler til alle mulige input.

Denne udtømmende dækning af alle mulige scenarier er det, der adskiller det fra testning, der kun kan finde bugs, ikke bevise fraværet af bugs.

Funktionel korrekthed betyder, at kernen opfører sig som forventet i dens specifikation. Denne egenskab er stærkere og mere præcis end hvad automatiserede teknikker som modelkontrol eller statisk analyse kan opnå.

Vi analyserer ikke kun specifikke aspekter af kernen, såsom sikker udførelse, men giver også en fuld specifikation og bevis for kernens nøjagtige opførsel.

Den tilgang, vi bruger, er en interaktiv teorem, der beviser . Det kræver menneskelig indgriben og kreativitet for at konstruere og vejlede beviset, men har fordelen, at det ikke er begrænset til specifikke egenskaber eller fi nite, gennemførlige tilstandsrum.

Kassner : Jeg forstår nu, hvad du leder efter. Kunne du give et kort overblik over, hvordan du prøver at finde problemer? Andronick : Et problem registreres, når koden ikke opfører sig som specifikationen foreskriver.

Processen starter med at skrive en formel specifikation af, hvad kernen skal gøre. For eksempel kan du kræve, at en sorteringsfunktion returnerer en liste, der er sorteret, med de samme elementer end inputlisten. Koden beskriver, hvordan denne funktionalitet implementeres som valg af en sorteringsalgoritme.

Derefter skal du bevise, at resultatet af funktionen altid vil opfylde specifikationskravet. Igen er nøgledifferentieringen til testning, at vi resonnerer om alle mulige input. Hvis specifikationen ikke gælder for nogle input, vil beviset afsløre den. Fejlen rettes, og bevisforsøget genoptages. Når beviset er afsluttet, ved du , at der ikke er nogen implementeringsfejl tilbage.

Kassner : Hvad er det næste trin i bekræftelsesprocessen? Kan denne procedure bruges til at teste computer-operativsystemer, vi er vant til? Andronick : Den nøjagtige samme fremgangsmåde skaleres ikke til systemer, der indeholder en million kodelinjer, såsom moderne operativsystemer. Men vi har en plan for store komplekse systemer.

Den første ting, der skal bemærkes, er, at formel verifikation ikke er billig. Vi brugte markant e ff ort på verifikation af ca. 10.000 linjer med kode. Det ser stadig ud til at være omkostningseffektivt og mere ordentligt end andre metoder, der opnår lavere grad af pålidelighed.

Hovedbudskabet er, at sådanne grundige metoder virkelig giver mening i kritiske systemer (medicinsk, bilindustri, forsvar osv.).

Vores tilgang til store kritiske systemer kommer fra den iagttagelse, at i sådanne systemer ikke alle koder er kritiske. F.eks. Har medicinsk udstyr store brugergrænseflader, og fly har underholdningssoftware (Prof. Heiser skrev en relevant blog, der illustrerer behovet for en verificeret kerne, der bruger underholdningssystemer under flyvning som eksempel).

Nøgletanken i vores aktuelle arbejde er at isolere de ikke-kritiske dele fra de kritiske. Dette gøres ved hjælp af seL4 og dens adgangskontrol. Dette gør det muligt for os at bevise, at en fejl i de ikke-kritiske dele ikke kan forhindre, at de kritiske dele opfører sig korrekt. På denne måde kan vi koncentrere verifikationsindsatsen på de kritiske dele af systemet.

Med andre ord viser vi, at formel verifikation af funktionel korrekthed praktisk talt kan opnås for OS-mikrokerner, og vi arbejder nu på at bruge dette pålidelige fundament til at give stærke garantier for store kritiske systemer.

Kassner : Sjovt, du skal nævne underholdningssoftware til flyselskaber. Mens de for nylig var røde øjne mod Amsterdam, løb kabinettsfolkene op og ned ad gangene og undskyldte. Underholdningssystemet var nede. ”Det skulle snart ske op.” De sagde: "Kaptajnen genstarter en computer."

Endelige tanker

Mit brændende spørgsmål: "Hvad ellers kontrollerer computeren?" Jeg blev forsikret om, at alt var under kontrol.

© Copyright 2020 | mobilegn.com