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.

4 of 517 comments (clear)

  1. Amiga Hand? by ArcadeNut · · Score: 4, Informative

    Or do you mean the "Guru Meditation Error"?

    --
    Visit the Arcade Restoration Workshop @ http://www.arcaderestoration.com
  2. Re:Apps running on top will crash... so by John+Hasler · · Score: 5, Informative

    > Even if we have a perfect kernel, it won't insulate us from bugs in the
    > software running on top of that kernel, so do we really gain much?

    Since a kernel crash kills all your applications and background processes, kills your network connection, requires you to reboot, and can scribble anywhere on the disk, yes.

    --
    Warning: this article may contain humor, sarcasm, parody, and perhaps even irony. Read at your own risk.
  3. Re:The Amiga Hand? by Anonymous Coward · · Score: 5, Informative

    The missing word is formal.

    They use a formal specification, which is then formally verified.

    The overhead? It took something like 5 years for a 10,000 line program. The benefit is if the specification is right, the program should be right.

    Other questions are answered in the FAQ linked in the summary and this page.

  4. Re:spec? by JasterBobaMereel · · Score: 5, Informative

    It only means it meets the spec, not that the spec is correct ...

    It does not mean that the faulty or erratic hardware cannot crash the system

    It does not mean that other programs cannot crash and lose your data ...

    It does not mean that buggy device drivers can make your system unusable

    It does not mean that the system is perfect, only that it will always do what it is supposed to ... which may not be what you want ...

    --
    Puteulanus fenestra mortis