Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
10-2025
Abstract
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.
Keywords
Intel TDX Emulation, Intel TDX Module, Dynamic Program Analy-sis, Symbolic Execution
Discipline
Information Security
Areas of Excellence
Digital transformation
Publication
CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, Taipei, Taiwan October 13-17
First Page
3885
Last Page
3899
Identifier
10.1145/3719027.3765212
Publisher
ACM
City or Country
New York
Citation
PITIGALAARACHCHILLAGE, Pansilu and DING, Xuhua.
A system framework to symbolically explore Intel TDX module execution. (2025). CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security, Taipei, Taiwan October 13-17. 3885-3899.
Available at: https://ink.library.smu.edu.sg/sis_research/10971
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1145/3719027.3765212