Skip to main content

Proving compilation correctness

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

ASM refine diagram
  • 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

Current

Past

Publications

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
Served by Apache on Linux on seL4.