seL4: Formal Veriﬁcation of an OS Kernel

By Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish and 3 more. 2009

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

Research Priorities for Robust and Beneficial Artificial Intelligence (2015, background): “Formal veriﬁcation of software has advanced signiﬁ-cantly in recent years: examples include the seL4 kernel [28], a complete, general-purpose operating-system kernel that has been mathematically checked against a formal speciﬁcation to give a strong guarantee against crashes and unsafe operations,…”
Autoformalization with Large Language Models (2022, methodology): “It would reduce the currently excessive cost of formalization efforts [27], and in the long-term it could connect the various research ﬁelds that automate aspects of mathematical reasoning, such as automated theorem proving and computer algebra, to the vast body of mathematical knowledge…”
A FORMAL PROOF OF THE KEPLER CONJECTURE (2015, unknown): “The Flyspeck project has roughly similar size and complexity as other major formalization projects such as the Feit–Thompson odd order theorem [ 9 ], the CompCert project giving a veriﬁed C compiler [ 31 ], and the seL4 project that veriﬁed an operating system microkernel [ 28 ].”
Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers (2022, background): “…the formalisation of complicated mathematical results [Gonthier et al., 2008, Avigad et al., 2007, Gonthier et al., 2013, Scholze, 2021] and operating system kernel veriﬁcation [Klein et al., 2009] are done in interactive theorem provers, often based on higher-order logic or dependent type theory.”
Eliminating the hypervisor attack surface for a more secure cloud (2011, background): “The large code base is not suitable for formal ver-iﬁcation – the best formal veriﬁcation techniques available today are only able to handle around 10K lines of code [18].”
HyperSafe: A Lightweight Approach to Provide Lifetime Hypervisor Control-Flow Integrity (2010, background): “Among them, seL4 [26] recently made signiﬁcant progress.”
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware (2016, background): “Speciﬁcally, the seL4 microkernel [93] has a proof of binary-level functional correctness, as well as proofs of (spatial) conﬁdentiality, availability and integrity enforcement [94].”
A Machine-Checked Proof of the Odd Order Theorem (2013, unknown): “The technology has also been used to verify the correctness of hardware and software components with respect to given speciﬁcations; signiﬁcant successes in that area include the formal proof of correctness of a realistic compiler [32] and of a small operating system [29].”
Why3: Shepherd Your Herd of Provers (2011, methodology): “In the L4.veriﬁed project [18], the Haskell language is used to model the C code of a micro-kernel.”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, unknown): “Like Coq and HOL Light, also Isabelle [14] was used for major formalization e ﬀ orts, such as the formalization of the seL4 microkernel [16].”
Developing Bug-Free Machine Learning Systems With Formal Mathematics (2017, background): “…correctness of machine learning systems requires building on the tools and insights from two distinct ﬁelds: program veriﬁcation (Leroy, 2009; Klein et al., 2009; Chli-pala, 2013; Chen et al., 2015), which has aimed to prove properties of computer programs, and formal mathematics (Rudnicki,…”
The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology (2019, background): “Furthermore full-featured OSes (e.g. Sel4 [10]) provide an additional guaranteed layer of security.”
Shielding Applications from an Untrusted Cloud with Haven (2014, background): “…given a hypervisor that is veriﬁed (down to binary code) to protect guest conﬁdentiality and integrity, so that the attestation a user receives is meaningfully connected to a proof of the isolation mechanism, but current progress on OS-level formal veriﬁcation is some way from this goal [23, 30].”
Verdi: a framework for implementing and formally verifying distributed systems (2015, background): “Previous work has shown that formal veriﬁcation can help produce extremely reliable systems, including compilers [41] and operating systems [18, 39].”
Moat: Verifying Confidentiality of Enclave Programs (2015, background): “While some eﬀorts are under way to build a fully veriﬁed software stack ground-up (e.g. [21, 25]), this approach is unlikely to scale to real-world OS and system software.”
The multikernel: a new OS architecture for scalable multicore systems (2009, methodology): “For Barrelﬁsh, we decided to use a capability system modeled on that of seL4 [39].”
Preliminary design of the SAFE platform (2011, methodology): “Despite recent successes such as seL4 [9], formal veriﬁcation of whole operating systems still requires daunting amounts of eﬀort.”