Towards a Practical, Verified Kernel

Kevin Elphinstone, Gerwin Klein, Philip Derrin, Timothy Roscoe, and Gernot Heiser

Abstract

In the paper we examine one of the issues in designing, specifying, implementing and formally verifying a small operating system kernel -- how to provide a productive and iterative development methodology for both operating system developers and formal methods practitioners.

We espouse the use of functional programming languages as a medium for prototyping that is readily amenable to formalisation with a low barrier to entry for kernel developers, and report early experience in the process of designing and building \sel4: a new, practical, and formally verified microkernel.

Online Copy

Available as [PDF]

Bibtex entry

@InProceedings{Elphinstone_KDRH_07,
  author =       {Kevin Elphinstone and Gerwin Klein and Philip Derrin
                  and Timothy Roscoe and Gernot Heiser},
  title =        {Towards a Practical, Verified Kernel},
  booktitle =    {Proc.\ 11th Workshop on Hot Topics in Operating Systems},
  year =         2007,
  pages =        6,
  address =      {San Diego, CA, USA},
  month =        may,
  note =         {Online proceedings at \url{http://www.usenix.org/events/hotos07/tech/}
}
Gerwin Klein
2007-07-13 14:26:30