Automatic Enforcement of Expressive Security Policies using Enclaves
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.
Thu 3 Nov
|10:30 - 10:55|
|10:55 - 11:20|
|11:20 - 11:45|
Daniele BonettaOracle Labs, Luca SalucciUniversità della Svizzera italiana (USI), Stefan MarrJohannes Kepler University Linz, Walter BinderUniversity of LuganoDOI
|11:45 - 12:10|
Arthur Michener PetersThe University of Texas at Austin, Texas, USA, David KitchinGoogle, Inc., John A. ThywissenThe University of Texas at Austin, William CookUT AustinDOI Pre-print