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):
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
O2. More recently, Matthew Brecknell, Zoltan A. Kocsis and others
developed a toolchain for the 64-bit RISC-V architecture.
|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
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