Trustworthy Systems

Secure microkernels, state monads and scalable refinement

Authors

David Cock, Gerwin Klein and Thomas Sewell

NICTA

UNSW

Abstract

We present a scalable, practical Hoare Logic and refinement calculus for the nondeterministic state monad with exceptions and failure in Isabelle/HOL. The emphasis of this formalisation is on large-scale verification of imperative-style functional programs, rather than expressing monad calculi in full generality. We achieve scalability in two dimensions. The method scales to multiple team members working productively and largely independently on a single proof and also to large programs with large and complex properties.

We report on our experience in applying the techniques in an extensive (100K lines of proof) case study---the formal verification of an executable model of the seL4 operating system microkernel.

BibTeX Entry

  @inproceedings{Cock_KS_08,
    address          = {Montreal, Canada},
    author           = {Cock, David and Klein, Gerwin and Sewell, Thomas},
    booktitle        = {International Conference on Theorem Proving in Higher Order Logics},
    doi              = {10.1007/978-3-540-71067-7_16},
    editor           = {{Otmane Ait Mohamed, C{\'e}sar Mu{\~n}oz, Sofi{\`e}ne Tahar}},
    keywords         = {state monad, refinement, microkernel, isabelle/hol, sel4},
    month            = aug,
    pages            = {167--182},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/483.pdf},
    publisher        = {Springer},
    title            = {Secure Microkernels, State Monads and Scalable Refinement},
    year             = {2008}
  }

Download