Trustworthy Systems

Provably trustworthy systems

Authors

Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk, Toby Murray and Liam O'Connor

DATA61

University of NSW

UNSW Sydney

University of Melbourne

Abstract

We present recent work on building trustworthy systems with formal proof from the ground up, including the operating system kernel, at the level binary machine code. In particular, we give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We show two complementary techniques for scaling these methods to larger systems: proof engineering, and code/proof co-generation.

BibTeX Entry

  @article{Klein_AKMMO_17,
    author           = {Klein, Gerwin and Andronick, June and Keller, Gabriele and Matichuk, Daniel and Murray, Toby and
                        O'Connor, Liam},
    date             = {2017-9-4},
    doi              = {https://doi.org/10.1098/rsta.2015.0404},
    issue            = {2104},
    journal          = {Philosophical Transactions of the Royal Society A},
    keywords         = {{seL4}, proof engineering, code/proof co-generation, {Cogent}, {Isabelle}/{HOL}},
    month            = sep,
    pages            = {1-23},
    paperurl         = {https://trustworthy.systems/publications/full_text/Klein_AKMMO_17.pdf},
    publisher        = {The Royal Society Publishing},
    title            = {Provably Trustworthy Systems},
    volume           = {375},
    year             = {2017}
  }

Download