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