Trustworthy Systems

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

Download