Proposed future Core Platform extension: hosting other seL4-native OSs
While reading Andrew’s message on syscall origin checking, I realized that UX/RT could potentially replace Linux VMs in Core Platform applications. I imagine that this would require changes to both the Core Platform and UX/RT. Andrew, would you be interested in adding a hosting interface to UX/RT, so that static systems such as the Core Platform can use UX/RT as a Linux VM replacement? UX/RT seems like a fantastic alternative, with both better security and (eventually) better performance. I would imagine that it also would use less memory than a Linux VM. Gernot (and the rest of the seL4 team): would it be possible to support running other seL4-based systems as protection domains in a future version of the Core Platform? Such systems would be opaque from the Core Platform’s perspective, but they might need capabilities that normal protection domains are not provided. Of course, they would not be granted any capabilities that would allow them to violate system security. Yes, I know that one can run seL4 in a VM, but it seems rather wasteful to do so. Sincerely, Demi
On 23 Nov 2020, at 05:34, Demi M. Obenour
Gernot (and the rest of the seL4 team): would it be possible to support running other seL4-based systems as protection domains in a future version of the Core Platform? Such systems would be opaque from the Core Platform’s perspective, but they might need capabilities that normal protection domains are not provided. Of course, they would not be granted any capabilities that would allow them to violate system security.
Yes, I know that one can run seL4 in a VM, but it seems rather wasteful to do so.
I don’t think I understand what you’re after. You want to run an seL4 system on seL4? That would be some form of virtualisation. Rather than platform virtualisation (which is what we usually mean when talking VMs) one can virtualise at the seL4 ABI, basically interposing syscalls by virtualising all caps. Being virtualisable is a standard property of cap systems, and achieved by the opaqueness of caps. If someone gives you a cap to a TCB, you have no way of telling that it is indeed a TCB cap. It can be an EP cap, which invokes an emulation server that implements the operations on the virtualised TCB. seL4 is presently not fully virtualisable in this sense, as the yield() syscall is invoked without a cap. I’ve long been thinking we should change this, but there wasn’t enough incentive for it. In any case, this is completely outside the scope of this RFC. Gernot
On 11/22/20, Demi M. Obenour
Andrew, would you be interested in adding a hosting interface to UX/RT, so that static systems such as the Core Platform can use UX/RT as a Linux VM replacement? UX/RT seems like a fantastic alternative, with both better security and (eventually) better performance. I would imagine that it also would use less memory than a Linux VM.
I didn't have any plans to add support for co-hosting with any other system to UX/RT. Adding support for running as a non-root task to the process server would very likely add significant complexity. Handling IPC between UX/RT and external threads would also probably add significant complexity since UX/RT won't expose any of the raw kernel API to user processes (message passing will be only exposed through the transport layer, and memory capabilities will be managed exclusively by the process server).
participants (3)
-
Andrew Warkentin -
Demi M. Obenour -
Heiser, Gernot (Data61, Kensington NSW)