Comment by wmf
5 hours ago
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.
5 hours ago
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.