Hardware-based enclave protection mechanisms, such as Intel’s
SGX, ARM’s TrustZone, and Apple’s Secure Enclave,
can protect code and data from powerful low-level attackers.
In this work, we use enclaves to enforce strong application-specific
information security policies.

We present $IMP_E$, a novel calculus that captures the
essence of SGX-like enclave mechanisms, and show that a
security-type system for $IMP_E$ can enforce expressive confidentiality
policies (including erasure policies and delimited
release policies) against powerful low-level attackers,
including attackers that can arbitrarily corrupt non-enclave
code, and, under some circumstances, corrupt enclave code.
We present a translation from an expressive security-typed
calculus (that is not aware of enclaves) to $IMP_E$. The
translation automatically places code and data into enclaves
to enforce the security policies of the source program.