Provably trustworthy systems
Philosophical transactions. Series A, Mathematical, physical, and engineering sciences, Volume 375, Issue 2104, 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 compl...More
Full Text (Upload PDF)
PPT (Upload PPT)