Comment by avadodin

10 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.

Secure–boot virtualization platforms are dime a dozen nowadays.

9 comments

avadodin

Reply
simiones  8 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.

  • avadodin  7 hours ago

    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.

    • 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.

boredatoms  8 hours ago

The current value is that you can take an existing specialist/military device that used distinct physical chips for provable isolation, and consolidate them all onto one chip (lowering cost/power/space), while still saying that you met the security requirements

So its more of an economic argument than that of increasing security

jdub  10 hours ago

"native seL4/Linux"? seL4 can already host Linux VMs, and there are various methods of running Linux code / binaries without hardware virtualisation.