Proving Compilation Correctness
Proving Compilation Correctness is an activity of the Trustworthy Systems project.
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.
- 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.
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.
|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