Max-Planck-Institut für Informatik
max planck institut
mpii logo Minerva of the Max Planck Society

MPI-INF or MPI-SWS or Local Campus Event Calendar

<< Previous Entry Next Entry >> New Event Entry Edit this Entry Login to DB (to update, delete)
What and Who
Title:Securing enclaves with formal verification
Speaker:Andrew Baumann
coming from:Microsoft Research, Redmond
Speakers Bio:Andrew Baumann is a researcher in the Systems Group at Microsoft Research, Redmond. His research interests include operating systems,

distributed systems, and systems security. Recent research highlights include the Barrelfish multikernel OS, Drawbridge LibOS, and Haven
trusted cloud platform. He was previously at The University of New South Wales (BE/PhD)and ETH Zurich (postdoc).

Event Type:SWS Colloquium
Visibility:D1, D2, D3, D4, D5, SWS, RG1, MMCI
We use this to send out email in the morning.
Level:AG Audience
Date, Time and Location
Date:Wednesday, 26 April 2017
Duration:-- Not specified --
Building:E1 5
Moore's Law may be slowing, but, perhaps as a result, other measures of processor complexity are only accelerating. In recent years,
Intel's architects have turned to an alphabet soup of instruction set extensions such as MPX, SGX, MPK, and CET as a way to sell CPUs
through new security features. SGX in particular promises powerful security: user-mode "enclaves" protected against both physical attacks
and privileged software adversaries. To achieve this, SGX's designers implemented an isolation mechanism approaching the complexity
of an OS microkernel in the ISA, using an inscrutable mix of silicon and microcode. However, while CPU-based security mechanisms are
harder to attack, they are also harder to deploy and update, and already a number of significant flaws have been identified. Worse, the
availability of new SGX features is dependent on the slowing deployment of new CPUs.

In this talk, I'll describe an alternative approach to providing SGX-like enclaves: decoupling the underlying hardware mechanisms such
as memory encryption, address-space isolation and attestation from a privileged software monitor which implements enclaves. The monitor's
trustworthiness is guaranteed by a machine-checked proof of both functional correctness and high-level security properties. The ultimate goal
is to achieve security that is equivalent or better than SGX while decoupling enclave features from the underlying hardware.
Name(s):Roslyn Stricker
EMail:--email address not disclosed on the web
Video Broadcast
Video Broadcast:YesTo Location:Kaiserslautern
To Building:G26To Room:112
Meeting ID:
Tags, Category, Keywords and additional notes
Attachments, File(s):

Roslyn Stricker/MPI-SWS, 04/10/2017 01:41 PM
Last modified:
Uwe Brahm/MPII/DE, 04/26/2017 07:01 AM
  • Roslyn Stricker, 04/10/2017 01:48 PM -- Created document.