The seL4 verification: the art and craft of proof and the reality of commercial s
summary
A formally verified seL4 microkernel exists end-to-end: a C implementation of roughly 500 functions (10–15k LOC originally) is proved correct against an abstract state‑monad spec using Isabelle/HOL and forward simulation, with integrity and non‑interference confidentiality proofs and binary agreement via translation validation of compiler output. The proofs target real platforms (ARM32, RISC‑V64, x86 variants), support is commercialized through a foundation and Proofcraft, continuous integration tracks proof breakage, and mixed‑criticality support is still under verification.
AI-written summary · about
chapters (19)
- 0:00Introduction
- 4:50Mission Impossible
- 5:35Micro Kernel
- 9:15The foundational techniques
- 9:55What is seL4
- 16:23Isolation
- 17:10Expectations
- 19:30What does it bring
- 24:01Scope of verification
- 28:43Formal verification
- 30:50Trustedness
- 33:15The proof stack
- 34:58The options
- 40:12I want it now
- 42:55What weve learned
- 46:23Summary
- 47:19Positive angle
- 48:30Questions
- 54:28Continuous integration
related talks
01h 04mSoftware Verification meets Real-World Cryptography
01h 00mCooperative Verification: Towards Reliable Safety-Critical Systems
16mTowards formally secure compilation of verified F* programs against unverified ML(…)
29müberSpark: Enforcing Verifiable Object Abstractions for Automated...
17mCode-Specify-Test-Debug-Prove: Flexibly Integrating Separation Logic Specification into(…)
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
27mC4: verified transactional objects
47mHow to trust a verified program?