Correct OS kernel? Proof? Done!
Gerwin Klein · 2009
completed and in this article I’m showing what we have proved and what that means for security. The seL4 microkernel: Correct! The basic idea goes back to the 1970s: since then people have been trying to formally verify operating systems [4,10]. It’s the obvious place to start when you are serious about meaningful assurance for critical systems. The idea for formal verification is that programs are just mathematics in the end. And if you want to show beyond doubt that something is true in mathematics, you prove it. If you want to be sure that the proof is right, you do it fully formally so that it can be machine-checked. It was clear early on that this is possible in principle, but enthusiasm ebbed off after an initial flurry of activity around the late ’70s and early ’80s. Mathematical semantics for real programming languages were not developed far enough, machine support for theorem proving was only starting to appear, and the whole problem seemed infeasible for any real program of interesting size. Full formal program verification was like controlled fusion power: about 30 years of research in the future. In contrast to controlled fusion, 30 years later things have changed. With the formal verification