Back to Search
Start Over
A formal foundation for secure remote execution of enclaves
- Source :
- CCS
- Publication Year :
- 2017
- Publisher :
- eScholarship, University of California, 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.
- Subjects :
- Integrity
Computer science
Remote Attestation
020206 networking & telecommunications
020207 software engineering
02 engineering and technology
Adversary
Computer security
computer.software_genre
Mathematical proof
Enclave Programs
Secure two-party computation
0202 electrical engineering, electronic engineering, information engineering
Key (cryptography)
Secure multi-party computation
Confidentiality
Formal verification
computer
Formal Verification
Adversary model
Secure Computation
Subjects
Details
- Database :
- OpenAIRE
- Journal :
- CCS
- Accession number :
- edsair.doi.dedup.....6bc872bc19ecde77a9979c4d3eb9a310