The L4.verified project
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.
The figure above shows the formal refinement approach L4.verified 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-preformance 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. A good start into to the general aria is "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 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.
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 has never been achieved before.
- The implementation correctness proof between high-level and low-level design alone already makes the seL4 kernel, to our knowledge, 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 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.