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 work, we 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 comprehensive security goals and a generic template for the comparison of the security strengths of attested TLS protocols. Using the approach, we discover vulnerabilities in two state-of-the-art protocols. The Confidential Computing Consortium (CCC) attestation Special Interest Group (SIG) and TLS working group have acknowledged the vulnerabilities. To mitigate the vulnerabilities, we present a formally verified solution for vulnerabilities and propose several potential solutions, which are under discussion for standardization at the Internet Engineering Task Force (IETF).

Abstract This research critically reviews the definition of confidential computing (CC) and the security comparison of CC with other related technologies by the Confidential Computing Consortium (CCC). We demonstrate that the definitions by CCC are ambiguous, incomplete and even conflicting. We also demonstrate that the security comparison of CC with other technologies is neither scientific nor fair. We highlight the issues in the definitions and comparisons and provide initial recommendations for fixing the issues. These recommendations are the first step towards more precise definitions and reliable comparisons in the future.

Vulnerabilities in privileged software layers have been exploited with severe consequences. Recently, Trusted Execution Environments (TEEs) based technologies have emerged as a promising approach since they claim strong confidentiality and integrity guarantees regardless of the trustworthiness of the underlying system software. In this paper, we consider one of the most prominent TEE technologies, referred to as Intel Software Guard Extensions (SGX). Despite many formal approaches, there is still a lack of formal proof of some critical processes of Intel SGX, such as remote attestation. To fill this gap, we propose a fully automated, rigorous, and sound formal approach to specify and verify the Enhanced Privacy ID (EPID)-based remote attestation in Intel SGX under the assumption that there are no side-channel attacks and no vulnerabilities inside the enclave. The evaluation indicates that the confidentiality of attestation keys 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 attestation during formal specification.