The University of New South Wales

seL4 enforces integrity

Authors

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

NICTA

UNSW

Abstract

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.

BibTeX Entry

  @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}
  }

Download