The L4.verified project
Approach
The figure above shows the formal refinement approach the L4.verified project has taken. The bottom level of the verification and of the refinement is a HOL4 representation of the compiled binary of the seL4 microkernel. This is followed by a high-performance C and assembly implementation, created using our C Parser tool. The next level up 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. The top two layers are a laguage for configuring seL4-based systems (capDL) and a collection of security properties (in particular integrity and confidentiality) that have been proven about seL4.
All proofs in the project, shown as bidirectional arrows in the picture, are machine-checked in interactive theorem provers such as Isabelle/HOL and HOL4.
For a more in-depth overview of the project, please check the publications page. An introductory overview of the general area can be found in "Operating System Verification — An Overview", a high-level overview of the verification project can be found in the SOSP'09 paper "seL4: Formal Verification of an OS Kernel". The TOCS paper "Comprehensive Formal Verification of an OS Microkernel" gives a retrospective overview of the verification, including the security theorems, binary verification, and system initialiation theorems that were produced later.
Status
The project has successfully completed all of the specification artefacts shown in the picture and all of the proofs depicted. Both the binary refinement proof and further security proofs are currently active research areas — for more information see their project pages here and here.
Outcomes
The project has achieved a number of significant research outcomes. Some highlights are:
- An implementation correctness proof between low-level design and C implementation for a code base of similar size or complexity had not been achieved before.
- 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 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, 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.