3 ms·

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

by jdub 1mo ago

avadodin 1mo ago
A real OS user-land kernel handling real workloads within the capability model. A Linux VM isn't it.
adastra22 1mo ago
And what would be the point of that?
- jdub 1mo ago
  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.
  - adastra22 1mo ago
    I don't understand though. If it's all running on the Linux VM, then you haven't inherited any of the secL4 benefits.
    - spectra2 1mo ago
      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 https://sel4.systems/About/how-to-use.html [1] https://trustworthy.systems/publications/abstracts/Klein_AKMHF_18.abstract https://trustworthy.systems/publications/abstracts/Klein_AKM...
    - jdub 1mo ago
      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.

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

by jdub 1mo ago

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

avadodin 1mo ago

A real OS user-land kernel handling real workloads within the capability model. A Linux VM isn't it.

adastra22 1mo ago

And what would be the point of that?

jdub 1mo ago
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.
- adastra22 1mo ago
  I don't understand though. If it's all running on the Linux VM, then you haven't inherited any of the secL4 benefits.
  - spectra2 1mo ago
    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 https://sel4.systems/About/how-to-use.html [1] https://trustworthy.systems/publications/abstracts/Klein_AKMHF_18.abstract https://trustworthy.systems/publications/abstracts/Klein_AKM...
  - jdub 1mo ago
    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.