Proving compilation correctness

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

Aim: To eliminate the compiler correctness assumption of the seL4 functional correctness proof.
- using the Cambridge ARM semantics.
- comparing the semantics of the compiled seL4 kernel to the semantics of the C source assumed in the existing verification.
Approach:
- Decompilation into logic. Translating the binary elf image into the theorem prover, producing a collection of recursive bitvector functions together with a proof of simulation to the compiled binary object.
- Conversion of decompiled recursive bitvector functions from HOL4 to Isabelle/HOL.
- Compilation into logic. Reduction of the C semantics used in the L4.verified project to bitvector functions by eliminating C language elements, including structure types, early return, underspecified types, etc.
- Proving equivalence of bitvector functions through a customised connection to SMT solvers.
Results:

Decompilation with proof is completed for all of seL4 as compiled by gcc 4.5.1 at optimisation levels 1 and 2.

Pseudo-compilation with proof is completed for all of seL4.

Equivalence is proven for all previously verified C functions in seL4 as compiled by gcc 4.5.1 at optimisation level 1. Assembly routines and nested loops were not handled; these did not appear in the previously verified codebase.

People

		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