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.

14 of 517 comments (clear)

  1. Re:Yeah right by oji-sama · · Score: 5, Funny

    It's not a bug, it's a formally proved feature ^.^

    --
    It is what it is.
  2. Give me six lines of code... by Joce640k · · Score: 4, Funny

    "If you give me six lines of code written by the most diligent of programmers, I will surely find enough in them to crash the OS" - Cardinal Ritchielieu

    --
    No sig today...
    1. Re:Give me six lines of code... by Telecommando · · Score: 5, Funny

      Every program contains at least one bug, and can be shortened by at least
      one instruction. By induction, every program can be reduced to a single
      instruction which doesn't work. /old, I know.

      --
      Beta sux! Join the Slashcott! http://hardware.slashdot.org/comments.pl?sid=4760465&cid=46173047
    2. Re:Give me six lines of code... by ranulf · · Score: 4, Funny
      > By induction, every program can be reduced to a single instruction which doesn't work.

      HACF?

    3. Re:Give me six lines of code... by Anonymous Coward · · Score: 5, Funny

      /*
        *
        *
        *
        *
        */

  3. Then a driver blows it all up.. by tjstork · · Score: 4, Funny

    Suddenly after that, the proven kernel will be brought to its knees when someone adds a driver for an old graphics card.

    --
    This is my sig.
  4. But... by TheDarkMaster · · Score: 2, Funny

    ... we will lost all the fun for Blue Screens and Kernel Panics!

    --
    Religion: The greatest weapon of mass destruction of all time
  5. Who proved the proof-checker? by Dr.+Manhattan · · Score: 3, Funny

    Recursion (n): see recursion.

    --
    PHEM - party like it's 1997-2003!
  6. Re:spec? by Anonymous Coward · · Score: 1, Funny

    It doesn't really even fit "language" either.

  7. Re:Thank goodness by Anonymous Coward · · Score: 1, Funny

    you should use be more accurate in your use of language

    Indeed :)

  8. Re:Empty promises... by Anonymous Coward · · Score: 2, Funny

    Thanks for quoting me.

    You're welcome. (I am not the poster you replied to, but you're full of shit)

  9. Re:The Amiga Hand? by feldicus · · Score: 2, Funny

    "Easier to read" is subjective, and generally only applies if the reader has spent a fairly significant amount of time dealing with the syntax. Coming from years of C/C++/C#/Python, I can tell you that Haskell is about as easy to read as a set of VCR instructions written in Japanese and translated to English by a blind Venezuelan with Carpal Tunnel Syndrome.

  10. A truly marvelous by autophile · · Score: 4, Funny

    I have written a truly marvelous bug-free operating system, however there is not enough space on this disk to include it here.

    --
    Towards the Singularity.
  11. Re:spec? by Tanktalus · · Score: 2, Funny

    In your case? I think the second word is "*WHOOSH*".