Translation validation for a verified OS kernel

Authors

Thomas Sewell, Magnus Myreen and Gerwin Klein

NICTA

UNSW

University of Cambridge

Abstract

We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit the assembly routines and volatile accesses used to control system hardware.

More generally, we present an approach for proving refinement between the formal semantics of a program on the C source level and its formal semantics on the binary level, thus checking the validity of compilation, including some optimisations, and linking, and extending static properties proved of the source code to the executable. We make use of recent improvements in SMT solvers to almost fully automate this process.

We handle binaries generated by unmodified gcc 4.5.1 at optimisation level 1, and can handle most of seL4 even at optimisation level 2.

BibTeX Entry

  @inproceedings{Sewell_MK_13,
    publisher        = {ACM},
    booktitle        = {ACM SIGPLAN Conference on Programming Language Design and Implementation},
    month            = jun,
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/6449.pdf},
    slides           = {/publications/nicta_slides/6449.pdf},
    year             = {2013},
    keywords         = {isabelle, sel4, microkernel, binary verification},
    title            = {Translation Validation for a Verified {OS} Kernel},
    pages            = {471--481},
    author           = {Sewell, Thomas and Myreen, Magnus and Klein, Gerwin},
    address          = {Seattle, Washington, USA}
  }

Download