SeL4 security proofs now complete on AArch64
80 points by snvzz 3 hours ago | 16 comments
kvuj 2 hours ago
What operating systems use SeL4? I know of the following:
reply- 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?
angry_octet 2 hours ago
The Secure Enclave on iOS devices runs sepOS, and earlier fork of the UNSW/NICTA L4 nano kernel work. Obviously Apple has huge resources to verify their own kernel on their own hardware, but seL4 is likely much more secure. With Apple's appetite for architectural security improvements I think they will eventually move to an seL4 derivative with special hardware security add-ons.
replyThere are a number of talks at the upcoming seL4 summit, but see 2025, e.g. Kry10 KOS.
avadodin 2 hours ago
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.
replySecure–boot virtualization platforms are dime a dozen nowadays.
The one covering side channels is pretty honest:
Information side-channels: this assumption applies to the confidentiality proof only and is not present for functional correctness or integrity. The assumption is that the binary-level model of the hardware captures all relevant information channels. We know this not to be the case. This is not a problem for the validity of the confidentiality proof, but means that its conclusion (that secrets do not leak) holds only for the channels visible in the model. This is a standard situation in information flow proofs: they can never be absolute. As mentioned above, in practice the proof covers all in-kernel storage channels but does not cover timing channels.
So the proof won't be invalidated at it does not cover that particular threat.
Now the question is how useful the is a proof not covering side channels? I'd say pretty useful and it doesn't mean they don't have counter measures for to counter their exploitation, nor that they are not effective, just that a proof of efficiency is out of reach for now.
And then you'd need assurance that the Verilog is faithfully transcribed in the silicon, which is a can of worms in itself.
That said, the big caveat of the whole thing, is that by pushing stuff traditionally considered to be sensitive to user space doesn't solve security or stability, it makes it other people's problem. There's no reason you couldn't do a side channel (or a different kind of) attack against a process that hosts the filesystem.
We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.