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.
Or do you mean the "Guru Meditation Error"?
Visit the Arcade Restoration Workshop @ http://www.arcaderestoration.com
> 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.
The missing word is formal.
They use a formal specification, which is then formally verified.
The overhead? It took something like 5 years for a 10,000 line program. The benefit is if the specification is right, the program should be right.
Other questions are answered in the FAQ linked in the summary and this page.
Honywell SCOMP Early 1980s Was intended to me a secure front-end to Multics.
Verified by NSA et all as part of the first Orange-book A1 level certification.
For the time it was a magnificent bit of work.
It only means it meets the spec, not that the spec is correct ...
It does not mean that the faulty or erratic hardware cannot crash the system
It does not mean that other programs cannot crash and lose your data ...
It does not mean that buggy device drivers can make your system unusable
It does not mean that the system is perfect, only that it will always do what it is supposed to ... which may not be what you want ...
Puteulanus fenestra mortis
Formal proofs are not unit tests. Unit tests test that certain values work correctly. Formal proofs show that the code works to the specification in all cases (modulo errors in the proof, of course). They of course cannot find bugs in the specification (which unit tests might, if they test what you thought the specification said, instead of what the specification really said).
The Tao of math: The numbers you can count are not the real numbers.
You're conflating two different concepts. Common Criteria Evaluation Assurance Level focuses on security while this test focuses on complete mathematical provability IOW, can it be mathematically proven that the kernel meets all of its specifications and that the compiled kernel is exactly what was specified in the source code? CC EAL focuses only on security aspects.
Furthermore, a system that was specified as being completely secure[1] would, in theory, be equivalent to a EAL 7, not merely "6+".
[1] I mean this only in a hypothetical sense since I don't believe it is even possible to specify a system that is completely impenetrable, let alone implement one. But then, that's because I subscribe to the theory of information security that says a completely secure system is impossible, therefore we must use multiple compensating ocntrols that get us to a 'virtually impenetrable' state, tuned to prevent the most likely types of attacks (cheap) vs. the possibility of someone building a multi-billion dollar super cluster to break the security.
My blog