Verifying Memory Confidentiality and Integrity of Intel TDX Trusted Execution Environments

Encryption is widely used to protect the confidentiality of data when it is in transit or at rest. However, encryption itself is not enough to guarantee the confidentiality of data-in-use. A Trusted Execution Environment (TEE) provides assurance of three key properties: data confidentiality, data integrity, and code integrity for data-in-use. This is done by enabling isolation and secure storage within a system. It is a major challenge to verify the security requirements in a TEE since isolation and secure storage require complex interaction between different components such as the operating system, hypervisor, firmware, and hardware. In this paper, we perform a comprehensive security analysis of the Intel Trust Domain Extensions (TDX) for memory confidentiality and integrity. Specifically, we analyze the Intel TDX architecture to derive invariants. We generate security assertions (properties) for the invariants based on Finite State Machine (FSM) analysis. We utilize model checking to verify security properties. We also perform static analysis of TDX code to check for various vulnerabilities, including buffer overflow, pointer safety, and arithmetic issues. Extensive experimental evaluation demonstrates that our proposed framework is suitable for verifying Intel TDX architecture. We are also able to identify inconsistency in the TDX specification.