seL4: formal verification 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

1,992 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computer Networks and Communications, Hardware and Architecture

How researchers see this paper

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

In Artificial Intelligence

In Computer Networks and Communications

In Hardware and Architecture

Citations in the corpus

Research Priorities for Robust and Beneficial Artificial Intelligence (2015, methodology): “Formal verification of software has advanced significantly in recent years: examples include the seL4 kernel (Klein et al. 2009), a complete, general-purpose operating-system kernel that has been mathematically checked against a formal specification to give a strong guarantee against crashes and uns”
NOVA: a microhypervisor-based secure virtualization architecture (2010, methodology): “Inspired by EROS [32], recent microkernels introduced capabilities for controlling access to kernel objects [3, 19, 21, 33].”
Developing Bug-Free Machine Learning Systems With Formal Mathematics (2017, neutral): “Proving 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,…”
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.”
HOList: An Environment for Machine Learning of Higher-Order Theorem Proving (extended version) (2019, methodology): “Like Coq and HOL Light, also Isabelle [14] was used for major formalization efforts, such as the formalization of the seL4 microkernel [16].”
Formal certification of code-based cryptographic proofs (2009, methodology): “2010], or complex software systems, such as operating systems [Klein et al. 2009], virtual machines [Klein and Nipkow 2006] and optimizing compilers [Leroy 2006].”
Hypervision Across Worlds: Real-time Kernel Protection from the ARM TrustZone Secure World (2014, methodology): “Another method to do system protection without relying on the hypervisor is to use a thin privileged software layer, such as microhypervisors [36,40,53] or formally verified microkernels [34].”
Premise Selection for Theorem Proving by Deep Graph Embedding (2017, background): “It not only constitutes a key aspect of general intelligence, but also underpins a broad set of applications ranging from circuit design to compilers, where it is critical to verify the correctness of a computer system [2, 3, 4].”
History of Interactive Theorem Proving (2014, methodology): “Subsequently several other versions of HOL were written, including HOL Light, a version with a simplified axiomatization and rationalized structure written in CAML Light by one of the present authors and subsequently ported to OCaml [Harrison, 2006a], and Isabelle/HOL, described in more detail in th”
Uniform Coherence (2016, background): “Formal logic is a tool that is particularly well-suited for making claims about computations, such as claims of the form “this computation will halt and produce a number larger than 7” or “this computation will use less memory than that computation” or “this operating system’s scheduler will not dea”
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.”
A FORMAL PROOF OF THE KEPLER CONJECTURE (2015, methodology): “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 verified C compiler [31], and the seL4 project that verifi d an operating system micro-kernel [28].”
A Formal Foundation for Secure Remote Execution of Enclaves (2017, methodology): “The seL4 project [33, 47] proves isolation and information flow enforcement in the seL4 microkernel using the Isabelle/HOL proof assistant [49].”
Sanctum: Minimal Hardware Extensions for Strong Software Isolation (2016, background): “In stark contrast, the seL4 formal verification effort [29] spent 20 man-years to cover 9,000 lines of code.”
Preliminary design of the SAFE platform (2011, background): “Despite recent successes such as seL4 [9], formal verification of whole operating systems still requires daunting amounts of effort.”