seL4: Formal Verification of an OS Kernel¶
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., et al. (2009). seL4: Formal Verification of an OS Kernel. Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, 207-220.
Cited by¶
3 citations across 3 artifacts.
Each citation links to the sentence it supports in the citing article.
Primes¶
- Mathematical Induction
- … proving**, induction is a central proof tactic in Coq, Isabelle, Lean, Agda, and ACL2; the Boyer-Moore family of provers (Nqthm, ACL2) introduced sophisticated heuristics for selecting induction principles, generalising goals, and guessing inductive variables; industrial-scale verified software (the seL4 microkernel
This sourceACM. End-to-end functional-correctness proof of an OS microkernel; demonstrates that strict isolation between kernel and user space concentrates analytical complexity into a small bounded region, making formal verification tractable.
- … proving**, induction is a central proof tactic in Coq, Isabelle, Lean, Agda, and ACL2; the Boyer-Moore family of provers (Nqthm, ACL2) introduced sophisticated heuristics for selecting induction principles, generalising goals, and guessing inductive variables; industrial-scale verified software (the seL4 microkernel
- Sequestration
- Sequestration simplifies system analysis by partitioning hazardous or sensitive elements into dedicated, bounded analysis domains. Klein et al. (2009) demonstrate this analytical economy concretely with the seL4 microkernel: by formally isolating untrusted user-space code from a small verified kernel, the proof obligation shrinks to roughly 8,700 lines of C, enabling end-to-end functional-correctness verification that would be intractable in a monolithic system.
This sourceACM. End-to-end functional-correctness proof of an OS microkernel; demonstrates that strict isolation between kernel and user space concentrates analytical complexity into a small bounded region, making formal verification tractable.
- Sequestration simplifies system analysis by partitioning hazardous or sensitive elements into dedicated, bounded analysis domains. Klein et al. (2009) demonstrate this analytical economy concretely with the seL4 microkernel: by formally isolating untrusted user-space code from a small verified kernel, the proof obligation shrinks to roughly 8,700 lines of C, enabling end-to-end functional-correctness verification that would be intractable in a monolithic system.
Domain-specific¶
- Formal Verification
- … profile: hardware circuit verification (Intel's formal verification program after the 1994 FDIV bug; ARM's processor cores; cache-coherence protocol checking at IBM), safety-critical software (the CompCert verified C compiler; the seL4 formally verified microkernel, proved in Isabelle/HOL in roughly 20 person-years
This sourceThe machine-checked functional-correctness proof of the seL4 microkernel in Isabelle/HOL, at a total effort of about 20 person-years.
Supported in partVerified against the source
- … profile: hardware circuit verification (Intel's formal verification program after the 1994 FDIV bug; ARM's processor cores; cache-coherence protocol checking at IBM), safety-critical software (the CompCert verified C compiler; the seL4 formally verified microkernel, proved in Isabelle/HOL in roughly 20 person-years
Verification¶
Does it exist? Confirmed. This work's DOI resolves to a registered record, which fixes its identity. That is all it fixes.
Does it back the claim? Read against the text for 1 of 3 citations: 1 supported in part. Each verdict is shown under its citation below, with what in the work backs the sentence.
Was it audited? Yes. A second, independent pass read the citation against the article text and recorded a verdict.
Support is checked per citation rather than per work — the same source can be cited soundly in one article and wrongly in another. Per-citation recording began recently, so a citation with no recorded check is a gap in the record rather than evidence it went unchecked.
See how references were verified.
Registry ID ref:46934e813fdd · see in the full table