Skip to main page content
U.S. flag

An official website of the United States government

Dot gov

The .gov means it’s official.
Federal government websites often end in .gov or .mil. Before sharing sensitive information, make sure you’re on a federal government site.

Https

The site is secure.
The https:// ensures that you are connecting to the official website and that any information you provide is encrypted and transmitted securely.

Access keys NCBI Homepage MyNCBI Homepage Main Content Main Navigation
. 2017 Oct 13;375(2104):20150404.
doi: 10.1098/rsta.2015.0404.

Provably trustworthy systems

Gerwin Klein  1   2 , June Andronick  3   2 , Gabriele Keller  3   2 , Daniel Matichuk  3   2 , Toby Murray  3   4 , Liam O'Connor  2
Affiliations

Provably trustworthy systems

Gerwin Klein et al. Philos Trans A Math Phys Eng Sci. .

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: Cogent; code/proof co-generation; proof engineering; seL4.

PubMed Disclaimer

Conflict of interest statement

The authors have no competing interests.

Figures

Figure 1.
Figure 1.
seL4 provides isolation. (Online version in colour.)
Figure 2.
Figure 2.
Simplified seL4 verification artefact overview. (Online version in colour.)
Figure 3.
Figure 3.
The relationship of OS properties to safety and security. (Online version in colour.)
Figure 4.
Figure 4.
Article size in lines of proof in the AFP by submission date compared with four-colour theorem, odd-order theorem, Verisoft, seL4 (rightmost four). (Online version in colour.)
Figure 5.
Figure 5.
COSMIC function point versus artefact size (a,c,e) and artefact size (b,d,f) relationships. Each point is an seL4 API function. (a) Functionality versus abstract spec. (ρ = 0.31, p = 0.09), (b) executable spec. versus abstract spec. (ρ = 0.89, p = 0.00), (c) functionality versus executable spec. (R = 0.15, p = 0.42), (d) executable spec. versus C (R = 0.95, p = 0.00), (e) functionality versus C (R = 0.19, p = 0.32) and (f) abstract spec. versus C (ρ = 0.92, p = 0.00).
Figure 6.
Figure 6.
Proof size versus effort. (a) Scatter plot of project total effort in person-weeks versus final size in lines of proof (R2 = 0.914, p < 0.001) and (b) scatter plot of total effort (person-weeks) versus sum of repo-delta size (lines of proof) of all changes made in the 24 individual contributions to the four proofs and the specification (R2 = 0.93, p < 0.001).
Figure 7.
Figure 7.
Relationships between idealized statement size and proof size for the six projects analysed.
Figure 8.
Figure 8.
Code/proof co-generation with Cogent. (Online version in colour.)
Figure 9.
Figure 9.
Looking up an inode in ext2fs, in Cogent. (Online version in colour.)
See this image and copyright information in PMC

References

    1. Leroy X. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 107–115. ( 10.1145/1538788.1538814) - DOI
    1. Leroy X. 2009. A formally verified compiler back-end. J. Autom. Reason. 43, 363–446. ( 10.1007/s10817-009-9155-4) - DOI
    1. Klein G, et al. 2009. seL4: formal verification of an OS kernel. In Proc. 22nd ACM Symp. on Operating Systems Principles, Big Sky, MT, 11–14 October, pp. 207–220. New York, NY: ACM.
    1. Klein G, Andronick J, Elphinstone K, Murray T, Sewell T, Kolanski R, Heiser G. 2014. Comprehensive formal verification of an OS microkernel. ACM Trans. Comput. Syst. 32, 2:1–2:70. ( 10.1145/2560537) - DOI
    1. The seL4 microkernel code and proofs See https://github.com/seL4/.

LinkOut - more resources