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?
Or do you mean the "Guru Meditation Error"?
Visit the Arcade Restoration Workshop @ http://www.arcaderestoration.com
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.
"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...
"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.
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.
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).
Godel's Incompleteness Theorem just say(In this context) that there exists infinite many kernels that are correct but which can not be proven correct. It does not say that no kernel can be proven correct.
So they just happen to write one of the kernels that could be proven.
I thought any sufficiently complex system was impossible to prove correct.
Then obviously this OS is not sufficiently complex.
Yes, it gains you a lot.
Firefox crashing means your userland memory is fucked up and can't be trusted anymore. No problem, kill it, clean it and restart the application.
A kernel crash leads to undefined behaviour on the ring 0 level. You don't want that, it's where root exploits live.
Furthermore, we have a lot of really, really strong kernel-level security extensions, like SELinux, whose only two vulnerable spots are kernel-level exploits and weak security policies. If you can remove one of them, you've done a lot to improve security.
Assorted stuff I do sometimes: Lemuria.org
First off, as an Australian and a nerd, I am very proud.
Now.
Good news: there is now a formally verified microkernel. 8,700 lines of C and 600 odd lines of ARM assembly. Awesome.
Bad news: it took 200,000 lines of manually-generated proof and approximately 25 person-years by PhDs to verify the aforementioned microkernel.
Conclusion: formal verification of software is not going to take off any time soon.
Classical Liberalism: All your base are belong to you.
Most faults on most platforms are caused by hardware faults
bullshit.
As someone who does not work in IT, count me as surprised that not all OSes are tested this rigorously.
Genocide Man -- Life is funny. Death is funnier. Mass murder can be hilarious.
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.