A Formal Foundation for Secure Remote Execution of Enclaves
Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas Devadas, Sanjit Seshia

Citation
Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas Devadas, Sanjit Seshia. "A Formal Foundation for Secure Remote Execution of Enclaves". Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, ACM, 2435-2450, October, 2017.

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.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas
  Devadas, Sanjit Seshia. <a
  href="http://www.terraswarm.org/pubs/1021.html"
  >A Formal Foundation for Secure Remote Execution of
  Enclaves</a>,  Proceedings of the 2017 ACM SIGSAC
  Conference on Computer and Communications Security, ACM,
  2435-2450, October, 2017.

• Plain text

  Pramod Subramanyan, Rohit Sinha, Ilia Lebedev, Srinivas
  Devadas, Sanjit Seshia. "A Formal Foundation for Secure
  Remote Execution of Enclaves".  Proceedings of the 2017
  ACM SIGSAC Conference on Computer and Communications
  Security, ACM, 2435-2450, October, 2017.

• BibTeX

  @inproceedings{SubramanyanSinhaLebedevDevadasSeshia17_FormalFoundationForSecureRemoteExecutionOfEnclaves,
      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},
      booktitle = { Proceedings of the 2017 ACM SIGSAC Conference on
                Computer and Communications Security},
      organization = {ACM},
      pages = {2435-2450},
      month = {October},
      year = {2017},
      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://terraswarm.org/pubs/1021.html}
  }
  

Posted by Pramod Subramanyan on 14 Nov 2017.
Groups: tools