Forskere fører matematisk bevis for sikker styresystemkerne
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.
...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.
