seL4: Formal Verification of an OS Kernel

Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood

Abstract

We report on the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its C implementation. We assume correctness of compiler, assembly code, hardware, and boot code.

seL4 is a third-generation microkernel of L4 provenance, comprising 8,700 lines of C and 600 lines of assembler. Its performance is comparable to other high-performance L4 kernels.

We prove that the implementation always strictly follows our high-level abstract specification of kernel behaviour. This encompasses traditional design and implementation safety properties such as that the kernel will never crash, and it will never perform an unsafe operation. It also implies much more: we can predict precisely how the kernel will behave in every possible situation.

 

This is the shorter CACM research highlight version of the SOSP'09 paper for a more general computer-science audience.

Online Copy

Available as [PDF] (preprint)

Bibtex entry

@article{seL4_CACM_10,
  author =  {Gerwin Klein 
  and June Andronick
  and Kevin Elphinstone 
  and Gernot Heiser	 
  and David Cock
  and Philip Derrin
  and Dhammika Elkaduwe
  and Kai Engelhardt
  and Rafal Kolanski
  and Michael Norrish
  and Thomas Sewell
  and Harvey Tuch
  and Simon Winwood},
  title =        {{seL4}: Formal Verification of an {OS} Kernel},
  journal =      {Communications of the ACM (CACM)},
  publisher =    {ACM},
  year =         {2010},  
  month =        jun,
  pages =        {107--115},
  volume =       53, 
  number =       6
}
Gerwin Klein
2010-06-02