A Formal Foundation for Secure Remote Execution of Enclaves

  • Authors:
    Pramod Subramanyan (UC/Berkeley), Rohit Sinha (UC/Berkeley), Ilia Lebedev (MIT), Srini Devadas (MIT), Sanjit Seshia (UC/Berkeley)
    Publication ID:
    P091124
    Publication Type:
    Paper
    Received Date:
    16-Jun-2017
    Last Edit Date:
    23-Jan-2018
    Research:
    2637.001 (Carnegie Mellon University)
    2638.001 (University of California/Berkeley)

Abstract

This paper introduces the notion of a trusted abstract platform (TAP) that formally models a trusted platform supporting idealized enclave programs executing in the presence of a parameterized adversary. It presents machine-checked proofs showing that the TAP satisfies the three key security properties needed for secure remote execution: integrity, confidentiality and secure measurement. It presents machine-checked proofs that Intel SGX and MIT Sanctum are refinements of the TAP under certain parameterizations of the adversary, demonstrating that these systems implement secure enclaves for the stated adversary models.

4819 Emperor Blvd, Suite 300 Durham, NC 27703 Voice: (919) 941-9400 Fax: (919) 941-9450

Important Information for the SRC website. This site uses cookies to store information on your computer. By continuing to use our site, you consent to our cookies. If you are not happy with the use of these cookies, please review our Cookie Policy to learn how they can be disabled. By disabling cookies, some features of the site will not work.