On Sun, Jan 8, 2017 at 10:23 PM,
My tongue in cheek response would be to say that you are doing this backwards and you should be wanting to run Xen on seL4.
At a previous job I was interested in the potential of seL4 as a secure enclave providing cryptographic services to a Linux-based guest. That is not applicable to my current job though. So yes, that's great, and makes more sense than what I'm describing and it's something I've been a fan of, but not applicable to what I'm working on right now. Long-term I am considering the possibility of shipping seL4 on dedicated hardware devices as the only OS with no Linux host or guest. Deploying these services on EC2 would allow us a way to ship seL4 in a production capacity before we have a full hardware solution in place.
More seriously though, what is the value that seL4 is providing in this setup? What are the specific threat scenarios that seL4 is mitigating against? If you are using seL4 to provide isolation of two applications, then since you are already relying on the isolation provided by Xen, why not cut out seL4 and run those two applications directly on Xen?
A "unikernel" deployment of these applications is definitely another option. Explaining exactly what I'd like to do is a bit involved as it requires knowledge of several AWS features including KMS and EC2 roles/instance metadata. I've been talking about it on the Robigalia IRC channel if you'd like to discuss it there. I will say that shipping these services in separate Xen instance would require e.g. a TLS encrypted channel between them. While that's doable, I'd probably prefer for them to just run on the same OS, and would probably just fold them into the same unikernel were I not to use seL4. I agree having a reasonable threat model in place before moving forward on seL4 is a must, and I also understand there's much work to do re: Robigalia and things like capability spaces. -- Tony Arcieri