Provably trustworthy systems
Publication date
2017-10-13
Authors
Klein, Gerwin
Andronick, June
Keller, Gabriele
Matichuk, Daniel
Murray, Toby
O’Connor, Liam
Editors
Advisors
Supervisors
Document Type
Article
Metadata
Show full item recordCollections
License
Abstract
We present recent work on building and scaling trustworthy systems with formal, machine-checkable proof from the ground up, including the operating system kernel, at the level of binary machine code. We first give a brief overview of the seL4 microkernel verification and how it can be used to build verified systems. We then show two complementary techniques for scaling these methods to larger systems: proof engineering, to estimate verification effort; and code/proof co-generation, for scalable development of provably trustworthy applications. This article is part of the themed issue ‘Verified trustworthy software systems’.
Keywords
Code/proof co-generation, Cogent, Proof engineering, SeL4, General Mathematics, General Engineering, General Physics and Astronomy
Citation
Klein, G, Andronick, J, Keller, G, Matichuk, D, Murray, T & O’Connor, L 2017, 'Provably trustworthy systems', Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol. 375, no. 2104, 20150404. https://doi.org/10.1098/rsta.2015.0404