A Formal Foundation for Secure Remote Execution of Enclaves

Pramod Subramanyan, Rohit Sinha, Ilia A. Lebedev, Srinivas Devadas, and Sanjit A. Seshia. A Formal Foundation for Secure Remote Execution of Enclaves. In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security (CCS), pp. 2435–2450, 2017.
Best Paper Award.

Download

[pdf] 

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), a formalization of idealized enclave platforms along with a parameterized adversary. We also formalize the notion of secure remote execution and present machine-checked proofs showing that the TAP satisfies the three key security properties that entail 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.

BibTeX

@inproceedings{subramanyan-ccs17,
  author    = {Pramod Subramanyan and
               Rohit Sinha and
               Ilia A. Lebedev and
               Srinivas Devadas and
               Sanjit A. Seshia},
  title     = {A Formal Foundation for Secure Remote Execution of Enclaves},
  booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and
               Communications Security (CCS)},
  pages     = {2435--2450},
  year      = {2017},
  wwwnote = {<b>Best Paper Award</b>.},
  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), a formalization of idealized enclave platforms along with a parameterized adversary. We also formalize the notion of secure remote execution and present machine-checked proofs showing that the TAP satisfies the three key security properties that entail 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.},
}