|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 listsCambridge University Engineering Department Talks Life Sciences ‘Geographies of Radical Difference’
Other talksMoving Forward with Stem Cell Therapy Tracing the evolution of passive galaxies at z~1.4-2 with KMOS Discriminative Embeddings of Latent Variable Models for Structured Data Bayesian Hierarchical Community Discovery From Graphon to Graphex: Models and Estimators for Sparse Networks using Exchangeable Random Measures The functional study of P1/HC-Pro in the suppression of the miRNA pathway