seL4 Enforces Integrity
Thomas Arthur Leck Sewell, Simon Winwood, Peter Gammie, TC Murray, June Andronick, Gerwin Klein · 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. 1