A Formal Foundation for Secure Remote Execution of Enclaves
| Title | A Formal Foundation for Secure Remote Execution of Enclaves |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Subramanyan, Pramod, Sinha, Rohit, Lebedev, Ilia, Devadas, Srinivas, Seshia, Sanjit A. |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | composability, confidentiality, Enclave Programs, formal verification, integrity, Metrics, Microelectronic Security, Microelectronics Security, pubcrawl, remote attestation, resilience, Resiliency, secure computation |
| 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. |
| URL | http://doi.acm.org/10.1145/3133956.3134098 |
| DOI | 10.1145/3133956.3134098 |
| Citation Key | subramanyan_formal_2017 |