Skip to main content
CSIRO Logo Data 61 logo

It's time for trustworthy systems

Authors

Gernot Heiser, Toby Murray and Gerwin Klein

NICTA

UNSW

Abstract

The time has arrived for truly trustworthy systems, backed by machine-checked proofs of security and reliability. Research demonstrates that formal whole-system analysis that applies to the C and binary implementation level is feasible, including proofs of integrity, authority confinement, confidentiality, and worst-case execution time. Because these proofs build on previous results, they become easier each year. However, they do have some limitations.

BibTeX Entry

  @article{Heiser_MK_12,
    publisher        = {IEEE Computer Society},
    month            = mar,
    journal          = {IEEE Symposium on Security and Privacy},
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/5778.pdf},
    year             = {2012},
    keywords         = {trustworthy systems, verification and analysis, sel4 microkernel, integrity, confidentiality,
                        worst-case execution time, safety, security, computer security, functional correctness, authority
                        confinement, noninterference},
    volume           = {10},
    title            = {It's Time for Trustworthy Systems},
    number           = {2},
    author           = {Heiser, Gernot and Murray, Toby and Klein, Gerwin},
    pages            = {67--70}
  }

Download