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:
    Publication Type:
    Received Date:
    Last Edit Date:
    2637.001 (Carnegie Mellon University)
    2638.001 (University of California/Berkeley)


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.