{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:17:34Z","timestamp":1766441854809,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,11,19]]},"DOI":"10.1145\/3719027.3765212","type":"proceedings-article","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T23:32:38Z","timestamp":1763854358000},"page":"3885-3899","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A System Framework to Symbolically Explore Intel TDX Module Execution"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0008-9991-3390","authenticated-orcid":false,"given":"Pansilu","family":"Pitigalaarachchi","sequence":"first","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3974-590X","authenticated-orcid":false,"given":"Xuhua","family":"Ding","sequence":"additional","affiliation":[{"name":"Singapore Management University, Singapore, Singapore"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,11,22]]},"reference":[{"key":"e_1_3_2_1_1_1","unstructured":"AMD. 2024. SEV Secure Nested Paging Firmware ABI Specification. https:\/\/www.amd.com\/content\/dam\/amd\/en\/documents\/epyc-technical-docs\/specifications\/56860.pdf. Accessed: 2024-05-22."},{"key":"e_1_3_2_1_2_1","unstructured":"Arm. 2021. Arm CCA Security Model 1.0. https:\/\/developer.arm.com\/documentation\/DEN0096\/A_a."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2560217.2560219"},{"key":"e_1_3_2_1_4_1","volume-title":"USENIX Annual Technical Conference, FREENIX Track. 41-46","author":"Bellard Fabrice","year":"2005","unstructured":"Fabrice Bellard. 2005. QEMU, a fast and portable dynamic translator. In USENIX Annual Technical Conference, FREENIX Track. 41-46."},{"key":"e_1_3_2_1_5_1","volume-title":"Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). 209-224","author":"Cadar Cristian","year":"2008","unstructured":"Cristian Cadar, Daniel Dunbar, and Dawson Engler. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the USENIX Symposium on Operating Systems Design and Implementation (OSDI). 209-224."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2012.31"},{"key":"e_1_3_2_1_7_1","volume-title":"Proceedings of the 29th USENIX Security Symposium. 1093-1110","author":"Chen Weiteng","year":"2020","unstructured":"Weiteng Chen, Xiaochen Zou, Guoren Li, and Zhiyun Qian. 2020. KOOBE: Towards Facilitating Exploit Generation of Kernel Out-Of-Bounds Write Vulnerabilities. In Proceedings of the 29th USENIX Security Symposium. 1093-1110."},{"key":"e_1_3_2_1_8_1","volume-title":"Intel tdx demystified: A top-down approach. Comput. Surveys","author":"Cheng Pau-Chen","year":"2023","unstructured":"Pau-Chen Cheng, Wojciech Ozga, Enriquillo Valdez, Salman Ahmed, Zhongshu Gu, Hani Jamjoom, Hubertus Franke, and James Bottomley. 2023. Intel tdx demystified: A top-down approach. Comput. Surveys (2023)."},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2110356.2110358"},{"key":"e_1_3_2_1_10_1","volume-title":"Intel TDX Documentation. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/documentation.html Retrieved April 25th","author":"Intel Corporation","year":"2024","unstructured":"Intel Corporation. 2023. Intel TDX Documentation. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/documentation.html Retrieved April 25th, 2024 from"},{"key":"e_1_3_2_1_11_1","unstructured":"Intel Corporation. 2025a. TDX Module. https:\/\/github.com\/intel\/tdx-module. Accessed: 2025-04-13."},{"key":"e_1_3_2_1_12_1","unstructured":"Intel Corporation. 2025b. TDX Module Build Instructions (tdx_1.5 branch). https:\/\/github.com\/intel\/tdx-module\/blob\/tdx_1.5\/BUILD.md. Accessed: 2025-04-13."},{"key":"e_1_3_2_1_13_1","first-page":"463","volume-title":"22nd USENIX Security Symposium (USENIX Security 13)","author":"Davidson Drew","year":"2013","unstructured":"Drew Davidson, Benjamin Moench, Thomas Ristenpart, and Somesh Jha. 2013. {FIE} on firmware: Finding vulnerabilities in embedded systems using symbolic execution. In 22nd USENIX Security Symposium (USENIX Security 13). 463-478."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3433210.3453093"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3586040"},{"volume-title":"Frama-c Software Analyzers. https:\/\/frama-c.com\/ Retrieved November 8th","year":"2023","key":"e_1_3_2_1_16_1","unstructured":"Frama-c. 2023. Frama-c Software Analyzers. https:\/\/frama-c.com\/ Retrieved November 8th, 2023 from"},{"key":"e_1_3_2_1_17_1","unstructured":"Google LLC and Intel Corporation. 2023. Intel TDX Security Review Report. https:\/\/services.google.com\/fh\/files\/misc\/intel_tdx_-_full_report_041423.pdf. Accessed: 2025-04-14."},{"key":"e_1_3_2_1_18_1","unstructured":"Intel Corporation. 2024a. Intel TDX Module: KVM Upstream Branch. https:\/\/github.com\/intel\/tdx\/tree\/kvm-upstream. Accessed: 2025-04-14."},{"key":"e_1_3_2_1_19_1","unstructured":"Intel Corporation. 2024b. Intel\u00ae Trust Domain CPU Architectural Extensions. Available at: https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/documentation.html."},{"key":"e_1_3_2_1_20_1","unstructured":"Intel Corporation. 2024c. Intel\u00ae Trust Domain Extensions Module Architecture Application Binary Interface Specification. Available at: https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/documentation.html."},{"key":"e_1_3_2_1_21_1","unstructured":"Intel Corporation. 2024d. Intel\u00ae Trust Domain Extensions (TDX) Base Specification. Available at: https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/documentation.html."},{"key":"e_1_3_2_1_22_1","volume-title":"Proceedings of the IEEE Symposium on Security and Privacy (S&P). 588-603","author":"Jiang Zheyue","year":"2023","unstructured":"Zheyue Jiang, Yuan Zhang, Jun Xu, Xinqian Sun, Zhuang Liu, and Min Yang. 2023. AEM: Facilitating Cross-Version Exploitability Assessment of Linux Kernel Vulnerabilities. In Proceedings of the IEEE Symposium on Security and Privacy (S&P). 588-603."},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2020.24018"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"e_1_3_2_1_25_1","unstructured":"Canonical Ltd. 2024. Intel confidential computing - TDX. https:\/\/github.com\/canonical\/tdx Accessed: 2025-04-09."},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1064978.1065034"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395351.3399360"},{"key":"e_1_3_2_1_28_1","unstructured":"Microsoft. 2024. Cornelius. https:\/\/github.com\/microsoft\/Cornelius. Accessed: 2025-04-14."},{"key":"e_1_3_2_1_29_1","unstructured":"Microsoft and Intel Corporation. 2024. Microsoft and Intel joint security review of Intel TDX 1.5. https:\/\/community.intel.com\/t5\/Blogs\/Products-and-Solutions\/Security\/Intel-and-Microsoft-joint-security-review-of-Intel-TDX-1-5\/post\/1615189. Accessed: 2025-04-14."},{"volume-title":"Issue 8: Canary validation in tdh_sys_lp_init(). https:\/\/github.com\/intel\/tdx-module\/issues\/8 Retrieved August 21st","year":"2025","key":"e_1_3_2_1_30_1","unstructured":"pansilup. 2024. Issue 8: Canary validation in tdh_sys_lp_init(). https:\/\/github.com\/intel\/tdx-module\/issues\/8 Retrieved August 21st, 2025 from"},{"volume-title":"Issue 15: Input validation in SEAM\/TD Calls for reading metadata. https:\/\/github.com\/intel\/tdx-module\/issues\/15 Retrieved August 21st","year":"2025","key":"e_1_3_2_1_31_1","unstructured":"pansilup. 2025a. Issue 15: Input validation in SEAM\/TD Calls for reading metadata. https:\/\/github.com\/intel\/tdx-module\/issues\/15 Retrieved August 21st, 2025 from"},{"volume-title":"Issue 20: Incorrect output operand values on TD Call failure. https:\/\/github.com\/intel\/tdx-module\/issues\/20 Retrieved August 21st","year":"2025","key":"e_1_3_2_1_32_1","unstructured":"pansilup. 2025b. Issue 20: Incorrect output operand values on TD Call failure. https:\/\/github.com\/intel\/tdx-module\/issues\/20 Retrieved August 21st, 2025 from"},{"volume-title":"Issue 21: Incorrect output operand values on SEAM Call failure. https:\/\/github.com\/intel\/tdx-module\/issues\/21 Retrieved August 21st","year":"2025","key":"e_1_3_2_1_33_1","unstructured":"pansilup. 2025c. Issue 21: Incorrect output operand values on SEAM Call failure. https:\/\/github.com\/intel\/tdx-module\/issues\/21 Retrieved August 21st, 2025 from"},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TDSC.2025.3528737"},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576915.3623198"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2021.24118"},{"key":"e_1_3_2_1_37_1","volume-title":"https:\/\/github.com\/dyninst\/dyninst\/tree\/v12.0.0 Retrieved September 8th","author":"Project Dyninst","year":"2023","unstructured":"Dyninst Project. 2021. Dyninst. https:\/\/github.com\/dyninst\/dyninst\/tree\/v12.0.0 Retrieved September 8th, 2023 from"},{"key":"e_1_3_2_1_38_1","volume-title":"TDXplorer: extended paper. https:\/\/github.com\/KRoverSystems\/TDXplorer\/blob\/master\/TDXplorerLongPaper.pdf Retrieved September 6th","author":"Xplorer","year":"2024","unstructured":"TDXplorer project. 2025. TDXplorer: extended paper. https:\/\/github.com\/KRoverSystems\/TDXplorer\/blob\/master\/TDXplorerLongPaper.pdf Retrieved September 6th, 2024 from"},{"key":"e_1_3_2_1_39_1","volume-title":"Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI). 279-292","author":"Renzelmann Matthew J","year":"2012","unstructured":"Matthew J Renzelmann, Asim Kadav, and Michael M Swift. 2012. SymDrive: Testing drivers without devices. In Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation (OSDI). 279-292."},{"key":"e_1_3_2_1_40_1","volume-title":"https:\/\/github.com\/Z3Prover\/z3\/tree\/z3-4.8.15 Retrieved September 8th","author":"Research Microsoft","year":"2024","unstructured":"Microsoft Research. 2021. Z3. https:\/\/github.com\/Z3Prover\/z3\/tree\/z3-4.8.15 Retrieved September 8th, 2024 from"},{"key":"e_1_3_2_1_41_1","first-page":"3459","volume-title":"33rd USENIX Security Symposium (USENIX Security 24)","author":"Schl\u00fcter Benedict","year":"2024","unstructured":"Benedict Schl\u00fcter, Supraja Sridhara, Mark Kuhne, Andrin Bertschi, and Shweta Shinde. 2024. {HECKLER}: Breaking Confidential {VMs} with Malicious Interrupts. In 33rd USENIX Security Symposium (USENIX Security 24). 3459-3476."},{"key":"e_1_3_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF.2012.25"},{"key":"e_1_3_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2016.17"},{"key":"e_1_3_2_1_44_1","unstructured":"Intel\u00ae Memory Encryption Technologies. 2024. https:\/\/cdrdv2-public.intel.com\/679154\/multi-key-total-memory-encryption-spec-1.4.pdf."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2024.3395412"},{"key":"e_1_3_2_1_46_1","volume-title":"Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS). 1914-1927","author":"Wang Yan","year":"2018","unstructured":"Yan Wang, Chao Zhang, Xiaobo Xiang, Zixuan Zhao, Wenjie Li, Xiaorui Gong, Bingchang Liu, Kaixiang Chen, and Wei Zou. 2018. Revery: From Proof-of-Concept to Exploitable (One Step towards Automatic Exploit Generation). In Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS). 1914-1927."},{"volume-title":"weggli. https:\/\/github.com\/weggli-rs\/weggli Retrieved November 8th","year":"2023","key":"e_1_3_2_1_47_1","unstructured":"weggli rs. 2023. weggli. https:\/\/github.com\/weggli-rs\/weggli Retrieved November 8th, 2023 from"},{"key":"e_1_3_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3658644.3690230"},{"key":"e_1_3_2_1_49_1","volume-title":"Allowing an Intel TDX Module to Run Without SEAM. https:\/\/www.youtube.com\/watch?v=wNq6shZCYm0. KVM Forum","author":"Yamahata Isaku","year":"2022","unstructured":"Isaku Yamahata. 2022. Allowing an Intel TDX Module to Run Without SEAM. https:\/\/www.youtube.com\/watch?v=wNq6shZCYm0. KVM Forum 2022, Intel Corporation."},{"key":"e_1_3_2_1_50_1","volume-title":"Proceedings of the 27th USENIX Security Symposium. 745-761","author":"Yun Insu","year":"2020","unstructured":"Insu Yun, Sangho Lee, Meng Xu, Yeongjin Jang, and Taesoo Kim. 2020. QSYM: A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing. In Proceedings of the 27th USENIX Security Symposium. 745-761."},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.14722\/ndss.2014.23229"}],"event":{"name":"CCS '25: ACM SIGSAC Conference on Computer and Communications Security","sponsor":["SIGSAC ACM Special Interest Group on Security, Audit, and Control"],"location":"Taipei Taiwan","acronym":"CCS '25"},"container-title":["Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3719027.3765212","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,22]],"date-time":"2025-12-22T22:15:14Z","timestamp":1766441714000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3719027.3765212"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,19]]},"references-count":51,"alternative-id":["10.1145\/3719027.3765212","10.1145\/3719027"],"URL":"https:\/\/doi.org\/10.1145\/3719027.3765212","relation":{},"subject":[],"published":{"date-parts":[[2025,11,19]]},"assertion":[{"value":"2025-11-22","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}