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.
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.
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.
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.
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
It's frequently done in research and industry when there's a component that has strict timing and separation requirements, and a bunch of supporting software that doesn't.
Like an autonomous helicopter. Flight control? Very important. A bunch of hardware drivers and services for imaging, navigation, comms... not so much, and not worth the (long term ongoing) effort of replatforming.
I think a scheme as simple as running two Linux VMs, where you have isolated the services that have real-time guarantees into their own VM, lets you benefit from seL4.
This is tangential to your comment, but it's worth mentioning that you can often begin securing a (Linux) system with seL4 by putting the entire system into a VM. Then, you iteratively port components to run "natively" over seL4 -- a process called "cyber retrofit" [0, 1].
BTW, it was probably just a typo but I believe "se" in seL4 is not a shortening of "secure", but an initialism for "secure embedded". Which is why it's not "secL4".
A system with two seL4 tasks, (1) a flight control system, and (2) a VMM running Linux, uses seL4's formally proven safety properties to meet the timing and separation requirements of the critical flight control system... and run a bunch of less critical stuff on Linux that no one wants to rewrite.
Comments
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.
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.
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
"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.
And what would be the point of that?
It's frequently done in research and industry when there's a component that has strict timing and separation requirements, and a bunch of supporting software that doesn't.
Like an autonomous helicopter. Flight control? Very important. A bunch of hardware drivers and services for imaging, navigation, comms... not so much, and not worth the (long term ongoing) effort of replatforming.
I don't understand though. If it's all running on the Linux VM, then you haven't inherited any of the secL4 benefits.
I think a scheme as simple as running two Linux VMs, where you have isolated the services that have real-time guarantees into their own VM, lets you benefit from seL4.
This is tangential to your comment, but it's worth mentioning that you can often begin securing a (Linux) system with seL4 by putting the entire system into a VM. Then, you iteratively port components to run "natively" over seL4 -- a process called "cyber retrofit" [0, 1].
BTW, it was probably just a typo but I believe "se" in seL4 is not a shortening of "secure", but an initialism for "secure embedded". Which is why it's not "secL4".
[0] https://sel4.systems/About/how-to-use.html
[1] https://trustworthy.systems/publications/abstracts/Klein_AKM...
A system with two seL4 tasks, (1) a flight control system, and (2) a VMM running Linux, uses seL4's formally proven safety properties to meet the timing and separation requirements of the critical flight control system... and run a bunch of less critical stuff on Linux that no one wants to rewrite.