The L4.verified project
These are the technical project pages. If you are looking for a general overview, please follow this link.
News
Submit a paper to the JAR Special Issue on Operating System Verification!Creating Trustworthy Software
The L4.verified project is providing a mathematical, machine-checked proof of the functional correctness of the seL4 microkernel with respect to a high level, formal description of its expected behaviour. The aim is to produce a truly trustworthy, high-performance operating system kernel.
Approach
The figure above shows the formal refinement approach L4.verified is taking. The bottom level of the verification and of the refinement picture is a high-performance C and assembly implementation of the seL4 microkernel. The next level up, the low-level design, is a detailed, executable specification of the intended behaviour of the C implementation. This executable specification is derived automatically from a prototype of the kernel, developed in the seL4 project. The prototype was written in the high-level, functional programming language Haskell. The next refinement layer up is the high-level design, an abstract, operational specification of the kernel. It contains less detail and is not directly executable any more, but it still precisely captures the intended kernel behaviour. Finally, on the top-most level, there is an abstract access control model of seL4 that captures how capabilities (the kernel's access control mechanism) are distributed in the system. To the right of this access control model, the picture shows one security property that seL4 can enforce: guaranteed isolation of security domains.
All proofs in the project, shown as green arrows in the picture, are machine-checked in the interactive theorem prover Isabelle/HOL.
For a more in-depth overview of the project, please check the publications page.
Status
The project has so far completed all of the specification artefacts show in the picture and proved the formal correspondence between abstract and executable specification as well as the security property of the top-level model. Work is currently ongoing on the two remaining correspondence proofs.
People
Current
- Andrew Boyton
- David Cock
- Gernot Heiser
- Gerwin Klein
- Kai Engelhardt
- Kevin Elphinstone
- Michael Norrish
- Philip Derrin
- Rafal Kolanski
- Simon Winwood
- Thomas Sewell
Past
- Catherine Menon
- David Tsai
- Harvey Tuch
- Jeremy Dawson
- Jia Meng