Blogs (9) >>
Sun 30 October - Fri 4 November 2016 Amsterdam, Netherlands
Thu 3 Nov 2016 10:30 - 10:55 at Matterhorn 2 - Language Design and Programming Models II Chair(s): Olivier Tardieu

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
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: Language Design and Programming Models IIOOPSLA at Matterhorn 2
Chair(s): Olivier TardieuIBM Research
10:30 - 10:55
Anitha Gollamudi, Stephen ChongHarvard University
10:55 - 11:20
Alexei ColinCarnegie Mellon University, Brandon LuciaCarnegie Mellon University
DOI Pre-print
11:20 - 11:45
Daniele BonettaOracle Labs, Luca SalucciUniversità della Svizzera italiana (USI), Stefan MarrJohannes Kepler University Linz, Walter BinderUniversity of Lugano
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 Austin
DOI Pre-print