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.
@inproceedings{Elkaduwe_KE_08,
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,
}