The University of New South Wales

Noninterference for operating system kernels

Authors

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie and Gerwin Klein

NICTA

UNSW

Australian National University

Abstract

While intransitive noninterference is a natural property for any secure OS kernel to enforce, proving that the implementation of any particular general-purpose kernel enforces this property is yet to be achieved. In this paper we take a significant step towards this vision by presenting a machine-checked formulation of intransitive noninterference for OS kernels, and its associated sound and complete unwinding conditions, as well as a scalable proof calculus over nondeterministic state monads for discharging these unwinding conditions across a kernel's implementation. Our ongoing experience applying this noninterference framework and proof calculus to the seL4 microkernel validates their utility and real-world applicability.

BibTeX Entry

  @inproceedings{Murray_MBGK_12,
    isbn             = {978-3-642-35307-9},
    publisher        = {Springer},
    booktitle        = {International Conference on Certified Programs and Proofs},
    month            = dec,
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6004.pdf},
    year             = {2012},
    editor           = {{Chris Hawblitzel and Dale Miller}},
    keywords         = {information flow, refinement, scheduling, state monads},
    title            = {Noninterference for Operating System Kernels},
    pages            = {126--142},
    author           = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Klein, Gerwin},
    address          = {Kyoto, Japan}
  }

Download