Comment by simiones
9 hours ago
> but they need a native seL4/Linux if they want to honestly claim they are improving systems' security with their capability model.
Are you using "seL4/Linux" in the style of "GNU/Linux"? Because then it should be "GNU/seL4" - that would describe an OS exposing the GNU core utilities on top of the seL4 kernel. There's no way to mix the Linux kernel with the seL4 kernel, other than using one to run VMs of the other.
https://en.wikipedia.org/wiki/L4Linux
Per that link, this runs a Linux kernel as a VM on top of an L4-based hypervisor.
I mean something like MkLinux with seL4 at its core with all processes and drivers running under seL4 and taking advantage of the seL4 capability model.
It doesn't even have to be a Linux–compatible OS in theory although that is the standard to beat.
But running Linux on top of seL4 does not take advantage of the capability model at all. You need a new non-unix-like userspace for that.
Just securing the whole billion lines of Linux kernel code would make a huge difference even if the user-land ABI remains the same.
The difference with a VM is that Linux is privileged vs the Linux user-land where most interesting things happen so a vulnerability within that blob is as critical as it was before other than for the few modules that are placed in seL4 custody.
For embedded applications, the Linux part is often just used to display a UI so the criticality math is a bit different.