@COMMENT This file was generated by bib2html.pl version 0.94
@COMMENT written by Patrick Riley
@COMMENT This file came from Sanjit Seshia's publication pages at http://www.eecs.berkeley.edu/~sseshia
@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 = {Best Paper Award.},
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.},
}