Trustworthy Systems

Proving compilation correctness

Proving compilation correctness is one of our formal methods research projects.

ASM refine diagram

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




Abstract PDF 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
Abstract PDF Thomas Sewell
Translation validation for verified, efficient and timely operating systems
PhD Thesis, UNSW, Sydney, Australia, July, 2017
PDF 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