Provably trustworthy systems
2017
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:
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
65
References
5
Citations
NaN
KQI