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?
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? I guess for mission critical apps the answer could be yes... But for every-day computing?? On my desktop I have more trouble with Firefox crashing than I do the OS! (Yes I run linux).
"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.
People are starting to see the value of this. Also of programming in logic based languages like Haskell, ML etc.
People have seen the value of this since the first days of programming. In fact, the value is so enormous that no one can afford it... And they have just finished proving that first few lines of code they wrote. In another five decades they hope to be able to have Notepad proven and ready to run so you can actually get some work done!
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.
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.
Name the logic that C is based on, then.
C may be "logical" in a colloquial sense. It's not based on a formal logical calculus.
Do you even know what the hell you are talking about?
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.
That this moves the bugs to the formal specification is true, but that therefore you might just as well write the actual code is an invalid derivation. Formal specification languages are designed with the idea that one should be able to reason about them in mind (be it manually or with the help of automatic/interactive theorem proving, model checking). This typically leads to a language in which systems can be expressed on a higher level, because performance issues are not important: the specification does not need to be executed. Due to this higher level and the fact that they are easier to reason about with tool support, it is easier to find a bug in a formal specification than it is in programming language code.
It's a paradigm, technically. Although Haskell isn't a logic language, it's functional. Prolog is logical, and nigh useless for most applications.
No, it's just more difficult to write the program for most applications.
IMO, it's because it's more difficult to precisely articulate the problem and method (for Prolog) than to work through the solution (for an imperative language).
Dude, can C's types be reasoned by formal inference? No. Hence, C does not follow typed logical calculus.
C doesn't follow boolean logic either, actually, it just maps to assembly instructions. The best thing you could do to reason about C is to use Dijkstra's proof method which is impractical in a large scale and easy to screw up.
We'll have to prove the specification does what we want, then. Of course, then we have to make sure our conception of what we want is right...
Personally, I think it's elephants all the way down.
The context of your full original post does not change the fact that you claim most faults are caused by hardware, which is the specific point he was disputing.
If you have something to strengthen your claim (from your original "context" or otherwise), present it. Otherwise, complaining about being quoted "out of context" is just rhetorical posturing.
"Mind, as manifested by the capacity to make choices, is to some extent present in every electron." -Freeman Dyson
You know the funny thing about this whole discussion is that the OS linked to in the article is not the first. Integrity from Green Hills Software was proven correct a while ago. It is popular for safety critical stuff like flight controls for airplanes and is one of the dominant players in that niche. :)
http://www.informationweek.com/blog/main/archives/2008/11/green_hills_sof.html
And what is truly amusing about following this argument, is that Integrity is written in C.
Although I can see that you're amused, what you're saying is false: Integrity is not formally proven correct, it only has some amusing but mathematically irrelevant industry certificate.