Identity Crisis in Confidential Computing: Formal Analysis of Attested TLS
ABSTRACT Remote attestation is increasingly being composed with different protocols to provide endpoint security. Transport Layer Security (TLS) is the most widely used among those protocols, and the composition of TLS with remote attestation is known as attested TLS protocol. Such protocols are used in security-critical applications, e.g., they serve as the backbone of an emerging computing paradigm, Confidential Computing (CC). In this talk, we first explore the identity crisis that results from ambiguous notions of identity for attested TLS protocols in CC. We present a formal approach with a set of modular security goals and a generic template for the comparison of the security strengths of attested TLS protocols. Using the approach, we discover diversion attacks in two state-of-the-art protocols, namely Intel's RA-TLS (pre-handshake attestation) and draft standard draft-fossati-tls-attestation (intra-handshake attestation). The Confidential Computing Consortium (CCC) attestation Special Interest Group (SIG), Internet Engineering Task Force (IETF), and Internet Research Task Force (IRTF) have acknowledged the diversion attacks. The formal artifacts are available at https://github.com/CCC-Attestation/formal-spec-id-crisis under Apache-2.0 License for further research and development. We then present an overview of follow-up research with Viacheslav Dubeyko and Jean-Marie Jacquet, where we discovered relay attacks in various intra-handshake attestation proposals for standardization as well as state-of-the-art implementations in production. In particular, these implementations include Meta’s AI for which an extensive security review by Trail of Bits could not discover these attacks. These relay attacks have been acknowledged by the CCC Attestation SIG, IETF, IRTF, and the vendors. A CVE (CVE-2026-33697) with high severity (7.5/10) has been issued. Our study reveals that it may not be possible to achieve strong application-traffic (level 3) binding using intra-handshake attestation alone. We finally present our post-handshake proposal (draft-fossati-seat-expat) for the mitigation of relay attacks, which is undergoing thorough formal analysis. |
BIO Muhammad Usama Sardar has been working at TU Dresden since October 2017. Since March 2025, he also serves as the co-chair of the Trusted Research Environment (TRE) Open Suite in The Global Alliance for Genomics and Health (GA4GH). He led the completed TEE formal specification project and currently leads the Key Broker Service (KBS) formal verification project in Confidential Computing Consortium (CCC) Attestation Special Interest Group (SIG). He also contributes to various research networks, such as EuroProofNet (WG3), Méthodes formelles pour la sécurité, Internet Research Task Force (IRTF) Usable Formal Methods Research Group (UFMRG), as well as engineering networks, such as Internet Engineering Task Force (IETF) Remote ATtestation procedureS (RATS), Transport Layer Security (TLS), and Workload Identity in Multi System Environments (WIMSE) working groups. |