Trustworthy Systems

Provably trustworthy systems


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


University of NSW

UNSW Sydney

University of Melbourne


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

    author           = {Klein, Gerwin and Andronick, June and Keller, Gabriele and Matichuk, Daniel and Murray, Toby and
                        O'Connor, Liam},
    date             = {2017-9-4},
    doi              = {},
    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         = {},
    publisher        = {The Royal Society Publishing},
    title            = {Provably Trustworthy Systems},
    volume           = {375},
    year             = {2017}