Formalising a High-Performance Microkernel

Kevin Elphinstone, Gerwin Klein and Rafal Kolanski

Abstract

This paper argues that a pragmatic approach is needed for integrating design and formalisation of complex systems. We report on our approach to designing the seL4 operating system microkernel API and its formalisation in Isabelle/HOL. The formalisation consists of the systematic translation of significant parts of the functional programming language Haskell into Isabelle/HOL, including monad-based code. We give an account of the experience, decisions and outcomes in this translation as well as the technical problems we encountered together with our solutions. The longer-term goal is to demonstrate that formalisation and verification of a large, complex, OS-level code base is feasible with current tools and methods and is in the order of magnitude of traditional development cost.

Online Copy

Available as [PDF]

Bibtex entry

@inproceedings{ElphinstoneKK-06,
  author =    {Kevin Elphinstone and Gerwin Klein and Rafal Kolanski},
  title =     {Formalising a High-Performance Microkernel},
  booktitle = {Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06)},
  series =    {Microsoft Research Technical Report MSR-TR-2006-117},
  year =      {2006},
  editor =    {Rustan Leino},
  address =   {Seattle, USA},
  month =     Aug,
  pages =     {1-7}
}
Gerwin Klein
2006-09-13 08:00:27