Provably trustworthy systems. (13th October 2017)

• Record Type: Journal Article
• Authors: Klein, Gerwin; Andronick, June; Keller, Gabriele; Matichuk, Daniel; Murray, Toby; O'Connor, Liam
• Is Part Of: Philosophical transactions. Volume 375:Number 2104(2017)
• Publication Date: 2017-10-13
• Subjects: seL4 -- proof engineering -- code/proof co-generation -- Cogent; Physical sciences -- Periodicals; Engineering -- Periodicals; Mathematics -- Periodicals; 500
• DOI: 10.1098/rsta.2015.0404
• Languages: English
• ISSNs: 1364-503X

Abstract

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'.