SeL4 security proofs now complete on AArch64

Coming soon: a side-channel timing attack which completely invalidates this result

Read the fine print, "non-MCS (mixed criticality systems), unicore"

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?

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.