There is an announcement of a first formal proof of a kernel written in C

However just see those figures:
“The outcome is the result of four years’ research by Dr Klein’s team of 12 NICTA researchers, NICTA/UNSW PhD students and UNSW contributed staff. They have successfully verified 7,500 lines of C code and proved over 10,000 intermediate theorems in over 200,000 lines of formal proof. The proof is machine-checked using the interactive theorem-proving program Isabelle. It is one of the largest machine-checked proofs ever done.”

Four years for “just 7500 lines of C and just see what they’ve done for the proofs, (who the hell will verify 200 000 lines of formals proofs) however if that is what it takes then we have a ratio of
roughly 1/200. That means for a code base of around 1 000 000 lines we would have to accept 200 000 000 lines of proof, not reagarding the exponential grows of proababilty. But let us just assume a linear scale than this would take around 133,33 years to build the proof. Now that’s really quite a time if we just let IT to be around 60 years or so old…..

Just another point:
The proof is machine-checked using the interactive theorem-proving program Isabelle.

So who guarantees that Isabelle does get it right?

And one other figure let us assume that one does can write around 30 Lines of code an hour, than one needs around 7500 / 30 250 hours to write 7500 lines. That just a bit below 6 weeks. Let us assume 200 EUR for payments then this would be around 200 * 250 = 50 000. Now the proof has taken 4 years let us assume one person could have done it in that time so we have around 250 * 8 = 2000 hours a year so for four years that arou around 8000 hours now let’s do one other calculation, the “proof” has costed 8000 * 200 = 1 600 000 EUR.

Just imagine, you spend that much money on the assumption you get it all right, and then just see what they wrote:
“The proof also shows that many kinds of common attacks will not work on the seL4 kernel. For instance, the microkernel is impervious to buffer overflows, a common form of software attack where hackers take control of programs by injecting malicious code. “Our seL4 kernel cannot be subverted by this kind of attack,” says Dr Klein.”

How cost effective would it have been to use a language which does not even permit this buffer overflows and just see how expensive those buffer overflows really are….

This is an amazing number.

However the conclusions are very doubtful:
“The NICTA team has achieved a landmark result which will change the game for security-
and safety-critical software,” said OK Labs’ Chief Technology Officer and Leader of NICTA’s
ERTOS Group, Professor Gernot Heiser. “It 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. OK Labs looks forward to taking this groundbreaking research to
market.”

This has simply a touch of lying. The conculsion is simply wrong, what will happen if the program still has some bug? What will they tell us then, “well sorry but we have a fault in lined 179333 of our “formal proof”.”

Another point about the “kernel”
“The evolution of seL4 is continuing within NICTA, and it is the basis of ongoing research activities here at NICTA. However, it is also the subject of commercialisation activities, and thus is currently proprietary. We are endeavouring to release seL4 in the future, but the time-line and exact nature of the release is yet to be decided. Stay tuned for further info.”
see here:http://ertos.nicta.com.au/research/sel4/

So the kernel is not available at all and sorry, it has not run under “real” scenarios. And it was written by the same group. Sorry, that has a bit more than just a small smell.

Let’s see if the stuff ever will hit the market and how it will “survive” in the wild. Maybe we just read about it in a few other articles but never see it in reality….