Trustworthy Systems

Mind the gap: A verification framework for low-level C

Authors

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock and Michael Norrish

NICTA

UNSW

Australian National University

Abstract

This paper presents the formal Isabelle/HOL framework we use to prove refinement between an executable, monadic specification and the C implementation of the seL4 microkernel. We describe the refinement framework itself, the automated tactics it supports, and the connection to our previous C verification framework. We also report on our experience in applying the framework to seL4. The characteristics of this microkernel verification are the size of the target (8,700 lines of C code), the treatment of low-level programming constructs, the focus on high performance, and the large subset of the C programming language addressed, which includes pointer arithmetic and type-unsafe code.

BibTeX Entry

  @inproceedings{Winwood_KSACN_09,
    address          = {Munich, Germany},
    author           = {Winwood, Simon and Klein, Gerwin and Sewell, Thomas and Andronick, June and Cock, David and Norrish,
                        Michael},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    doi              = {10.1007/978-3-642-03359-9_34},
    editor           = {{S. Berghofer, T. Nipkow, C. Urban, M. Wenzel}},
    keywords         = {sel4, isabelle, os verification, c},
    month            = aug,
    pages            = {500--515},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/1842.pdf},
    publisher        = {Springer},
    title            = {Mind the Gap: A Verification Framework for Low-Level {C}},
    year             = {2009}
  }

Download