World's First Formally-Proven OS Kernel

An anonymous reader writes "Operating systems usually have bugs — the 'blue screen of death,' the Amiga Hand, and so forth are known by almost everyone. NICTA's team of researchers has managed to prove that a particular OS kernel is guaranteed to meet its specification. It is fully, formally verified, and as such it exceeds the Common Criteria's highest level of assurance. The researchers used an executable specification written in Haskell, C code that mapped to Haskell, and the Isabelle theorem prover to generate a machine-checked proof that the C code in the kernel matches the executable and the formal specification of the system." Does it run Linux? "We're pleased to say that it does. Presently, we have a para-virtualized version of Linux running on top of the (unverified) x86 port of seL4. There are plans to port Linux to the verified ARM version of seL4 as well." Further technical details are available from NICTA's website.

Comments

Sounds like automated unit test generation to me

[Anonymous Coward]

Most large scale commercial software that is worth anything has massive batches of automated unit and functional tests applied to it - How does this differ? Are they automatically generating their "formal proof" code (unit tests I assume). If so, how do the automatically generated tests stack up against manually generated versions? I would imagine said tests can catch a variety of bugs, but as regards insisting that a program has been verified "bug free" - I will believe it when I see it.

The words

[AP31R0N]

KLAATU!
BARADA!
NICTA!