Biblio

With a broad spectrum of technologies for the protection of personal data, it is important to be able to reliably compare these technologies to choose the most suitable one for a given problem. Although technologies like Homomorphic Encryption have matured over decades, Confidential Computing is still in its infancy with not only informal but also incomplete and even conflicting definitions by the Confidential Computing Consortium (CCC). In this work, we present key issues in definitions and comparison among existing technologies by CCC. We also provide recommendations to achieve clarity and precision in the definitions as well as fair and scientific comparison among existing technologies. We emphasize on the need of formal definitions of the terms and pose it as an open challenge to the community.

One of the essential features of confidential computing is the ability to attest to an application remotely. Remote attestation ensures that the right code is running in the correct environment. We need to ensure that all components that an adversary might use to impact the integrity, confidentiality, and consistency of an application are attested. Which components need to be attested is defined with the help of a policy. Verification of the policy is performed with the help of an attestation engine. Since remote attestation bootstraps the trust in remote applications, any vulnerability in the attestation mechanism can therefore impact the security of an application. Moreover, mistakes in the attestation policy can result in data, code, and secrets being vulnerable. Our work focuses on 1) how we can verify the attestation mechanisms and 2) how to verify the policy to ensure that data, code, and secrets are always protected.

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 at-testation 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.

In August 2020, Intel asked the research community for feedback on the newly offered architecture extensions, called Intel Trust Domain Extensions (TDX), which give more control to Trust Domains (TDs) over processor resources. One of the key features of these extensions is the remote attestation mechanism, which provides a unified report verification mechanism for TDX and its predecessor Software Guard Extensions (SGX). Based on our experience and intuition, we respond to the request for feedback by formally specifying the attestation mechanism in the TDX using ProVerif's specification language. Although the TDX technology seems very promising, the process of formal specification reveals a number of subtle discrepancies in Intel's specifications that could potentially lead to design and implementation flaws. After resolving these discrepancies, we also present fully automated proofs that our specification of TD attestation preserves the confidentiality of the secret and authentication of the report by considering the state-of-the-art Dolev-Yao adversary in the symbolic model using ProVerif. We have submitted the draft to Intel, and Intel is in the process of making the changes.