Sign up to save your podcasts
Or
Share seL4: Proving a Microkernel in C
Share to email
Share to Facebook
Share to X
Share to email
Share to Facebook
Share to X
Or
seL4: Proving a Microkernel in C
This episode explores the 2009 seL4 paper and why formally verifying an operating-system kernel matters when that kernel sits at the center of every higher-level security claim. It explains how seL4’s microkernel design keeps only core mechanisms like threads, IPC, interrupts, and memory objects in privileged code, contrasting that with monolithic kernels and showing why minimality makes theorem-proving tractable. The discussion digs into the system’s capability-based authority model, CNodes, explicit reply paths, and untyped memory retyping, arguing that seL4 was designed so allocation, mapping, and permissions remain visible enough for proofs to track every state change. Listeners would find it interesting because the episode draws a sharp line between proving functional correctness and proving true end-to-end security, showing both the power and the limits of formal methods in real systems.
Sources:
1. seL4: Proving a Microkernel in C
https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf
2. On Micro-Kernel Construction — Jochen Liedtke, 1995
https://scholar.google.com/scholar?q=On+Micro-Kernel+Construction
3. The Performance of Micro-Kernel-Based Systems — Hermann Hartig, Michael Hohmuth, Jochen Liedtke, Sebastian Schonberg, Jean Wolter, 1997
https://scholar.google.com/scholar?q=The+Performance+of+Micro-Kernel-Based+Systems
4. seL4: Formal Verification of an OS Kernel — Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock and others, 2009
https://scholar.google.com/scholar?q=seL4%3A+Formal+Verification+of+an+OS+Kernel
5. seL4: Formal Verification of an Operating-System Kernel — Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin and others, 2010
https://scholar.google.com/scholar?q=seL4%3A+Formal+Verification+of+an+Operating-System+Kernel
6. Translation Validation for a Verified OS Kernel — Thomas Sewell, Magnus Myreen, Gerwin Klein, 2013
https://scholar.google.com/scholar?q=Translation+Validation+for+a+Verified+OS+Kernel
7. Comprehensive Formal Verification of an OS Microkernel — Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser, 2014
https://scholar.google.com/scholar?q=Comprehensive+Formal+Verification+of+an+OS+Microkernel
8. Kernel Design for Isolation and Assurance of Physical Memory — Dhammika Elkaduwe, Philip Derrin, Kevin Elphinstone, 2008
https://scholar.google.com/scholar?q=Kernel+Design+for+Isolation+and+Assurance+of+Physical+Memory
9. seL4 Enforces Integrity — Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, Gerwin Klein, 2011
https://scholar.google.com/scholar?q=seL4+Enforces+Integrity
10. seL4: From General Purpose to a Proof of Information Flow Enforcement — Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein, 2013
https://scholar.google.com/scholar?q=seL4%3A+From+General+Purpose+to+a+Proof+of+Information+Flow+Enforcement
11. Verified Protection Model of the seL4 Microkernel — Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone, 2008
https://scholar.google.com/scholar?q=Verified+Protection+Model+of+the+seL4+Microkernel
12. Time Protection: The Missing OS Abstraction — Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser, 2019
https://scholar.google.com/scholar?q=Time+Protection%3A+The+Missing+OS+Abstraction
13. Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures — Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su, 2024
https://scholar.google.com/scholar?q=Practical+Rely%2FGuarantee+Verification+of+an+Efficient+Lock+for+seL4+on+Multicore+Architectures
14. Modeling Dynamic (De)Allocations of Local Memory for Translation Validation — Abhishek Rose, Sorav Bansal, 2024
https://scholar.google.com/scholar?q=Modeling+Dynamic+%28De%29Allocations+of+Local+Memory+for+Translation+Validation
15. PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot — Zhuoruo Zhang et al., 2022
https://scholar.google.com/scholar?q=PA-Boot%3A+A+Formally+Verified+Authentication+Protocol+for+Multiprocessor+Secure+Boot
16. Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core — Nils Wistoff et al., 2020
https://scholar.google.com/scholar?q=Prevention+of+Microarchitectural+Covert+Channels+on+an+Open-Source+64-bit+RISC-V+Core
17. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts — Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, Marco Guarnieri, 2023
https://scholar.google.com/scholar?q=Specification+and+Verification+of+Side-channel+Security+for+Open-source+Processors+via+Leakage+Contracts
18. AI Post Transformers: From Natural Language to Verified Dafny Code — Hal Turing & Dr. Ada Shannon, 2026
https://podcast.do-not-panic.com/episodes/2026-06-14-from-natural-language-to-verified-dafny-8abed9.mp3
Interactive Visualization: seL4: Proving a Microkernel in C
View all episodes
By mcgrofThis episode explores the 2009 seL4 paper and why formally verifying an operating-system kernel matters when that kernel sits at the center of every higher-level security claim. It explains how seL4’s microkernel design keeps only core mechanisms like threads, IPC, interrupts, and memory objects in privileged code, contrasting that with monolithic kernels and showing why minimality makes theorem-proving tractable. The discussion digs into the system’s capability-based authority model, CNodes, explicit reply paths, and untyped memory retyping, arguing that seL4 was designed so allocation, mapping, and permissions remain visible enough for proofs to track every state change. Listeners would find it interesting because the episode draws a sharp line between proving functional correctness and proving true end-to-end security, showing both the power and the limits of formal methods in real systems.
Sources:
1. seL4: Proving a Microkernel in C
https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf
2. On Micro-Kernel Construction — Jochen Liedtke, 1995
https://scholar.google.com/scholar?q=On+Micro-Kernel+Construction
3. The Performance of Micro-Kernel-Based Systems — Hermann Hartig, Michael Hohmuth, Jochen Liedtke, Sebastian Schonberg, Jean Wolter, 1997
https://scholar.google.com/scholar?q=The+Performance+of+Micro-Kernel-Based+Systems
4. seL4: Formal Verification of an OS Kernel — Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock and others, 2009
https://scholar.google.com/scholar?q=seL4%3A+Formal+Verification+of+an+OS+Kernel
5. seL4: Formal Verification of an Operating-System Kernel — Gerwin Klein, June Andronick, Kevin Elphinstone, Gernot Heiser, David Cock, Philip Derrin and others, 2010
https://scholar.google.com/scholar?q=seL4%3A+Formal+Verification+of+an+Operating-System+Kernel
6. Translation Validation for a Verified OS Kernel — Thomas Sewell, Magnus Myreen, Gerwin Klein, 2013
https://scholar.google.com/scholar?q=Translation+Validation+for+a+Verified+OS+Kernel
7. Comprehensive Formal Verification of an OS Microkernel — Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, Gernot Heiser, 2014
https://scholar.google.com/scholar?q=Comprehensive+Formal+Verification+of+an+OS+Microkernel
8. Kernel Design for Isolation and Assurance of Physical Memory — Dhammika Elkaduwe, Philip Derrin, Kevin Elphinstone, 2008
https://scholar.google.com/scholar?q=Kernel+Design+for+Isolation+and+Assurance+of+Physical+Memory
9. seL4 Enforces Integrity — Thomas Sewell, Simon Winwood, Peter Gammie, Toby Murray, June Andronick, Gerwin Klein, 2011
https://scholar.google.com/scholar?q=seL4+Enforces+Integrity
10. seL4: From General Purpose to a Proof of Information Flow Enforcement — Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, Gerwin Klein, 2013
https://scholar.google.com/scholar?q=seL4%3A+From+General+Purpose+to+a+Proof+of+Information+Flow+Enforcement
11. Verified Protection Model of the seL4 Microkernel — Dhammika Elkaduwe, Gerwin Klein, Kevin Elphinstone, 2008
https://scholar.google.com/scholar?q=Verified+Protection+Model+of+the+seL4+Microkernel
12. Time Protection: The Missing OS Abstraction — Qian Ge, Yuval Yarom, Tom Chothia, Gernot Heiser, 2019
https://scholar.google.com/scholar?q=Time+Protection%3A+The+Missing+OS+Abstraction
13. Practical Rely/Guarantee Verification of an Efficient Lock for seL4 on Multicore Architectures — Robert J. Colvin, Ian J. Hayes, Scott Heiner, Peter Höfner, Larissa Meinicke, Roger C. Su, 2024
https://scholar.google.com/scholar?q=Practical+Rely%2FGuarantee+Verification+of+an+Efficient+Lock+for+seL4+on+Multicore+Architectures
14. Modeling Dynamic (De)Allocations of Local Memory for Translation Validation — Abhishek Rose, Sorav Bansal, 2024
https://scholar.google.com/scholar?q=Modeling+Dynamic+%28De%29Allocations+of+Local+Memory+for+Translation+Validation
15. PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot — Zhuoruo Zhang et al., 2022
https://scholar.google.com/scholar?q=PA-Boot%3A+A+Formally+Verified+Authentication+Protocol+for+Multiprocessor+Secure+Boot
16. Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core — Nils Wistoff et al., 2020
https://scholar.google.com/scholar?q=Prevention+of+Microarchitectural+Covert+Channels+on+an+Open-Source+64-bit+RISC-V+Core
17. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts — Zilong Wang, Gideon Mohr, Klaus von Gleissenthall, Jan Reineke, Marco Guarnieri, 2023
https://scholar.google.com/scholar?q=Specification+and+Verification+of+Side-channel+Security+for+Open-source+Processors+via+Leakage+Contracts
18. AI Post Transformers: From Natural Language to Verified Dafny Code — Hal Turing & Dr. Ada Shannon, 2026
https://podcast.do-not-panic.com/episodes/2026-06-14-from-natural-language-to-verified-dafny-8abed9.mp3
Interactive Visualization: seL4: Proving a Microkernel in C