L4.Verified project - A formally correct OS kernel.

This sounds very impressive, but if you think about it they've really solved a very uninteresting problem. What they have done is essentially layered a sound type system on top of C, and run a particular C program (the kernel) through this type checker. (It's a little more sophisticated than that, but that's the gist of it.) You could accomplish exactly the same thing by simply writing the code in a language like Haskell or Lisp that had a sound type system built in as part of its design. Haskell and Lisp programs have all the same properties as the L4 kernel: they never overflow their buffers, never dereference null pointers, never leak memory, and never have arithmetic overflows. But when you think about it that way, it's a much less impressive result. The only thing that makes this interesting at all is that they wrote their code in C. This is rather like climbing a mountain carrying a 500lb weight. Yes, in a sense it's impressive, but it's a lot easier to scale the mountain if you just don't pick up that 500lb weight to begin with.

The following does not happen in this kernel.

Quoted Verbatim

* Buffer overflows: buffer overflows are a classic security attack against operating systems, trying to make the software crash or even to inject malicious code into the cycle. We have proved that no such attack can be successful on seL4.

* Null pointer dereferences: null pointer dereferences are another common issue in the C programming language. In applications they tend to lead to strange error messages and lost data. In operating systems they will usually crash the whole system. They do not occur in seL4.

Pointer errors in general: in C it is possible to accidentally use a pointer to the wrong type of data. This is a common programming error. It does not happen in the seL4 kernel.

* Memory leaks: memory leaks occur when memory is requested, but never given back. The other direction is even worse: memory could be given back, even though it is still in use. Neither of these can happen in seL4.

* Arithmetic overflows and exceptions: humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4.

Previous discussion: http://news.ycombinator.com/item?id=760547

Impressed at how well they understood the limitations of doing this.