Comprehensive formal verification of an OS microkernel
Top Cited Papers
- 26 February 2014
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in ACM Transactions on Computer Systems
- Vol. 32 (1), 1-70
- https://doi.org/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 initialiser for user-level systems that connects kernel-level access-control enforcement with reasoning about system behaviour. We summarise these results and show how they integrate to form a coherent overall analysis, backed by machine-checked, end-to-end theorems. The seL4 microkernel is currently not just the only general-purpose operating system kernel that is fully formally verified to this degree. It is also the only example of formal proof of this scale that is kept current as the requirements, design and implementation of the system evolve over almost a decade. We report on our experience in maintaining this evolving formally verified code base.Keywords
Funding Information
- Department of Broadband, Communications and the Digital Economy , Australian Government
- Australian Research Council
This publication has 73 references indexed in Scilit:
- The worst-case execution-time problem—overview of methods and survey of toolsACM Transactions on Embedded Computing Systems, 2008
- Chronos: A timing analyzer for embedded softwareScience of Computer Programming, 2007
- The MILS architecture for high-assurance embedded systemsInternational Journal of Embedded Systems, 2006
- Toward real microkernelsCommunications of the ACM, 1996
- Kit: a study in operating system verificationIEEE Transactions on Software Engineering, 1989
- Specification and verification of the UCLA Unix security kernelCommunications of the ACM, 1980
- A Linear Time Algorithm for Deciding Subject SecurityJournal of the ACM, 1977
- HYDRACommunications of the ACM, 1974
- The nucleus of a multiprogramming systemCommunications of the ACM, 1970
- Programming semantics for multiprogrammed computationsCommunications of the ACM, 1966