[seL4] seL4 in an SGX enclave?

Tony Arcieri bascule at gmail.com
Wed Feb 28 05:31:59 AEDT 2018

On Tue, Feb 27, 2018 at 2:02 AM, <Gernot.Heiser at data61.csiro.au> wrote:

> Running seL4 as the trusted base on SGX would be nice. Unfortunately, SGX
> has a major shortcoming (which I told the Intel folks as soon as I saw it
> first): SG enclaves run in Ring 3. Which means there is no protection
> inside an enclave, you have to trust everything in there, and consequently
> seL4 is of no help at all.

I think it'd be fantastic to use seL4 as a sort of "enclave hypervisor",
where enclave(s) can make OCALLs to seL4 to access (from the enclave's
perspective) untrusted services, e.g. speaking to networks or interacting
with filesystems.

If an enclave can OCALL out to communicate to the network, trust can be
established by terminating a cryptographically secure channel protocol
(e.g. TLS, Noise) inside of the enclave. Filesystem access can be similarly
secured by only storing cryptographically authenticated data, e.g. files
encrypted with an AEAD scheme with keys held inside the enclave.

I think it'd be very neat to use seL4 in this way: running one or more
enclaves, and potentially some (untrusted from SGX's perspective) userspace
services that e.g. provide a web UI or other functionality that doesn't
need access to enclave facilities/secrets.

You'd need to effectively reimplement the whole SGX RTS to accomplish this,
but I know at least one person who has already done that (in Rust, as it


Tony Arcieri
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://sel4.systems/pipermail/devel/attachments/20180227/76142463/attachment.html>

More information about the Devel mailing list