Trustworthy Systems

Formally verified software in the real world

Authors

Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez

DATA61

Intel

UNSW Sydney

University of Melbourne

Abstract

We present an approach for building highly-dependable systems that derive their assurance from a formally-verified operating system which guarantees isolation between subsystems. We leverage those guarantees to enforce security through non-bypassable architectural constraints, and through generation of code and proofs from the architecture. We show that this approach can produce a system that is highly robust against cyber attacks, even without formal proof of its overall security. We demonstrate not only that this approach is applicable to real-world systems, such as autonomous vehicles, but also that it is possible to re-engineer an existing insecure system to achieve high robustness, and that this can be done by engineers not trained in formal methods.

BibTeX Entry

  @article{Klein_AKMHF_18,
    author           = {Klein, Gerwin and Andronick, June and Kuz, Ihor and Murray, Toby and Heiser, Gernot and Fernandez,
                        Matthew},
    date             = {2018-10-1},
    doi              = {https://doi.org/10.1145/3230627},
    issn             = {0001-0782},
    issue            = {10},
    journal          = {Communications of the ACM},
    month            = oct,
    pages            = {68-77},
    paperurl         = {https://trustworthy.systems/publications/full_text/Klein_AKMHF_18.pdf},
    publisher        = {ACM},
    title            = {Formally Verified Software in the Real World},
    volume           = {61},
    year             = {2018}
  }

Download