Confidential Computing Attestation Mechanisms: Unveiling Vulnerabilities in Arm CCA and Intel TDX

Attestation is a crucial aspect of confidential computing (CC), a technology that safeguards data during processing. It is particularly relevant in the context of privacy and data protection laws such as the GDPR. There are four primary Privacy Enhancing Technologies (PETs) that offer potential solutions for protecting data in active use: Secure Multi-party computation (MPC), Homomorphic Encryption (HE), Zero-Knowledge Proofs (ZKPs), and Confidential Computing (CC) using hardware-based Trusted Execution Environments (TEEs). Each technology has its pros and cons, with CC offering high performance but requiring a larger Trusted Computing Base (TCB). The article also discusses the importance of formal specification and verification of attestation mechanisms, and presents a study on attestation mechanisms in Arm CCA and Intel TDX.

What is the Importance of Attestation in Confidential Computing?

Attestation is a critical mechanism in confidential computing (CC), a technology that protects data during processing. This is particularly important in the context of privacy and data protection laws such as the General Data Protection Regulation (GDPR). While data protection at rest and in transit is well understood, protecting data in use is a relatively new concept. There are four primary technologies, known as Privacy Enhancing Technologies (PETs), that offer potential solutions for protecting data in active use. These include Secure Multi-party computation (MPC), Homomorphic Encryption (HE), Zero-Knowledge Proofs (ZKPs), and Confidential Computing (CC) using hardware-based Trusted Execution Environments (TEEs).

Each of these technologies has its advantages and disadvantages. For instance, while MPC, HE, and ZKPs offer a small Trusted Computing Base (TCB) consisting of software only, they suffer from high computation and communication overhead. On the other hand, CC enables high performance at the cost of a relatively larger TCB consisting of hardware, firmware, and software components. Because of this dependence on hardware, firmware, and software components in CC, it is necessary to attest that the platform on which user-provided workload executes is real, authentic, and up-to-date, and that the workload executing on the data is the expected one, unmodified. This is referred to as architecturally-defined attestation.

How is Attestation Implemented in Different Technologies?

While MPC, HE, and ZKPs have existed for decades and are based on well-defined mathematical concepts, CC is a relatively emerging technology. In addition to the existing TEEs such as Intel Software Guard Extensions (SGX) and AMD Secure Encrypted Virtualization-Secure Nested Paging (SEV-SNP), new TEEs such as Arm Confidential Compute Architecture (CCA), Intel Trust Domain Extensions (TDX), RISCV Confidential Virtual Machine Extensions (CoVE), and IBM Protected Execution Facility (PEF) are being introduced. Each of these TEEs has a distinctive attestation architecture and design.

For example, Intel SGX and TDX and AMD SEV-SNP are deployed products where all details of the platform attestation have been established, referred to as vendor solutions. In contrast, Arm CCA and RISCV APTEE have common architectural specifications that multiple products may share, referred to as architecture-led solutions. These solutions only provide a common design for attestation, allowing detailed differentiation between the actual products from their partners. Moreover, some technologies such as Intel SGX and TDX have a layered structure for attestation, while attestation in Arm CCA comprises multiple Attesters.

Why is Formal Specification and Verification of Attestation Mechanisms Important?

Due to the distinctive attestation architecture and security-critical nature of the architecturally-defined attestation mechanisms in TEEs, it is crucial to understand and perform a systematic security analysis of such mechanisms for emerging TEEs. Formal methods provide a systematic and mathematically rigorous approach to understanding, specifying, and verifying system behavior. Specifically, symbolic security analysis tools are widely used to precisely define and rigorously analyze the behavior and properties of a protocol such as TLS 13.

Compared to such protocols, a major challenge in the formalization of architecturally-defined attestation is that all vendors present specifications of architecturally-defined attestation in natural language. Such vague specifications can lead to a violation of integrity, freshness, and secrecy properties for Intel’s claimed trusted computing base (TCB), which could not be captured by considering the attestation protocol alone in the related work.

What are the Findings of the Study on Attestation Mechanisms in Arm CCA and Intel TDX?

The study presents a holistic verification approach enabling comprehensive and rigorous security analysis of architecturally-defined attestation mechanisms in CC. Specifically, the researchers analyze two prominent next-generation hardware-based Trusted Execution Environments (TEEs), namely Arm Confidential Compute Architecture (CCA) and Intel Trust Domain Extensions (TDX). For both of these solutions, they provide a comprehensive specification of all phases of the attestation mechanism, namely provisioning, initialization, and attestation protocol.

The researchers demonstrate that including the initialization phase in the formal model leads to a violation of integrity, freshness, and secrecy properties for Intel’s claimed trusted computing base (TCB), which could not be captured by considering the attestation protocol alone in the related work. The researchers have open-sourced their artifacts, and other researchers, including a team from Intel, are adopting these artifacts for further analysis.

What is the Impact of this Research?

This research has significant implications for the field of confidential computing. By providing a comprehensive specification and verification of the attestation mechanisms in Arm CCA and Intel TDX, the researchers have highlighted potential vulnerabilities in these systems. This could lead to improvements in the design and implementation of these and other similar systems, enhancing the security of confidential computing. By open-sourcing their artifacts, the researchers have also made a valuable contribution to the broader research community, enabling further analysis and development in this area.