Skip to main content

TS

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,
    slides           = {http://www.nicta.com.au/pub-download/slides/7313},
    author           = {Heiser, Gernot},
    month            = {jul},
    note             = {Keynote at APSys'13},
    year             = {2013},
    keywords         = {sel4 microkernel verification},
    title            = {Can Truly Dependable Systems Be Affordable?},
    type             = {Presentation},
    booktitle        = {Asia-Pacific Workshop on Systems (APSys)},
    address          = {Singapore}
  }

Download