A System Framework to Symbolically Explore Intel TDX Module Execution

We present TDXplorer, the first dynamic symbolic analysis system for Intel's TDX Module, the software trusted computing base of TDX. Without using TDX hardware, an analyzer function on top of TDXplorer can not only apply dynamic analysis to control and instrument the TDX Module's execution, but also carry out symbolic execution for path exploration as well as security and functionality reasoning. The two types of analysis are seamlessly integrated in a way that symbolic execution is conducted directly upon the TDX Module's binary code and runtime states, which are shaped by using dynamic analysis techniques. We implement TDXplorer on Linux and measure its performance and correctness against executions on a TDX platform. Our case studies on symbolic modeling of secure EPT creation and KeyHole region management demonstrate that TDXplorer is a versatile and capable tool supporting various analysis tasks.