Forskere fører matematisk bevis for sikker styresystemkerne

18. august 2009 kl. 15:248
En gruppe forskere har lavet en mikrokerne til et styresystem, som de har ført matematisk bevis for er fuldstændig sikker. Kernen kan bruges til indlejrede systemer.
Artiklen er ældre end 30 dage
Manglende links i teksten kan sandsynligvis findes i bunden af artiklen.

En gruppe forskere fra Australien har ført matematisk bevis for, at den mikrokerne til et styresystem, som de har udviklet, er fuldstændig sikker. Ifølge forskerne er det den første bevisligt sikre kerne, som er stor nok til at kunne anvendes i praksis.

»Der har været ført formelle beviser inden for specifikke funktioner for mindre kerner, men det vi gjort, er et generelt bevis for korrekt funktionalitet, og det har aldrig før været gjort for højtydende, praktisk anvendelig software af denne størrelse og kompleksitet,« udtaler chefforsker Gerwin Klein fra det australske it-forskningscenter NICTA ifølge en pressemeddelelse.

Kernen til styresystemet er på 7.500 linjers programkode i programmeringssproget C. Den vil ifølge forskerne kunne bruges som mikrokerne i indlejrede systemer til kritisk udstyr inden for eksempelvis våbenindustrien.

Selve beviset er udført maskinelt ved hjælp af programmet Isabelle, som kan føre beviser for opstillede matematiske teoremer. For at bevise sikkerheden af mikrokernen skulle forskerne føre bevis for 10.000 teoremer, og de formelle beviser fyldte mere end 200.000 linjer.

8 kommentarer.  Hop til debatten
Denne artikel er gratis...

...men det er dyrt at lave god journalistik. Derfor beder vi dig overveje at tegne abonnement på Version2.

Digitaliseringen buldrer derudaf, og it-folkene tegner fremtidens Danmark. Derfor er det vigtigere end nogensinde med et kvalificeret bud på, hvordan it bedst kan være med til at udvikle det danske samfund og erhvervsliv.

Og der har aldrig været mere akut brug for en kritisk vagthund, der råber op, når der tages forkerte it-beslutninger.

Den rolle har Version2 indtaget siden 2006 - og det bliver vi ved med.

Debatten
Log ind eller opret en bruger for at deltage i debatten.
settingsDebatindstillinger
2
18. august 2009 kl. 20:09

"teoremer" plejer vi at kalde "sætninger" på dansk.

3
18. august 2009 kl. 20:35

Var det ikke mere eller mindre det samme Søren Lauesen og Brinch-Hansen gjorde omkring 1970 ?

Poul-Henning

4
19. august 2009 kl. 08:55

Hvad hvis der er en fejl i programmet Isabelle ?

6
19. august 2009 kl. 10:57

De er vel ikke helt dumme, de har da sikkert allerede testet Isabelle med Isabelle.

7
19. august 2009 kl. 11:35

Yep, ligesom at diskutere med sig selv og give sig selv ret ;-)

Hvis beviset skal være så sikkert vil det vel være bedst om Isabelle kunne verificeres i et andet program end sig selv?

Link til Isabelle projektet er her for dem der vil se det selv : http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.htmlUnder download er der også samlet dokumentation....i pdf for en gangs skyld.

8
Indsendt af Anonym (ikke efterprøvet) den tir, 08/25/2009 - 12:04

Det er en meget interessant nyhed og det er spændende hvad det kommer til at betyde for "high-integrity" folket.

Jeg kan ikke lige finde noget information om, hvad kernen tilbyder, men for at få en brugbar kerne skal der faktisk ikke så meget funktionalitet til. Hvis blot Ravenscar profilen kan understøttes http://en.wikipedia.org/wiki/Ravenscar_profile behøver man sådan set ikke mere for at kunne lave deterministiske tidstro systemer.

5
19. august 2009 kl. 09:44

Et bevissystem som Isabelle består af et centralt logisk system, som er meget lille og overordentligt velafprøvet. Uanset, hvad der sker i de andre komponenter, så bliver alle beviser checket af det centrale logiske system, så risikoen for, at der slipper et forkert bevis forbi er ekstremt lav.

En langt større risiko er, at brugerne af Isabelle laver fejl, når de specificerer det sikkerhedskriterie, der skal bevises, så det de får bevis for ikke er det, de troede, de beviste.