Formal Verification of Key Components of Intel TDX Firmware

Abstract

As computing evolves and the use of cloud environments increases, there is growing concern over security and data confidentiality. Virtual machine-based trusted execution environments (VM-based TEEs) have emerged as a promising solution due to their flexibility and scalability. This thesis presents a formal verification framework for reasoning about the correctness of the Intel TDX firmware—a central component of a prominent VM-based TEE. Using CBMC, a suite of abstraction strategies, and modular verification reasoning, the framework enables tractable analysis of this complex, real-world system. The methodology is specifically applied to the TD creation sequence, demonstrating that the verification process successfully validates correct flows and reliably detects errors when deviations occur. Beyond TDX, this work contributes to the broader goal of developing a scalable and rigorous methodology for evaluating secure processor architectures and ensuring their reliability in real-world deployments.