Skip to main content

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):

  • 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

Current

Past

  • Ed Pierzchalski
  • Magnus Myreen
  • Thomas Sewell

Publications

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, 2017
Abstract
Slides
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