MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Securing enclaves with formal verification

Andrew Baumann
Microsoft Research, Redmond
SWS Colloquium

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).
AG 1, AG 2, AG 3, AG 4, AG 5, SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Wednesday, 26 April 2017
16:00
-- Not specified --
E1 5
029
Saarbrücken

Abstract

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.

Contact

Roslyn Stricker
--email hidden

Video Broadcast

Yes
Kaiserslautern
G26
112
passcode not visible
logged in users only

Roslyn Stricker, 04/10/2017 13:48 -- Created document.