SeL4 security proofs now complete on AArch64
snvzz
178 points
39 comments
August 24, 2026
Related Discussions
Found 5 related stories in 105.8ms across 8,906 title embeddings via pgvector HNSW
- Qubes OS Security in the Public Record sciences44 · 86 pts · July 18, 2026 · 51% similar
- Two ARM64-specific compiler optimization bugs, in GCC 15/16 and Rust, hit curl torutofu · 51 pts · October 06, 2026 · 49% similar
- OSS-SEC: 432 Linux kernel CVEs (in less than 32 hours) refp · 14 pts · July 22, 2026 · 48% similar
- AI-generated, Lean-verified proof of Collatz conjecture exploits Lean kernel bug YeGoblynQueenne · 14 pts · July 30, 2026 · 48% similar
- Compiler Can Undo Your Security Checks birdculture · 28 pts · September 12, 2026 · 48% similar
Discussion Highlights (4 comments)
kvuj
What operating systems use SeL4? I know of the following: - GenodeOS - LionsOS - A chinese car maker was using it as a hypervisor in their cars, IIRC - What else? Are there any private deployments you guys are aware of?
StilesCrisis
Coming soon: a side-channel timing attack which completely invalidates this result
i_am_a_peasant
Read the fine print, "non-MCS (mixed criticality systems), unicore"
avadodin
The embedded and military markets may keep funding them for the foreseeable future but they need a native seL4/Linux if they want to honestly claim they are improving systems' security with their capability model. Secure–boot virtualization platforms are dime a dozen nowadays.