Comprehensive formal verification of an OS microkernel
ACM Trans. Comput. Syst., 2014.
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 correctness proof of the kernel's C implementation and we cover further steps that transf...More
Full Text (Upload PDF)
PPT (Upload PPT)