World's First Formally-Proven OS Kernel 517
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.
spec? (Score:5, Insightful)
but is the spec useable ? bugfree ?
Thank goodness (Score:2, Insightful)
Apps running on top will crash... so (Score:3, Insightful)
Knuth on proven correct: (Score:5, Insightful)
"Beware of bugs in the above code. I have only proven it correct, not tested it."
Empty promises... (Score:1, Insightful)
You can't assure we'd never see a kernel fault again even using this. Most faults on most platforms are caused by hardware faults that even a formally proven OS cannot prevent. They also claim that something entirely on spec' has no bugs, which of course is laughable to anyone that has done any length of development. You just cannot account for everything that could happen within a complex system with maybe thousands of independant components.
Further more they claim in the article that software faults have caused plane crashes, when? Off the top of my head I cannot name a single instance when a software fault caused a plane crash (and yes, that includes the recent Air France crash).
Re:Thank goodness (Score:2, Insightful)
As opposed to programming languages that aren't logic-based? What separates Haskell, Ocaml, Lisp, Scheme, etc. from others is that they are functional programming languages, as opposed to imperative-based languages like C.
Both use logic, just in different ways.
Re:Thank goodness (Score:4, Insightful)
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!
Proven? (Score:5, Insightful)
Re:Godel's Incompleteness Theorem? (Score:5, Insightful)
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.
Re:Provable? (Score:5, Insightful)
I thought any sufficiently complex system was impossible to prove correct.
Then obviously this OS is not sufficiently complex.
Re:spec? (Score:4, Insightful)
Wish I had mod points (Score:3, Insightful)
This is something that people who bang on about formal proofs conveniently forget - all it does is move the bugs from the source code to the formal specification. And if the spec is detailed enough to be useful it effectively becomes code anyway so you might just as well write the actual code and debug *that* instead.
Re:Apps running on top will crash... so (Score:5, Insightful)
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.
Not very useful... (Score:2, Insightful)
In addition to what's already been pointed out about formal vs. informal specifications,
1. Running Linux on top of this is no more safe than running Linux directly on the hardware--it's Linux that crashes (though not very often!)
2. Running this on a CPU that has not been formally proven is nearly useless because only part of the system has been proven, which results in an overall system that is unproven.
Good News and Bad News (Score:5, Insightful)
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.
Re:Empty promises... (Score:5, Insightful)
Most faults on most platforms are caused by hardware faults
bullshit.
Re:Thank goodness (Score:3, Insightful)
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?
Re:Thank goodness (Score:3, Insightful)
You mean they aren't all tested like this? (Score:5, Insightful)
As someone who does not work in IT, count me as surprised that not all OSes are tested this rigorously.
Re:Thank goodness (Score:1, Insightful)
What separates Haskell, Ocaml, Lisp, Scheme, etc. from others is that they are functional programming languages, as opposed to imperative-based languages like C.
And all (pure) functional lanuages are equivalent by a very well-known and understood isomorphism (Curry-Howard) to a deductive logic system. C and other imperative languages afford no known similar isomorphism (indeed, it can be proven that such a thing can't possibly exist).
Both use logic, just in different ways.
Not at all. It's not about "using" logic -- it's about programs being equivalent to logical proofs. This is demonstrable with functional languages. Absolutely not so with imperative ones.
Re:World's First Formally-Proven OS Kernel - NOT (Score:3, Insightful)
Re:Wish I had mod points (Score:3, Insightful)
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.
Re:spec? (Score:1, Insightful)
Re:Thank goodness (Score:4, Insightful)
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).
Re:You mean they aren't all tested like this? (Score:3, Insightful)
Linux has more than ten million lines of code. Given that they needed 5 years for 12 persons to verify ten thousand lines of code, this means verifying the Linux kernel would give an estimated cost of 60,000 man-years. So even if they got a thousand people doing nothing else but verifying the Linux kernel, it would take then 60 years to finish.
NOT TRUE: Remeber Dijkstra & THE? (Score:2, Insightful)
I daresay the folks who have made this recent excellent achievement are likely well aware of THE, and therefore are being specious in claiming to be the world's first at doing this.
Re:Wish I had mod points (Score:1, Insightful)
Is this really true?
Here's a semi-formal (easily formalizable) specification of the function "sort":
For all lists L, for all x,y in sort(L), ( if x <= y then index(x, sort(L)) <= index(y, sort(L)) )
Is this an implementation of the function sort?
Re:Wish I had mod points (Score:3, Insightful)
I don't thinks that's fair: the spec. just says *what* properties the system should have; the implementation says *how* those properties are provided. Where you can do it, denotational semantics (the spec.) let you say a lot more than you can with operational semantics (the code).
Of course, your argument also suffers from circularity: to debug code you have to have a spec. in the first place to tell you when the implementation is doing the wrong thing.
Re:Thank goodness (Score:3, Insightful)
Re:You mean they aren't all tested like this? (Score:3, Insightful)
That more like "not only doesn't work in IT, but doesn't know of or understand the theory". No slam, just the facts.
Seriously, the reason all OSes aren't tested this vigorously is that the time/amount of work needed to do so rises exponentially with the size/complexity of the OS. Not only does that imply the OS would take years to bring to market, but also that said OS would incredibly expensive. Worse yet, after all that time and expense, all you've actually proven is that your running code matches your specification - you're protected against errors arising from faulty programming, but not from errors arising from conceptual errors in the spec or from incorrect algorithms embedded in the spec.
Re:Wish I had mod points (Score:1, Insightful)
Correct!
Wrong! The whole point of the spec is that it can be formally checked for bugs. You can prove that the spec no longer contains buffer overflow vulnerabilities, and be sure the code matches it. If all you're doing is hacking on code, you can't prove anything.
Re:Empty promises... (Score:2, Insightful)
Re:Thank goodness (Score:3, Insightful)
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.
Re:spec? (Score:4, Insightful)
If you pass the customer a mix of water, flour, yeast, eggs and sugar and the customer says "That's not cake, it's not acceptable".
And you then say - "But we meet the cake spec we agreed on, so by that definition it's cake, you have to pay us".
Sure you can go sue the customer and force them to pay you the full sum, but unless most other people agree the customer has just been way too fussy, you might have fewer customers in the future.
Re:The Amiga Hand? (Score:5, Insightful)
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.
Re:Empty promises... (Score:4, Insightful)
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.
Re:Thank goodness (Score:3, Insightful)
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 [informationweek.com]
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.
Re:Who proved the proof-checker? (Score:3, Insightful)
If he were being honest, he would say that recursion is a just convoluted, unnecessarily confusing method of doing iteration
Some would say that iteration is just a convoluted, unnecessarily confusing method of doing recursion.
For example, try iterating over all the nodes in a tree without using recursion. It's doable, but more complicated and error-prone than the recursive method.