Abstract

The L4.verified project has proved functional correctness of C code which implements a general-purpose operating system. The C code is about 10,000 lines long and is designed to run on ARM processors. The 200,000-line L4.verified proof currently bottoms out at the level of C code, i.e. the C compiler is currently a trusted component in the intended workflow.

In this talk, we will describe how we are using the Cambridge model of the ARM instruction set architecture (ISA) to remove the C compiler from the trusted computing base. That is, we are extending the existing L4.verified proof downwards so that it bottoms out at a much lower level, namely, the concrete ARM machine code which runs directly on ARM hardware.

The L4.verified project and the Cambridge ARM project have for years been developed independently of one another. The main challenge is now: how do we bridge the gap between these separate projects? Our solution is to apply a technology, which we call, decompilation into logic. Our tool, a decompiler, translates ARM machine code into functional programs that are automatically verified to be functionally equivalent with respect to the Cambridge model of the ARM ISA . We apply our decompiler to the output of the C compiler to turn the seL4 binary into a large functional program. A connection can then be proved semi-automatically between this functional program and the semantics of the C code used in the L4.verified proof.

This talk describes ongoing work which, when complete, will remove the need to trust the C compiler and the C semantics. The new proof will instead have the Cambridge ARM model as a trusted component.

This is joint work with Thomas Sewell, Michael Norrish and Gerwin Klein of NICTA , Australia.