To add a bit to what Adam wrote

On 6 Nov 2018, at 14:38, Adam.Felizzi@data61.csiro.au wrote:

- Using a camkes system would mean you're working in a static environment. This would mean the number of components in your system (Guest VMM's including) would be static, whilst the ultimate goal of this project sounds like you want to create a dynamic system? Regardless, using the camkes vm would be a good starting point to experiment and build your system. We currently don't have a dynamic system to support launching and shutting down VMs.

If you want something dynamic you should look at Genode, it is a fully dynamic system. Genode has been ported to seL4, although that port is less mature than on other microkernels (but the Genode folks continue to work on this AFAIK).

2. Unfortunately I can't really comment on the feasibility of porting L4Linux to seL4 and what this would specifically gain.

I don’t think this makes sense. L4Linux is a para-virtualised system, I see no benefit from such a port. You want full virtualisation that runs an unmodified Linux binary.

Gernot