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.

Comments

spec?

[polar red]

but is the spec useable ? bugfree ?

Re:spec?

[jadrian]

To verify the software meets its specification the specification itself must formalised in the theorem prover. This in turn gives you the possibility of proving properties of the spec itself.

Re:spec?

[TheLink]

Exactly. That's why these formal verification stuff is rather useless for most cases I see.

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.

Apps running on top will crash... so

[WiseOwl2001]

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).

Re:Apps running on top will crash... so

[Tom]

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.

Knuth on proven correct:

[John Hasler]

"Beware of bugs in the above code. I have only proven it correct, not tested it."

Re:Thank goodness

[morgan_greywolf]

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

[johannesg]

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?

[mseeger]

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).

Re:Godel's Incompleteness Theorem?

[TheSunborn]

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?

[jamesh]

I thought any sufficiently complex system was impossible to prove correct.

Then obviously this OS is not sufficiently complex.

Wish I had mod points

[Viol8]

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:Wish I had mod points

[Anonymous Coward]

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:Wish I had mod points

[ralphbecket]

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.

Not very useful...

[jamesivie]

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

[Jacques Chester]

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...

[ezzzD55J]

Most faults on most platforms are caused by hardware faults

bullshit.

Re:Thank goodness

[Anonymous Coward]

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

[Idiot with a gun]

It's a paradigm, technically. Although Haskell isn't a logic language, it's functional. Prolog is logical, and nigh useless for most applications.

You mean they aren't all tested like this?

[Remus Shepherd]

As someone who does not work in IT, count me as surprised that not all OSes are tested this rigorously.

Re:You mean they aren't all tested like this?

[maxwell demon]

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.

Re:You mean they aren't all tested like this?

[DerekLyons]

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:World's First Formally-Proven OS Kernel - NOT

[TheRaven64]

Thanks, I was surprised by this claim too. I remember hearing back in 2007 about a formally-verified kernel written in Ocaml that some people at Cambridge had written, and they weren't claiming that theirs was the first (although it may have been the first to run on commodity x86 hardware).

Re:Thank goodness

[xaxa]

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).

NOT TRUE: Remeber Dijkstra & THE?

[fortunatus]

In the 1960's Edsger Dijkstra (arguably one the founding fathers of "Computer Science", at least as a university subject) led a group at Eindhoven to develop a multiprocessing OS called "THE". The kernal was formally proven BY HAND .

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:Thank goodness

[arethuza]

While C includes some logical operators based on boolean logic most of the language has no connection whatsoever to anything that looks like formal logic. Compare this to Prolog - which has a much closer mapping to predicate calculus or pure functional languages which have a very good mapping to lambda calculus.

Re:Empty promises...

[JKDguy82]

You gotta love how a single word "bullshit" response gets modded "Insightful".

Re:Thank goodness

[kamatsu]

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:The Amiga Hand?

[Chris Mattern]

The benefit is if the specification is right, the program should be right.

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...

[Wraithlyn]

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

[ioshhdflwuegfh]

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.

Re:Who proved the proof-checker?

[Jeremi]

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.