Using the Cambridge ARM model to verify the concrete machine code of seL4

Add to your list(s) Download to your calendar using vCal

• Magnus Myreen (University of Cambridge)
• Thursday 28 April 2011, 13:15-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact William Denman.

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.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory Security Seminar
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Security-related talks
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.