|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 listsChurchill Undergraduate Physics Seminars Existential Risk Seminar Series Institution of Civil Engineers (Cambridge Branch)
Other talksHyperkhler toy models Antibiotic resistance and antibiotic alternatives: Looking towards the future The 2015 Pregnancy Summit TBC Symplectic and hyperkahler implosion Hack the Lab