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.