It turns out that seL4 already supports running a VM-based Linux on ARMv7 and is pushing toward x86 support, as described in their FAQ:
How good is seL4 at supporting virtual machines?
Can I run Linux on top of seL4?
Yes, seL4 can run Linux in a virtual machine. At present the master branch supports this on ARMv7 processors (presently A15/A7 cores). For x86 there is experimental virtualisation support (requiring Intel VT-x, ETP and a HPET that supports MSI delivery). Please see the roadmap for anticipated release of a mature version.
To support virtual machines, seL4 itself runs as a hypervisor (x86 Ring-0 root mode or ARM hyp mode) and forwards virtualisation events to a virtual machine monitor (VMM) which performs the necessary emulations. The VMM runs de-privileged (x86 Ring-3 root mode or ARM supv mode).
Does seL4 support multiple virtual machines at once?
Yes, multiple VMs are supported, including heterogeneous ones.
In keeping with the spirit of seL4, it might be appropriate to use a “secure” (for some value of secure) Linux, Rust-based commands where possible, etc. That said, I’d think that seL4’s capability-based approach would already provide a fair amount of security.
Can anyone provide more information on the use of Linux and/or Linux ports of applications on Kry10, or more generally, seL4?
-r