The L4.verified project
These are the technical project pages. If you are looking for a general overview, please follow this link.
News
The JAR Special Issue on Operating System Verification has appeared and the proceedings of SSV'09 will appear soon.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. A good overview paper is "Operating System Verification -- An Overview".
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 with the C-level verification proof more than 95% completed. We expect to finish within the next weeks.
Outcomes
While the project is not fully completed yet, it has already achieved a number of significant research outcomes. Some highlights are:
- With the implementation correctness proof between high-level and low-level design completed, the seL4 kernel, to our knowledge, is already now the best, and most deeply analysed high-performance microkernel in the world.
- In producing the seL4 design and implementation together with the seL4 project, we have developed a methodology and tool set for rapid-prototyping of small OS kernels. This methodology has a very short turn-around time for trying out new features and integrates formal specification and verification directly into the development cycle. Developing and testing new kernel features in this method takes on the order of hours and days instead of weeks and months. Developing a new high-assurance kernel-design would not have been possible without it in the available time.
- For the currently ongoing C implementation correctness proof, we developed a very precise formalisation of the C programming language and its memory model. The formalisation includes low-level and unsafe C programming constructs like pointer arithmetic and pointer cast. Harvey Tuch, the main investigator and PhD student on this part, recently won the CISRA PhD award for this model which allows us to reason abstractly and efficiently about these C features that are usually outside the scope of verification projects, but are required for microkernel performance optimisations.
Commercialisation
The research outcomes of the project are set to be commercialised in the NICTA spinout company Open Kernel Labs. Stay tuned for the first commercially available, fully formally verified microkernel.
People
Current
- Timothy Bourke
- Andrew Boyton
- David Cock
- Gernot Heiser
- Gerwin Klein
- June Andronick
- Kai Engelhardt
- Kevin Elphinstone
- Michael Norrish
- Philip Derrin
- Rafal Kolanski
- Thomas Sewell
Past
- Simon Winwood
- Catherine Menon
- David Tsai
- Harvey Tuch
- Jeremy Dawson
- Jia Meng