Formal Analysis of Remote Attestation in Trusted Execution Environments

Confidential computing, acknowledged as one of the top 10 Digital Transformation Trends for 2021 in Forbes Magazine, has the potential to be a game-changer in cloud security. The offered high level of security is enabled by the so-called hardware-based trusted execution environments (TEEs). The most important feature of these TEEs is remote attestation which enables a remote user to get security guarantees about the execution of the workload. Despite its importance, very little effort has been made on the formalization of remote attestation. Such formal guarantees are the key enablers of the technology for regulatory industries, such as finance, medical, and government. Towards this goal, we present an automated approach based on symbolic security analysis for the remote attestation in TEEs. The recently announced (but not yet released) technology, called Intel Trust Domain Extensions (TDX), will be presented as a case study. Although the TDX technology seems very promising, yet the process of formal specification reveals a number of subtle discrepancies in Intel’s informal specifications. 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.