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