Skip to main content

Proving Compilation Correctness

Proving Compilation Correctness

Proving Compilation Correctness is an activity of the Trustworthy Systems project.

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.

  • Contact:

    Thomas Sewell, thomas.sewell<at>nicta.com.au and
    Magnus Myreen, magnus.myreen<at>cl.cam.ac.uk

People

Current

Past

  • Magnus Myreen

Publications

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