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.
That's a bit unfair. Any side–channel attack that invalidates seL4 security guarantees —assuming the proofs are valid— also invalidates any other imaginable OS'.
We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.
Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.
Mathematical proofs tend to assume that they are built on perfect foundations (you have to stop the proof somewhere!). Unfortunately, proving that the software is correct just means you need to find a flaw in a deeper layer.
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.
"native seL4/Linux"? seL4 can already host Linux VMs, and there are various methods of running Linux code / binaries without hardware virtualisation.
A real OS user-land kernel handling real workloads within the capability model.
A Linux VM isn't it.
Coming soon: a side-channel timing attack which completely invalidates this result
That's a bit unfair. Any side–channel attack that invalidates seL4 security guarantees —assuming the proofs are valid— also invalidates any other imaginable OS'.
We're in the philosophical territory of tasking infallible beings with stopping their own flawless creations.
Are timing (over network) attacks, physical access, etc. typically excluded from research like this for being “out of scope”, so to speak? I’m not familiar.
Mathematical proofs tend to assume that they are built on perfect foundations (you have to stop the proof somewhere!). Unfortunately, proving that the software is correct just means you need to find a flaw in a deeper layer.
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?