Correct OS kernel? Proof? Done!

Select |




Print


Klein, Gerwin

Klein, Gerwin


2009-12-03


Journal Article


USENIX ;login:,


34


6


28--34


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.


seL4, microkernel, Isabelle, formal verification


http://www.usenix.org/publications/login/2009-12/index.html


nicta:3159


Klein, Gerwin. Correct OS kernel? Proof? Done!. USENIX ;login:,. 2009-12-03; 34(6):28--34.



Loading citation data...

Citation counts
(Requires subscription to view)