Proving compilation correctness
Proving compilation correctness is one of our formal methods research projects.
We have proved that the C source code of seL4 is correctly compiled to executable machine code. Together with the seL4 functional correctness proof, this means that seL4 behaves according to its formal specification, even when compiled with an untrusted compiler (such as GCC).
Our approach is post-hoc translation validation. We have developed a binary verification toolchain which takes the machine code produced by the C compiler, and automatically proves that it is a correct translation of the corresponding C source code. For the C code, the toolchain uses the same model and semantics as the seL4 functional correctness proof, so that the proofs compose. For the binary, the toolchain uses the Cambridge ARM semantics and the SRI RISC-V semantics, both expressed in the L3 specification language.
The toolchain consists of three components which communicate via a common control-flow graph language (GraphLang):
- A decompiler which takes the ELF binary, and produces corresponding GraphLang, together with a proof of simulation to the compiled binary in HOL4.
- A pseudo-compiler which takes the C source code, and produces corresponding GraphLang, together with a proof of refinement in Isabelle/HOL.
- A custom prover which takes the C and binary GraphLang, and proves refinement with the help of a suite of SMT solvers.
Thomas Sewell, during his PhD, developed a binary verification toolchain for
ARMv7. It proved compilation correctness for all functions covered by the
seL4 functional correctness proof
at optimisation level O1. It also verified many functions at optimisation
level O2. More recently, Matthew Brecknell, Zoltan A. Kocsis and others
developed a toolchain for the 64-bit RISC-V architecture.
People
Past
|
Publications
|
 |
Gernot Heiser, Gerwin Klein and June Andronick seL4 in Australia: From research to real-world trustworthy systems Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020 |
|
|
|
Thomas Sewell Translation validation for verified, efficient and timely operating systems PhD Thesis, UNSW, Sydney, Australia, 2017 |
|
|
Thomas Sewell, Magnus Myreen and Gerwin Klein Translation validation for a verified OS kernel ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013 |