7500-line seL4 microkernel proven bug-free

[bananas]

Code breakthrough delivers safer computing

25th September 2009

<snip>

Professor Gernot Heiser, the John Lions Chair in Computer Science in the School of Computer Science and Engineering and a senior principal researcher with NICTA, said for the first time a team had been able to prove with mathematical rigour that an operating-system kernel – the code at the heart of any computer or microprocessor – was 100 per cent bug-free and therefore immune to crashes and failures.

<snip>

“A rule of thumb is that reasonably engineered software has about 10 bugs per thousand lines of code, with really high quality software you can get that down to maybe one or three bugs per thousand lines of code,” Professor Heiser said.

<snip>

Verifying the kernel – known as the seL4 microkernel – involved mathematically proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years.

<snip>

“The verification provides conclusive evidence that bug-free software is possible, and in the future, nothing less should be considered acceptable where critical assets are at stake.”

<snip>

[mike_c]

1. it's always reassuring to know that nothing can go wrong...

...(skip) can go wrong..., (skip) can go wrong..., (skip) can go wrong.... :rofl:

[rfranklin]

2. Bill Gates has already claimed the patent....

Now he can Microsoft it into a flawed program with plenty of security problems.

[cliffordu]

3. To go along with Internet Exploder and Outbreak Express.

[drm604]

4. The proof is machine checked.

The proof is machine-checked using the interactive theorem-proving program Isabelle.

Is Isabelle bug free?

[joshcryer]

6. Indeed. It has a simplified logic core, and is considered "correct."

[Warren Stupidity]

5. Hopefully the code proof was more rigorous than the article proofreading.

"proving the correctness of about 7,500 lines of computer code in an project taking an average of six people more than five years."

[phantom power]

7. 7500 lines of code -- small operating sytem.

The fact that just 7500 lines of code took 30 man-years to prove says something about the computational complexity of proving software.

[joshcryer]

8. They had to actually *write* the proof, so it was probably ten times that.

Possibly even more since Issable proofs can become quite convoluted.

[Lithos]

9. Bug Free

Does not mean "quality" All they reaffirmed is that the code does what it says it does, no more no less. If the code says to spam the Internet with your bank account, then they just proved it will do so.


L-