The University of New South Wales

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.

Approach

L4.verified refinemetn apprach

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 of the security properties that seL4 can enforce: 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. The arrow between access control model and high-level design is dotted, because this proof is not part of the L4.verified project and is left for future work.

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".

Status

The project has successfully completed all of the specification artefacts shown in the picture and all of the proofs denoted by solid arrows: the security proof, the refinement towards the low-level design, and the refinement down to the C implementation.

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 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.

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.