Slashdot Mirror
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.
but is the spec useable ? bugfree ?
Yes, I'm left. You have a problem with that?
The Amiga Hand was the boot screen, not an error screen. You're thinking of the famous Guru Meditation.
Besides, who says that the Amiga kernel did _not_ meet the specifications? Have you read them? Does it mention "crash free" anywhere?
The Haskell code is called a "specfication", but if it is Haskell code, surely it should count as a _program_ already? How can you prove that that program is bug-free? How about conceptual bugs?
Was the toolchain verified? How about the hardware on which it runs?
What overhead does this approach have? Are the benefits worth it?
I'm not saying this is all bullshit, but it looks like me that they are pointing to one program, calling it a "specification", and then demonstrating machine translation / verification to a similar program. I'm not sure if I buy that methodology.
It's not a bug, it's a formally proved feature ^.^
It is what it is.
"Beware of bugs in the above code. I have only proven it correct, not tested it."
Warning: this article may contain humor, sarcasm, parody, and perhaps even irony. Read at your own risk.
> 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.
Every program contains at least one bug, and can be shortened by at least /old, I know.
one instruction. By induction, every program can be reduced to a single
instruction which doesn't work.
Beta sux! Join the Slashcott! http://hardware.slashdot.org/comments.pl?sid=4760465&cid=46173047
There is an old corollary that says, you cannot get from the informal to the formal by formal means. All they have proven is, that two specifications contain the same bugs. Both specification were formal (Haskell, C). This is the same as having Perl and Python code and you to prove they implement the same functionality. Neither is a proof, it is bug free (informal definition of bug, not if a bug is specified it isn't a bug).
I thought any sufficiently complex system was impossible to prove correct.
Then obviously this OS is not sufficiently complex.
Most faults on most platforms are caused by hardware faults
bullshit.
/*
*
*
*
*
*/