SeL4 security proofs now complete on AArch64

159 points - today at 11:32 AM

Source

Comments

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.