Paper 2017/565

A Formal Foundation for Secure Remote Execution of Enclaves

Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, 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.

Note: ACM CCS'17 camera-ready version.

Metadata
Available format(s)
PDF
Category
Applications
Publication info
Published elsewhere. ACM CCS 2017
DOI
10.1145/3133956.3134098
Contact author(s)
pramod @ berkeley edu
History
2017-08-29: revised
2017-06-14: received
See all versions
Short URL
https://ia.cr/2017/565
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/565,
      author = {Pramod Subramanyan and Rohit Sinha and Ilia Lebedev and Srinivas Devadas and Sanjit Seshia},
      title = {A Formal Foundation for Secure Remote Execution of Enclaves},
      howpublished = {Cryptology ePrint Archive, Paper 2017/565},
      year = {2017},
      doi = {10.1145/3133956.3134098},
      note = {\url{https://eprint.iacr.org/2017/565}},
      url = {https://eprint.iacr.org/2017/565}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.