Post #2985143
2026-05-12 03:50 UTC
Replies (1)
-
@david_chisnall@infosec.exchange 2026-05-12 08:50
@bob_zim@infosec.exchange @bignose@social.chinwag.org @stilgherrian@eigenmagic.net seL4 is formally verified and went almost 24 hours between being open sourced and the first security vulnerability being reported. That one was because the verification didn't cover all of the code, but seL4's verification was also done against a quiet simplified model of an MMU, so there may be other soundness issues. My favourite verification story is when some colleagues adopted EverCrypt in a previous job. EverCrypt is verified against a bunch of properties (including constant time execution). It is also proven to be memory safe. They expressed temporal safety as a property that no object is accessed after it was freed. It turned out that the codebase complied with this trivially: it never freed memory. Oh, and the proofs treat as axiomatic that the C code calling the APIs has no memory safety bugs.