SeL4 security proofs now complete on AArch64
159 points - today at 11:32 AM
SourceComments
StilesCrisis today at 12:24 PM
Coming soon: a side-channel timing attack which completely invalidates this result
i_am_a_peasant today at 12:33 PM
Read the fine print, "non-MCS (mixed criticality systems), unicore"
kvuj today at 12:23 PM
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 today at 12:34 PM
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.