General Dynamics C4 Systems and NICTA are pleased to announce the open sourcing of seL4, the world’s first operating-system kernel with an end-to-end proof of implementation correctness and security enforcement. It is still the world’s most highly-assured OS.
And here’s the code.
They even have the specs and proofs.
It was stupid closing sel4 in the first place. I think it would have been way more successful if it was open in development and everything and we would have something interesting coming out of it.
Proofs (in Isabelle proof language) are in a separate repository: https://github.com/seL4/l4v
A friend of mine did his dissertation on software verification, so I learned a decent amount about it. I’ve still always been confused about how you could capture all of the machine-dependent semantics and also construct logical specifications that are NARROW enough. Plus, if the automated solver can’t interpret the code directly (but has to rely on someone hand-translating code to a second set of logical transformations), and you cannot completely verify the compiler, then the proof is only as good as the weakest link. Perhaps someone out there is doing proofs based on the machine language code generated.
Also, my focus is computer architecture (I also have a digital circuit design background), and I focused on reliability problems. So I find it a little scary to fully trust the hardware to follow its specifications. Even if you don’t have timing or soft errors to deal with, hardware can have unexposed bugs.
So, I always had trouble accepting these formal proofs as anything other than “probably approximately correctâ€, not rigorous mathematical proofs. It’s more like a legal proof than a logical proof.
The Repository is actually quite nice in what they describe and how they put the limits of what they have done – or certify.
Sadly I am not finding to what Common Criteria level rating they have achieved. Linux has achieved the highest commercial OS level, along with Trusted Solaris – only way to go higher is to have custom software design.
May be L4 was designed for those higher levels; but now that they are Open source, that might compromise that rating…don’t know. I just find their whole “most highly-assured OS” thing to be a little far fetched.
In formal verification, you need to trust small things such as the core of proof assistant and user-defined programming language semantics (a.k.a “translation from programming language to standard math”, including machine model) and finally what property you want to prove. Once you are convinced these are satisfactorily defined, the actual proof is rigorously verified by proof assistant. Usually the compromisation happens in the machine model and the target property by simplifying them.
too late…