L4.Verified project - A formally correct OS kernel.

http://ertos.nicta.com.au/research/l4.verified/proof.pml

by socratees • 17 years ago

9 6 17 years ago

ertos.nicta.com.au

socratees• 17 years ago

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.

lisper2• 17 years ago

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.

ars2• 17 years ago

You need to look at it more closely.

They used Haskell as part of the formal definition. And they proved more than just those obvious things.

lisper2• 17 years ago

Yes, I know. I don't want to diminish their accomplishment. They did in fact scale the mountain. My point is only that they made it harder on themselves than they had to by choosing to focus their efforts on a C program. They could have accomplished exactly the same thing with a lot less effort by simply writing their code in Haskell (or Lisp or Qi) to begin with. But then the headline would have been "We wrote an OS kernel in Haskell" which would not have sounded nearly as impressive.

ars2• 17 years ago

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

wmf• 17 years ago

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

L4.Verified project - A formally correct OS kernel.

Related Stories