Skip to main content

TS

Provably trustworthy systems

Authors

Gerwin Klein, June Andronick, Gabriele Keller, Daniel Matichuk and Toby Murray

DATA61

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_AKMM_17,
    publisher        = {The Royal Society Publishing},
    doi              = {10.1098/rsta.2015.0404},
    journal          = {Philosophical Transactions of the Royal SocietyA},
    author           = {Klein, Gerwin and Andronick, June and Keller, Gabriele and Matichuk, Daniel and Murray, Toby},
    month            = sep,
    volume           = {375},
    keywords         = {sel4, proof engineering, code/proof co-generation, cogent, isabelle/hol},
    year             = {2017},
    date             = {2017-9-4},
    title            = {Provably Trustworthy Systems},
    type             = {Journal Article - Refereed},
    pages            = {1-23}
  }

Download

Served by Apache on Linux on seL4.