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 devel-bounces@sel4.systems on behalf of Jia He jiakernel2@gmail.com Sent: Monday, 17 September 2018 5:25 PM To: devel@sel4.systems Subject: [seL4] run docker on sel4

Hi all

I am new comer to sel4 community. I knew a little bit virtualisation infrastructe(kvm/qemu), but I know little about sel4/docker.

I am investigating the proper implemenatation for running docker on sel4 on arm64.

There might several ways I can figure out.Any suggestions are welcome :-) 1. run linux on sel4 vmm (camkes_vm) and run docker on linux. This might be the easiest way. It might have worked well on X86 2. porting l4linux to sel4. Don't know whether it is feasible? 3. run docker as sel4 service without linux. On this way, golang and its library should be ported to sel4. Some missed syscalls which are needed by docker should be implemenated.

Is there any other ways or anything else to make the implatation more feasible?

--- Cheers, Justin

_______________________________________________ Devel mailing list Devel@sel4.systems https://sel4.systems/lists/listinfo/devel