Hacker News Reader

Comment by luckydude | Hacker News Reader

"In short, the implementation is proved to be bug-free."

Has any smart person looked at their claims enough to vouch for them?

(Mill team)

They have published details of their formal verification on ACM http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...

They use Isabelle.

So whilst we haven't seen the proof, nor the code, will do have a good idea of what they've done and how they've done it.

Formal verification has been much researched, and its nice to see actual real systems starting to be checked by them. Just the other day I was reading about people doing TLS implementation verification using Coq.

Some discussion by smart people at http://www.eros-os.org/pipermail/cap-talk/2014-June/thread.h... ... probably have to wait til after it is open source end of next month to say.

You can download seL4 binaries and a copy of the specification (190 pages, no proof) here:

http://ssrg.nicta.com.au/software/TS/seL4/

Source: I have worked at NICTA, with the seL4 team, on the seL4 project, I've seen the seL4 source code and am (was?) a primary author of the user manual.

These claims have been peer reviewed in top formal methods and operating systems journals/conferences and have won some very awards doing so.

In short some very smart, and very qualified people can vouch for them.

Comprehensive formal verification of an OS microkernel with complete PDF available for download

http://ssrg.nicta.com.au/publications/nictaabstracts/Klein_A...

It will be interesting to see once it becomes open source.

My favorite story relating to that is john regher compiler testing effort found a bunch of bugs in a research compiler that was proved to be correct.

[Edit]

Not strictly true. As John noted in comment below:

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

actually that story is the opposite of true. John Regher and CSmith fuzzed CompCert and they found no bugs. from the csmith PLDI paper:

"The striking thing about our CompCert results is that the middleend bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task."

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

Sounds interesting -- is there a paper that describes this?

I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here:

http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

My error.

From the paper "Comprehensive formal verification of an OS microkernel": "We still assume correctness of hand- written assembly code, boot code, management of caches, and the hardware"

http://www.nicta.com.au/pub?doc=7371

There's a lot of assuming going on...I'm not saying that what they've done isn't interesting, but as always don't let yourself get carried away.

To be fair. Every operating system assumes these things. At least the seL4 team has made this explicit. Secondly, there is a tiny amount of this code amounting to a few hundred lines of assembly and there are numerous verified hardware projects underway. Furthermore, as time has gone by, many of the original assumptions have been whittled away. This is by far the most robust operating system ever written.

Sure, I agree. There is indeed some work being done in making some of those parts more trustworthy. That being said, it will probably be sometime before that technology is usable by the average person. I'm really interested in seeing what they release.

Reply on news.ycombinator.com