Correct OS Kernel? Proof? Done!

Gerwin Klein

Abstract

Two years ago Gernot Heiser demanded in this venue Your System is Secure? Prove it! He also mentioned the L4.verified project at NICTA which is doing just that. This proof is now completed and in this article I'm showing what we have proved and what that means for security.

Online Copy

Available as preprint [PDF] and from USENIX.

Bibtex entry

@article{Klein_09:login,
  author =   {Gerwin Klein},
  title =    {Correct OS Kernel? Proof? Done!},
  journal =  {USENIX ;login:},
  year =     2009,
  volume =   34,
  number =   6,
  pages =    {28--34},
  month =    dec,
  publisher = {USENIX},
}
Gerwin Klein
2009-12-07