Trustworthy Systems

Provable security: How feasible is it?

Authors

Gerwin Klein, Toby Murray, Peter Gammie, Thomas Sewell and Simon Winwood

NICTA

UNSW

Abstract

Strong, machine-checked security proofs of operating systems have been in the too hard basket long enough.

They will still be too hard for the humongous mainstream operating systems, but even for systems designed from the ground up for security they have been counted as infeasible. There are high-level formal models, nice security properties, ways of architecting and engineering secure systems, but no implementation level proofs yet, not even with the recent formal verification of the seL4 microkernel.

This needs to change.

BibTeX Entry

  @inproceedings{Klein_MGSW_11,
    address          = {Napa, USA},
    author           = {Klein, Gerwin and Murray, Toby and Gammie, Peter and Sewell, Thomas and Winwood, Simon},
    booktitle        = {Workshop on Hot Topics in Operating Systems (HotOS)},
    keywords         = {security, proof, sel4},
    month            = may,
    pages            = {5},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/4631.pdf},
    publisher        = {USENIX},
    title            = {Provable Security: How feasible is it?},
    year             = {2011}
  }

Download