On 12/1/20 11:07 PM, Andrew Warkentin wrote:
Am I correct to assume that support for running 32-bit code on a 64-bit kernel using compatibility mode rather than virtualization and support for (presumably limited) direct system calls from VMs, bypassing any user-mode VMM (using something like Xen's trampoline page) wouldn't be accepted into seL4?
These are yet more things that I am going to want at some point and can't think of any other way to do them (besides adding them to the kernel) without significant penalties to hardware compatibility (in the case of the 32-bit support; while UX/RT will mostly be focused on 64-bit systems, it will support 32-bit Linux programs in its compatibility layer) or performance (in the case of direct kernel traps from VMs; I am planning to write a dynamic general-purpose hypervisor to go with UX/RT eventually, and adding an extra trap into the VMM on every IPC would likely add a fair bit of overhead).
Running seL4 in a VM is probably not a good idea, since seL4 does not support making hypercalls itself. I believe that running seL4 in an seL4-based VMM is also of limited practical value, since seL4 natively supports OS-level virtualization. Specifically, since the seL4 API has no ambient authority whatsoever, there is no way for an OS running on seL4 to determine if there are additional resources (such as hardware devices) that have not been assigned to it, nor (if I understand correctly) to distinguish a real device form an emulated one. That said, a set of userland utilities to run multiple seL4-based systems on the same kernel would could arguably be considered a hypervisor, and I consider it quite practical. There may also be cases where the extra layer of page tables used in a VM are necessary for some reason. The only one I can think of is to prevent physical addresses from being leaked, since obtaining them is a prerequisite to Rowhammer attacks. Sincerely, Demi