SeL4 security proofs now complete on AArch64
snvzz
178 points
39 comments
August 24, 2026
Related Discussions
Found 5 related stories in 49.2ms across 4,281 title embeddings via pgvector HNSW
- Qubes OS Security in the Public Record sciences44 · 86 pts · July 18, 2026 · 51% 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
- GPT-5.6 Sol Ultra produces proof of the Cycle Double Cover Conjecture [pdf] scrlk · 411 pts · July 10, 2026 · 47% similar
- Building an Arch Linux Aarch64 Port for Holo Core losgehts · 13 pts · July 17, 2026 · 47% 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.