Hi Justin,
I'm really sorry for the delayed response, I hope this hasn't deterred you from the project. Docker on seL4 sounds like a really interesting project and we would be keen to hear of any progress.
I can provide high level comments on some of the mentioned approaches:
1. Building you system with the camkes vm project would probably be the easiest approach for getting Docker running on seL4. This would probably be an ideal starting point for the project. Were you envisioning of running the Docker cli and engine in a Linux VM and having Docker containers run as different VM guests on seL4? I'm aware of other projects that have looked into providing a similar Docker runtime on KVM and Xen (such as https://github.com/gotoz/runq/ & https://github.com/hyperhq/hyperd). There are some limitations to this approach however:
- 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.
- The X86 Camkes VM project currently supports multiple VMM's. We currently don't have any demo systems available for multiple aarch64 VMMs. We are currently looking into improving our virtualization support and this is something we can further update you on. It may be easier to prototype in a X86 environment in the meantime.
2. Unfortunately I can't really comment on the feasibility of porting L4Linux to seL4 and what this would specifically gain.
3. This approach is hard to scope as I'm not 100% clear on the dependencies of Docker and its libraries. More specifically if you want to look into supporting Golang on seL4, an approach that may help to get things running could involving using Rumprun (https://github.com/SEL4PROJ/rumprun-sel4-demoapps). The Rumprun unikernel may provide the syscall and OS support the Golang runtime needs. This could be a first step to support Docker as a seL4 service.
I hope some of this helps. Please don't hesitate to ask any further questions.
Kind Regards,
Adam
________________________________________
From: Devel