Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance. I was curious about the possibility of using seL4 as the host OS for a "unikernel"-like deployment of a Rust application split into a small set of services living in different capability spaces (e.g. network, key storage / crypto) -- Tony Arcieri
On Sat, Jan 7, 2017 at 6:11 AM, Tony Arcieri
Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance.
I'm mucking about with a Xen/HVM port at the moment, with EC2 as the ultimate target. Will hit the list when there's something useful to show.
Hi Tony, 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. 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? Not trying to discourage the proliferation on seL4, but we have not yet seen a compelling reason to want to run seL4 under something like Xen, which is part of the reason why we have made no effort to support it. Adrian On Sat 07-Jan-2017 6:11 AM, Tony Arcieri wrote: Has anyone managed to run seL4 as a Xen HVM guest? I was more specifically curious about running seL4 on an EC2 instance. I was curious about the possibility of using seL4 as the host OS for a "unikernel"-like deployment of a Rust application split into a small set of services living in different capability spaces (e.g. network, key storage / crypto) -- Tony Arcieri _______________________________________________ Devel mailing list Devel@sel4.systemsmailto:Devel@sel4.systems https://sel4.systems/lists/listinfo/devel
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
participants (3)
-
Adrian.Danis＠data61.csiro.au -
Jeff Waugh -
Tony Arcieri