seL4 Enforces Integrity

Select |




Print


Sewell, Thomas; Winwood, Simon; Gammie, Peter; Murray, Toby; Andronick, June; Klein, Gerwin

Sewell, Thomas; Winwood, Simon; Gammie, Peter; Murray, Toby; Andronick, June; Klein, Gerwin


2011-08-22


Conference Material


Interactive Theorem Proving (ITP)


Nijmegen, The Netherlands


325-340


We prove the enforcement of two high-level access control properties in the seL4 microkernel: 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 holds via refinement for the C implementation of the kernel.


Springer


seL4, Isabelle/HOL, integrity, access control, security


https://doi.org/10.1007/978-3-642-22863-6_24


http://itp2011.cs.ru.nl/ITP2011/


nicta:4709


Sewell, Thomas; Winwood, Simon; Gammie, Peter; Murray, Toby; Andronick, June; Klein, Gerwin. seL4 Enforces Integrity. In: Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk Editor, editor/s. Interactive Theorem Proving (ITP); Nijmegen, The Netherlands. Springer; 2011-08-22. 325-340. https://doi.org/10.1007/978-3-642-22863-6_24



Loading citation data...

Citation counts
(Requires subscription to view)