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