NICTA
UNSW
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.
@inproceedings{Sewell_WGMAK_11, publisher = {Springer}, doi = {10.1007/978-3-642-22863-6_24}, month = aug, booktitle = {International Conference on Interactive Theorem Proving}, paperurl = {https://trustworthy.systems/publications/nicta_full_text/4709.pdf}, year = {2011}, editor = {{Marko van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk}}, keywords = {sel4, isabelle/hol, integrity, access control, security}, title = {{seL4} Enforces Integrity}, pages = {325--340}, author = {Sewell, Thomas and Winwood, Simon and Gammie, Peter and Murray, Toby and Andronick, June and Klein, Gerwin}, address = {Nijmegen, The Netherlands} }