Trustworthy Systems

Towards proving security in the presence of large untrusted components

Authors

June Andronick, David Greenaway and Kevin Elphinstone

NICTA

UNSW

Abstract

This paper proposes a generalized framework to build large, complex systems where security guarantees can be given for the overall system's implementation. The work builds on the formally proven correct seL4 microkernel and on its fine-grained mandatory access control. This access control mechanism allows large untrusted components to be isolated in a way that prevents them from violating a defined security property, leaving only the trusted components to be formally verified. The first steps of the approach are illustrated by the formalisation of a multilevel secure access device and a proof in Isabelle/HOL that information cannot flow from one back-end network to another.

BibTeX Entry

  @inproceedings{Andronick_GE_10,
    address          = {Vancouver, CA},
    author           = {Andronick, June and Greenaway, David and Elphinstone, Kevin},
    booktitle        = {Systems Software Verification},
    editor           = {{Ralf Huuck, Gerwin Klein, Bastian Schlich}},
    month            = oct,
    pages            = {9},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/3997.pdf},
    publisher        = {USENIX},
    title            = {Towards proving security in the presence of large untrusted components},
    year             = {2010}
  }

Download