seL4 security proofs now complete on AArch64
Proofcraft has completed the formal proof that the seL4 microkernel enforces confidentiality on AArch64, the final piece of the security isolation proofs for that architecture. This means applications running on seL4 are mathematically guaranteed to be unable to access information without authorization. The milestone, supported by the UK's NCSC, completes the full security proof stack for 64-bit Arm, preventing attacks from propagating between critical and non-critical applications. The company also announced progress on MCS verification for RISC-V and a new dynamic domain scheduler API.
This isolation prevents attacks on non-critical applications from propagating to critical applications and compromising them.
- 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"
- 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?
- 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.