Forskere fører matematisk bevis for sikker styresystemkerne

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.

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.

Tips og korrekturforslag til denne historie sendes til tip@version2.dk
Kommentarer (8)
sortSortér kommentarer
  • Ældste først
  • Nyeste først
  • Bedste først
#5 Torben Mogensen Blogger

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.

  • 0
  • 0
#7 Michael Schade

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.html Under download er der også samlet dokumentation....i pdf for en gangs skyld.

  • 0
  • 0
#8 Anonym

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.

  • 0
  • 0
Log ind eller Opret konto for at kommentere