@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@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 = {<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.},
}