Af Torben B. Sørensen, 11/10/16
Artiklen blev oprindeligt publiceret den 18/8/2009
Forskere har bevist matematisk, at et operativsystem fungerer i henhold til specifikationerne og uden fejl.Tidligere har man ført bevis for, at mindre stykker software opfylder krav. Men ifølge forskerne fra NICTA (National ICT Australia) er det første gang, at det er lykkedes at føre formelt bevis for et helt operativsystem.
Styresystemet hedder Secure Embedded L4 (seL4). Det er en mikrokerne, som er beregnet til brug i militæret og andre steder, hvor man anvender indlejrede systemer. Hvis den slags systemer fejler, kan det medføre tab af menneskeliv.
"At bevise korrektheden af 7.500 linjer C-kode i et operativsystems kerne er en enestående bedrift. Den skulle efterhånden føre til software, der opfylder krav om pålidelighed, som vi ikke kan forestille os i dag," siger professor Lawrence C. Paulson fra Cambridge Universitys Computer Laboratory.
Forskerne har bevist, at C-programkoden korrekt implementerer den opførsel, der er beskrevet i den abstrakte specifikation af sL4 og ikke mere end det. Som konsekvens mener de, at programmet ikke indeholder bufferoverløb, pointer-fejl, memory-lækager eller aritmetiske overløb.
Bevisførelsen er tjekket med programmet Isabelle.