Search For:

Displaying 1-3 out of 3 total
It's Time for Trustworthy Systems
Found in: IEEE Security and Privacy
By Gernot Heiser,Toby Murray,Gerwin Klein
Issue Date:March 2012
pp. 67-70
The time has arrived for truly trustworthy systems, backed by machine-checked proofs of security and reliability. Research demonstrates that formal whole-system analysis that applies to the C and binary implementation level is feasible, including proofs of...
Comprehensive formal verification of an OS microkernel
Found in: ACM Transactions on Computer Systems (TOCS)
By Gernot Heiser, Gerwin Klein, June Andronick, Kevin Elphinstone, Rafal Kolanski, Thomas Sewell, Toby Murray
Issue Date:February 2014
pp. 1-70
We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel. We discuss the kernel design we used to make its verification tractable. We then describe the functional corre...
File systems deserve verification too!
Found in: Proceedings of the Seventh Workshop on Programming Languages and Operating Systems (PLOS '13)
By Gabriele Keller, Gernot Heiser, Gerwin Klein, Leonid Ryzhyk, Liam O'Connor, Sidney Amani, Toby Murray, Zilin Chen
Issue Date:November 2013
pp. 1-7
File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations --- we need verified correctness but ...