Trustworthy Systems

Can truly dependable systems be affordable?

Authors

Gernot Heiser

NICTA

UNSW

Abstract

With the formal verification of the seL4 microkernel, and subsequent work on assuring its safety and security properties, NICTA has recently not only demonstrated that unprecedented levels of assurance are possible, but also that the cost is competitive. In this talk I will examine what has been achieved, what the cost was, and how this might apply to larger systems, in particular the feasibility of assuring full-system safety or security. The result is cause for optimism.

BibTeX Entry

  @misc{Heiser_13_2,
    address          = {Singapore},
    author           = {Heiser, Gernot},
    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    keywords         = {sel4 microkernel verification},
    month            = jul,
    note             = {Keynote at APSys'13},
    paperurl         = {https://trustworthy.systems/publications/nicta_full_text/7313.pdf},
    slides           = {https://trustworthy.systems/publications/nicta_slides/7313.pdf},
    title            = {Can Truly Dependable Systems Be Affordable?},
    year             = {2013}
  }

Download