Conference Proceedings
seL4 Enforces Integrity
T Sewell, S Winwood, P Gammie, TC Murray, J Andronick, G Klein, M van Eekelen (ed.), H Geuvers (ed.), J Schmaltz (ed.), F Wiedijk (ed.)
Interactive Theorem Proving | Springer Berlin Heidelberg | Published : 2011
Abstract
We prove that the seL4 microkernel enforces two high-level access control properties: integrity and authority confinement. Integrity provides an upper bound on write operations. Authority confinement provides an upper bound on how authority may change. Apart from being a desirable security property in its own right, integrity can be used as a general framing property for the verification of user-level system composition. The proof is machine checked in Isabelle/HOL and the results hold via refinement for the C implementation of the kernel. © 2011 Springer-Verlag.