Journal article
Comprehensive Formal Verification of an OS Microkernel
G Klein, J Andronick, K Elphinstone, T Murray, T Sewell, R Kolanski, G Heiser
ACM Transactions on Computer Systems | Association for Computing Machinery (ACM) | Published : 2014
DOI: 10.1145/2560537
Abstract
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 transform this result into a comprehensive formal verification of the kernel: a formally verified IPC fastpath, a proof that the binary code of the kernel correctly implements the C semantics, a proof of correct access-control enforcement, a proof of information-flow noninterference, a sound worst-case execution time analysis of the binary, and an automatic initia..
View full abstractGrants
Funding Acknowledgements
NICTA is funded by the Australian Government as represented by the Department of Broadband, Communications and the Digital Economy and the Australian Research Council through the ICT Centre of Excellence program.