Verified Protection Model of the seL4 Microkernel

Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone


This paper presents a machine-checked high-level security analysis of seL4 -- an evolution of the L4 kernel series targeted to secure, embedded devices. We provide an abstract specification of the seL4 access control system together with a formal proof that shows how confined subsystems can be enforced. All proofs and specifications in this paper are developed in the interactive theorem prover Isabelle/HOL.

Online Copy

Available as [PDF]

Bibtex entry

	  author =      {Dhammika Elkaduwe and Gerwin Klein and Kevin Elphinstone},
	  title =       {Verified Protection Model of the {seL4} Microkernel},
	  booktitle = {Second IFIP Working Conference on
	  Verified Software: Theories, Tools, and Experiments (VSTTE 2008)},
	  editor =      {Jim Woodcock and Natarajan Shankar},
	  address =     {Toronto, Canada},
	  publisher =   {Springer},
	  year =         2008,
	  month =        oct,
	  series =      {LNCS},
	  pages =     {99--114},
	  volume =    5295,
Gerwin Klein