Trustworthy Systems

seL4: From general purpose to a proof of information flow enforcement

Authors

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein

NICTA

UNSW

Abstract

In contrast to testing, mathematical reasoning and formal verification can show the absence of whole classes of security vulnerabilities. We present the, to our knowledge, first complete, formal, machine-checked verification of information flow security for the implementation of a general-purpose microkernel; namely seL4. Unlike previous proofs of information flow security for operating system kernels, ours applies to the actual 8,830 lines of C code that implement seL4, and so rules out the possibility of invalidation by implementation errors in this code. We assume correctness of compiler, assembly code, hardware, and boot code. We prove everything else. This proof is strong evidence of seL4's utility as a separation kernel, and describes precisely how the general purpose kernel should be configured to enforce isolation and mandatory information flow control. We describe the information flow security statement we proved (a variant of intransitive noninterference), including the assumptions on which it rests, as well as the modifications that had to be made to seL4 to ensure it was enforced. We discuss the practical limitations and implications of this result, including covert channels not covered by the formal proof.

BibTeX Entry

  @inproceedings{Murray_MBGBSLGK_13,
    address          = {San Francisco, CA},
    author           = {Murray, Toby and Matichuk, Daniel and Brassil, Matthew and Gammie, Peter and Bourke, Timothy and
                        Seefried, Sean and Lewis, Corey and Gao, Xin and Klein, Gerwin},
    booktitle        = {IEEE Symposium on Security and Privacy},
    doi              = {10.1109/SP.2013.35},
    keywords         = {correctness proofs, information flow controls, mechanical verification},
    month            = may,
    pages            = {415--429},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/6464.pdf},
    publisher        = {IEEE},
    slides           = {https://trustworthy.systems/publications/nicta_slides/6464.pdf},
    title            = {{seL4}: from General Purpose to a Proof of Information Flow Enforcement},
    year             = {2013}
  }

Download