Cryptology ePrint Archive: Report 2017/565

A Formal Foundation for Secure Remote Execution of Enclaves

Pramod Subramanyan and Rohit Sinha and Ilia Lebedev and Srinivas Devadas and Sanjit Seshia

Abstract: Recent proposals for trusted hardware platforms, such as Intel SGX and the MIT Sanctum processor, offer compelling security features but lack formal guarantees. We introduce a verification methodology based on a trusted abstract platform (TAP) that formally models idealized enclaves and a parameterized adversary. We present machine-checked proofs showing that the TAP satisfies the three key security properties needed for secure remote execution: integrity, confidentiality and secure measurement. We then present machine-checked proofs showing that SGX and Sanctum are refinements of the TAP under certain parameterizations of the adversary, demonstrating that these systems implement secure enclaves for the stated adversary models.

Category / Keywords: applications /

Original Publication (in the same form): ACM CCS 2017
DOI:
10.1145/3133956.3134098

Date: received 9 Jun 2017, last revised 29 Aug 2017

Contact author: pramod at berkeley edu

Available format(s): PDF | BibTeX Citation

Note: ACM CCS'17 camera-ready version.

Version: 20170829:234313 (All versions of this report)

Short URL: ia.cr/2017/565

Discussion forum: Show discussion | Start new discussion


[ Cryptology ePrint archive ]