Slashdot Mirror

← Back to Stories (view on slashdot.org)

World's First Formally-Proven OS Kernel

Posted by Soulskill on from the wait-for-it dept.

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.

3 of 517 comments (clear)

  1. Re:spec? by Anonymous Coward · · Score: -1, Troll

    The spec is written in C, a Linux language, and as such is inherently untrustworthy. This becomes the weak point in the chain, from which the rest of their theory collapses; the fact that Isabelle can prove a faulty system secure by way of a faulty spec shows nothing. Also, the fact that they are using a functional language like Haskell is pure smoke and mirrors.

  2. Re:The Amiga Hand? by Dog-Cow · · Score: -1, Troll

    Obviously the mods didn't read the article either, or you would have been modded redundant. Or simply stupid.

  3. Re:Thank goodness by Desler · · Score: -1, Troll

    Name the logic that C is based on, then.

    There's this new thing called boolean logic. I suggest you read up on it some time.