|COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring.|
Using the Cambridge ARM model to verify the concrete machine code of seL4
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:
Note that ex-directory lists are not shown.
Other listsCentre of South Asian Studies occasional events Martin Centre Research Seminar Series - 40th Annual Series of Lunchtime Lectures Sedgwick Museum of Earth Sciences
Other talksNo Babbage Seminar Today Owing to The Wheeler Lecture Radiotherapy The 2014 Alcuin Lecture: The UK in or out of the EU: an Italian/European point of view Novel Biomaterials and Technology for use in Regenerative Medicine/Tissue Engineering Evaluation of the tumour bed biopsy technique in canine and feline oncologic surgery Mutational and Functional analysis of melanoma: filling in the gap