Trustworthy Systems

A verified shared capability model

Authors

Andrew Boyton

NICTA

UNSW

Abstract

This paper presents a high-level access control model of the seL4 microkernel. We extend an earlier formalisation by Elkaduwe et al with non-determinism, explicit sharing of capability storage, and a delete-operation for entities. We formally prove that this new model can enforce system-global security policies as well as authority confinement. The motivation for dealing with sharing explicitly in the high-level, abstract access control model is to simplify the refinement proof towards the seL4 implementation considerably. To our knowledge this is the first formal, machine-checked access control model with explicit sharing of authority.

BibTeX Entry

  @inproceedings{Boyton_09,
    address          = {Aachen, Germany},
    author           = {Boyton, Andrew},
    booktitle        = {Systems Software Verification},
    keywords         = {shared capabilities, interactive theorem proving},
    month            = oct,
    pages            = {25--44},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/1810.pdf},
    title            = {A Verified Shared Capability Model},
    year             = {2009}
  }

Download