The seL4 Foundation – growing through upheaval
summary
seL4 is a ~10–15k line C microkernel with machine-checked proofs of functional correctness, binary translation and security enforcement, open-sourced under GPLv2 in 2014 and claimed as the fastest L4 (2–3× faster than peers, ~10× faster than Zircon in published benchmarks). Real-world demos include DARPA helicopter and quadcopter challenges where attackers cannot escape a compromised VM. Foundation forms April 2020, survives a May 2021 near-death when CSIRO cuts funding, bridged by UNSW and then grows membership and budget (membership revenue ×10) while some boot and multicore proofs remain outstanding.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:10Welcome
- 1:45What is SE4
- 3:33Mathematical proof story
- 8:09Performance analysis
- 9:26Microkernel
- 11:23What has seL4 completed
- 14:08What happened in May 21
- 17:03What does life look like now
- 22:14The influx of talent
- 28:21The budget
- 30:54The community
- 34:39Industry consortium
- 35:35Research
- 36:28Conclusion
related talks
45mVerified seL4 on secure RISC-V processors
01h 03mKEYNOTE: From quadcopters to helicopters
45mThe Future of Security is in Open Silicon
27mKeynote: Jim Zemlin
21mHarmonizing Performance and Isolation in Microkernels with Efficient Intra-kernel
19mAn Open Source Approach to System Security
18mKeynote: Bianca Lewis, Executive Director, OpenSearch Software Foundation, The Linux Foundation
33mState of Linux