Trustworthy Systems

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

Download