Journal article
Provably trustworthy systems
G Klein, J Andronick, G Keller, D Matichuk, T Murray, L O’Connor
Philosophical Transactions of the Royal Society A Mathematical Physical and Engineering Sciences | ROYAL SOC | Published : 2017
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’.
Grants
Awarded by Defense Advanced Research Projects Agency
Funding Acknowledgements
The following note applies to 4 and partially 2. This material is based on research sponsored by the Air Force Research Laboratory and the Defense Advanced Research Projects Agency (DARPA) under agreement number FA8750-12-9-0179. The US Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon. The views and conclusions contained herein are those of the authors and should not be interpreted as necessarily representing the official policies or endorsements, either expressed or implied, of the Air Force Research Laboratory, the Defense Advanced Research Projects Agency or the US Government.