Formal Foundations for Intel SGX Data Center Attestation Primitives

Abstract

Intel has recently offered third-party attestation services, called Data Center Attestation Primitives (DCAP), for a data center to create its own attestation infrastructure. These services address the availability concerns and improve the performance as compared to the remote attestation based on Enhanced Privacy ID (EPID). Practical developments, such as Hyperledger Avalon, have already planned to support DCAP in their roadmap. However, the lack of formal proof for DCAP leads to security concerns. To fill this gap, we propose an automated, rigorous, and sound formal approach to specify and verify the remote attestation based on Intel SGX DCAP under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. In the proposed approach, the data center configuration and operational policies are specified to generate the symbolic model, and security goals are specified as security properties to produce verification results. The evaluation of non-Quoting Verification Enclave-based DCAP indicates that the confidentiality of secrets and integrity of data is preserved against a Dolev-Yao adversary in this technology. We also present a few of the many inconsistencies found in the existing literature on Intel SGX DCAP during formal specification.

VIEW FULL PAPER

BIOS

Muhammad Usama Sardar. Since 2017, he is recipient of the prestigious DAAD research grant for his PhD at TU Dresden. His current research focus is on the formal specification and verification of the remote attestation process in Trusted Execution Environments, with a special focus on Intel SGX. He is also a tutor for the master's courses: Systems Engineering 1, Principles of Dependable Systems and Software Fault Tolerance. He is also serving as a volunteer at CAVlinks. He has received South Asia Triple Helix Association (SATHA) Innovation Award in 2018, best researcher of the year award in System Analysis and Verification lab in Pakistan in 2017, and best speaker awards at Workshop on Applications in ASIC Design (December 2016) and Workshop on Recent Trends in Theorem Proving (April 2016).

Rasha Faqeh. She received her Master degree in computer science from the Technische Universitat Dresden in 2013. Then, she joined the systems engineering group as a tutor and a PhD student under the supervision of Prof. Christof Fetzer at TU Dresden. Her research focuses on the modeling and the analysis of dependable systems, specially the security analysis of systems designed for the distributed and the trusted computing domain.

Christof Fetzer. Prof. Fetzer's research focuses on Trusted Execution and Dependable Computing. He is a founder of CloudHeat GmbH, SIListra Systems GmbH, and Scontain UG. He has been a Professor at TU Dresden, Germany since 2004 and he received his PhD from the University of California, San Diego.