{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:05:36Z","timestamp":1776373536469,"version":"3.51.2"},"publisher-location":"Cham","reference-count":79,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032227485","type":"print"},{"value":"9783032227492","type":"electronic"}],"license":[{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T00:00:00Z","timestamp":1767225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-3-032-22749-2_3","type":"book-chapter","created":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:11:53Z","timestamp":1776258713000},"page":"42-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Case Study in Firmware Verification: Applying Formal Methods to Intel$$^\\circledR $$ TDX Module"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4832-7662","authenticated-orcid":false,"given":"Dirk","family":"Beyer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5139-5178","authenticated-orcid":false,"given":"Po-Chun","family":"Chien","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7069-4069","authenticated-orcid":false,"given":"Bo-Yuan","family":"Huang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8096-5595","authenticated-orcid":false,"given":"Nian-Ze","family":"Lee","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0291-815X","authenticated-orcid":false,"given":"Thomas","family":"Lemberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2026,4,15]]},"reference":[{"key":"3_CR1","unstructured":"Intel Trust Domain Extensions. https:\/\/www.intel.com\/content\/www\/us\/en\/developer\/tools\/trust-domain-extensions\/documentation.html, accessed: 2025\u201307-08."},{"key":"3_CR2","unstructured":"The Coq proof assistant, version 8.16.0 (2022). DOI: 10.5281\/zenodo.7313584."},{"key":"3_CR3","unstructured":"Aktas, E., Cohen, C., Eads, J., Forshaw, J., Wilhelm, F.: Intel Trust Domain Extensions (TDX) security review. Tech. rep., Google Project Zero (2023). https:\/\/services.google.com\/fh\/files\/misc\/intel_tdx__full_report_041423.pdf"},{"key":"3_CR4","doi-asserted-by":"crossref","unstructured":"Alglave, J., Donaldson, A.F., Kroning, D., Tautschnig, M.: Making software verification tools really work. In: Proc. ATVA. pp. 28\u201342. LNCS 6996, Springer (2011). DOI: 10.1007\/978-3-642-24372-1_3.","DOI":"10.1007\/978-3-642-24372-1_3"},{"key":"3_CR5","unstructured":"Ba, J., B\u00f6hme, M., Mirzamomen, Z., Roychoudhury, A.: Stateful greybox fuzzing. In: Proc. USENIX Security. pp. 3255\u20133272. USENIX Association (2022). https:\/\/www.usenix.org\/conference\/usenixsecurity22\/presentation\/ba."},{"key":"3_CR6","doi-asserted-by":"crossref","unstructured":"Baier, D., Beyer, D., Chien, P.C., Jankola, M., Kettl, M., Lee, N.Z., Lemberger, T., Lingsch-Rosenfeld, M., Spiessl, M., Wachowitz, H., Wendler, P.: CPAchecker 2.3 with strategy selection (competition contribution). In: Proc. TACAS (3). pp. 359\u2013364. LNCS 14572, Springer (2024). DOI: 10.1007\/978-3-031-57256-2_21.","DOI":"10.1007\/978-3-031-57256-2_21"},{"issue":"7","key":"3_CR7","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1145\/1965724.1965743","volume":"54","author":"T Ball","year":"2011","unstructured":"Ball, T., Levin, V., Rajamani, S.K.: A decade of software model checking with Slam. Commun. ACM 54(7), 68\u201376 (2011). DOI: 10.1145\/1965724.1965743.","journal-title":"Commun. ACM"},{"key":"3_CR8","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The Slam project: Debugging system software via static analysis. In: Proc. POPL. pp. 1\u20133. ACM (2002). DOI: 10.1145\/503272.503274.","DOI":"10.1145\/503272.503274"},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"Beyer, D.: Advances in automatic software testing: Test-Comp 2025. In: Proc. FASE. pp. 257\u2013274. LNCS 15693, Springer (2025). DOI: 10.1007\/978-3-031-90900-9_13.","DOI":"10.1007\/978-3-031-90900-9_13"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Evaluating tools for automatic software testing (Report on Test-Comp 2026). In: Proc. FASE. pp. 449\u2013468. LNCS 16504, Springer (2026). https:\/\/doi.org\/10.1007\/978-3-032-22774-4_23","DOI":"10.1007\/978-3-032-22774-4_23"},{"key":"3_CR11","unstructured":"Beyer, D., Chien, P.C., Huang, B.Y., Lee, N.Z., Lemberger, T.: A case study in firmware verification: Applying formal methods to Intel \u00ae TDX Module (Appendix) (2026). https:\/\/www.sosy-lab.org\/research\/tdx-module-firmware-verification\/tacas26-appendix.pdf."},{"key":"3_CR12","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.16547223","author":"D Beyer","year":"2025","unstructured":"Beyer, D., Chien, P.C., Huang, B., Lee, N.Z., Lemberger, T.: The Intel TDX Module benchmark set. Zenodo (2025). DOI: 10.5281\/zenodo.16547223.","journal-title":"Zenodo"},{"key":"3_CR13","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.18371342","author":"D Beyer","year":"2026","unstructured":"Beyer, D., Chien, P.C., Huang, B., Lee, N.Z., Lemberger, T.: Reproduction package for TACAS 2026 article \u2018A case study in firmware verification: Applying formal methods to Intel TDX Module\u2019. Zenodo (2026). DOI: 10.5281\/zenodo.18371342.","journal-title":"Zenodo"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Beyer, D., Grunske, L., Kettl, M., Rosenfeld, M.L., Raselimo, M.: P3: A dataset of partial program patches. In: Proc. MSR. pp. 123\u2013127. ACM (2024). DOI: 10.1145\/3643991.3644889.","DOI":"10.1145\/3643991.3644889"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Proc. CAV. pp. 184\u2013190. LNCS 6806, Springer (2011). DOI: 10.1007\/978-3-642-22110-1_16.","DOI":"10.1007\/978-3-642-22110-1_16"},{"key":"3_CR16","doi-asserted-by":"crossref","unstructured":"Beyer, D., Petrenko, A.K.: Linux driver verification. In: Proc. ISoLA. pp. 1\u20136. LNCS 7610, Springer (2012). DOI: 10.1007\/978-3-642-34032-1_1.","DOI":"10.1007\/978-3-642-34032-1_1"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Beyer, D., Strejcek, J.: Improvements in software verification and witness validation: SV-COMP 2025. In: Proc. TACAS (3). pp. 151\u2013186. LNCS 15698, Springer (2025). DOI: 10.1007\/978-3-031-90660-2_9.","DOI":"10.1007\/978-3-031-90660-2_9"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Beyer, D., Strej\u010dek, J.: Evaluating software verifiers for C, Java, and SV-LIB (Report on SV-COMP 2026). In: Proc. TACAS (2). pp. 461\u2013502. LNCS 16506, Springer.  (2026). https:\/\/doi.org\/10.1007\/978-3-032-22749-2_23","DOI":"10.1007\/978-3-032-22749-2_23"},{"key":"3_CR19","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15012096","author":"D Beyer","year":"2025","unstructured":"Beyer, D., Strej\u010dek, J.: SV-Benchmarks: Benchmark set for software verification (SV-COMP 2025). Zenodo (2025). DOI: 10.5281\/zenodo.15012096.","journal-title":"Zenodo"},{"key":"3_CR20","unstructured":"Cadar, C., Dunbar, D., Engler, D.R.: Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proc. OSDI. pp. 209\u2013224. USENIX Association (2008). https:\/\/dl.acm.org\/doi\/10.5555\/1855741.1855756."},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Cadar, C., Nowack, M.: Klee symbolic execution engine in 2019 (competition contribution). Int. J. Softw. Tools Technol. Transf. 23(6), 867\u2013870 (2021). DOI: 10.1007\/s10009-020-00570-3.","DOI":"10.1007\/s10009-020-00570-3"},{"key":"3_CR22","doi-asserted-by":"crossref","unstructured":"Calcagno, C., Distefano, D., Dubreil, J., Gabi, D., Hooimeijer, P., Luca, M., O\u2019Hearn, P.W., Papakonstantinou, I., Purbrick, J., Rodriguez, D.: Moving fast with software verification. In: Proc. NFM. pp. 3\u201311. LNCS 9058, Springer (2015). DOI: 10.1007\/978-3-319-17524-9_1.","DOI":"10.1007\/978-3-319-17524-9_1"},{"issue":"4","key":"3_CR23","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1002\/spe.2949","volume":"51","author":"N Chong","year":"2021","unstructured":"Chong, N., Cook, B., Eidelman, J., Kallas, K., Khazem, K., Monteiro, F.R., Schwartz-Narbonne, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Code-level model checking in the software development workflow at Amazon Web Services. Softw. Pract. Exp. 51(4), 772\u2013797 (2021). doi: 10.1002\/spe.2949.","journal-title":"Softw. Pract. Exp."},{"issue":"5","key":"3_CR24","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"EM Clarke","year":"2003","unstructured":"Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752\u2013794 (2003). doi: 10.1145\/876638.876643.","journal-title":"J. ACM"},{"key":"3_CR25","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroning, D., Lerda, F.: A tool for checking ANSI-C programs. In: Proc. TACAS. pp. 168\u2013176. LNCS 2988, Springer (2004). DOI: 10.1007\/978-3-540-24730-2_15.","DOI":"10.1007\/978-3-540-24730-2_15"},{"issue":"1","key":"3_CR26","doi-asserted-by":"publisher","first-page":"34","DOI":"10.1007\/S10703-020-00344-2","volume":"57","author":"B Cook","year":"2021","unstructured":"Cook, B., Khazem, K., Kroning, D., Tasiran, S., Tautschnig, M., Tuttle, M.R.: Model checking boot code from AWS data centers. Formal Methods Syst. Des. 57(1), 34\u201352 (2021). doi: 10.1007\/S10703-020-00344-2.","journal-title":"Formal Methods Syst. Des."},{"issue":"2\/3","key":"3_CR27","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2\/3), 95\u2013120 (1988). doi: 10.1016\/0890-5401(88)90005-3.","journal-title":"Inf. Comput."},{"key":"3_CR28","unstructured":"Costan, V., Devadas, S.: Intel SGX explained. IACR Cryptol. ePrint Arch. pp. 86:1\u201386:118 (2016). http:\/\/eprint.iacr.org\/2016\/086."},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Fink, X., Berger, P., Katoen, J.P.: Configurable benchmarks for C model checkers. In: Proc. NFM. pp. 338\u2013354. LNCS 13260, Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-06773-0_18","DOI":"10.1007\/978-3-031-06773-0_18"},{"key":"3_CR30","doi-asserted-by":"publisher","unstructured":"Fox, A.C.J., Stockwell, G., Xiong, S., Becker, H., Mulligan, D.P., Petri, G., Chong, N.: A verification methodology for the Arm \u00aeConfidential Computing Architecture: From a secure specification to safe implementations. Proc. ACM Program. Lang. 7(OOPSLA1), 376\u2013405 (2023). https:\/\/doi.org\/10.1145\/3586040.","DOI":"10.1145\/3586040."},{"key":"3_CR31","doi-asserted-by":"crossref","unstructured":"Fraer, R., Keren, D., Khasidashvili, Z., Novakovsky, A., Puder, A., Singerman, E., Talmor, E., Vardi, M.Y., Yang, J.: From visual to logical formalisms for SoC validation. In: Proc. MEMOCODE. pp. 165\u2013174. IEEE (2014). DOI: 10.1109\/MEMCOD.2014.6961855.","DOI":"10.1109\/MEMCOD.2014.6961855"},{"key":"3_CR32","doi-asserted-by":"crossref","unstructured":"Gadelha, M.R., Monteiro, F.R., Morse, J., Cordeiro, L.C., Fischer, B., Nicole, D.A.: ESBMC 5.0: An industrial-strength C model checker. In: Proc. ASE. pp. 888\u2013891. ACM (2018). DOI: 10.1145\/3238147.3240481.","DOI":"10.1145\/3238147.3240481"},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Geppert, T., Deml, S., Sturzenegger, D., Ebert, N.: Trusted execution environments: Applications and organizational challenges. Frontiers Comput. Sci. 4, 930741:1\u2013930741:6 (2022). DOI: 10.3389\/FCOMP.2022.930741.","DOI":"10.3389\/fcomp.2022.930741"},{"key":"3_CR34","doi-asserted-by":"crossref","unstructured":"Goel, A., Krstic, S., Leslie, R., Tuttle, M.R.: SMT-based system verification with DVF. In: Proc. SMT. EPiC Series in Computing, vol. 20, pp. 32\u201343. EasyChair (2012). DOI: 10.29007\/59RN.","DOI":"10.29007\/59rn"},{"key":"3_CR35","doi-asserted-by":"crossref","unstructured":"Gro\u00dfe, D., K\u00fchne, U., Drechsler, R.: HW\/SW co-verification of embedded systems using bounded model checking. In: Proc. GLSVLSI. pp. 43\u201348. ACM (2006). DOI: 10.1145\/1127908.1127920.","DOI":"10.1145\/1127908.1127920"},{"key":"3_CR36","doi-asserted-by":"crossref","unstructured":"Guo, Y., Wang, Z., Zhong, B., Zeng, Q.: Formal modeling and security analysis for intra-level privilege separation. In: Proc. ACSAC. pp. 88\u2013101. ACM (2022). DOI: 10.1145\/3564625.3567984.","DOI":"10.1145\/3564625.3567984"},{"key":"3_CR37","unstructured":"Hania, B., Villard, M., Netzer, Y., Kodalapura, N., Nguyen, T.: Technical report of joint security review by Microsoft and Intel on Intel TDX1.5. Tech. rep., Intel Corporation and Microsoft Corporation (August 2024). https:\/\/www.intel.com\/content\/dam\/www\/public\/us\/en\/security-advisory\/documents\/intel_tdx_joint_security_review_with_microsoft.pdf."},{"key":"3_CR38","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Bentele, M., Dietsch, D., Jiang, X., Klumpp, D., Schussele, F., Podelski, A.: Ultimate Automizer and the abstraction of bitwise operations (competition contribution). In: Proc. TACAS (3). pp. 418\u2013423. LNCS 14572, Springer (2024). DOI: 10.1007\/978-3-031-57256-2_31.","DOI":"10.1007\/978-3-031-57256-2_31"},{"key":"3_CR39","doi-asserted-by":"crossref","unstructured":"Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Proc. CAV. pp. 36\u201352. LNCS 8044, Springer (2013). DOI: 10.1007\/978-3-642-39799-8_2.","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"3_CR40","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54828-5","author":"V Herdt","year":"2021","unstructured":"Herdt, V., Gro\u00dfe, D., Drechsler, R.: Enhanced Virtual Prototyping: Featuring RISC-V Case Studies. Springer (2021). doi: 10.1007\/978-3-030-54828-5.","journal-title":"Springer"},{"key":"3_CR41","doi-asserted-by":"crossref","unstructured":"Horn, A., Tautschnig, M., Val, C., Liang, L., Melham, T., Grundy, J., Kroening, D.: Formal co-validation of low-level hardware\/software interfaces. In: Proc. FMCAD. pp. 121\u2013128. IEEE (2013). DOI: 10.1109\/FMCAD.2013.6679400.","DOI":"10.1109\/FMCAD.2013.6679400"},{"key":"3_CR42","doi-asserted-by":"crossref","unstructured":"Huang, B.Y., Ray, S., Gupta, A., Fung, J.M., Malik, S.: Formal security verification of concurrent firmware in SoCs using instruction-level abstraction for hardware. In: Proc. DAC. pp. 91:1\u201391:6. ACM (2018). DOI: 10.1145\/3195970.3196055.","DOI":"10.1145\/3195970.3196055"},{"key":"3_CR43","doi-asserted-by":"crossref","unstructured":"Huang, B.Y., Zhang, H., Subramanyan, P., Vizel, Y., Gupta, A., Malik, S.: Instruction-level abstraction (ILA): A uniform specification for system-on-chip (SoC) verification. ACM Trans. Des. Autom. Electron. Syst. 24(1), 10:1\u201310:24 (2018). DOI: 10.1145\/3282444.","DOI":"10.1145\/3282444"},{"key":"3_CR44","unstructured":"ISO\/IEC JTC 1\/SC 22: ISO\/IEC 9899\u20132018: Information technology - Programming Languages - C. International Organization for Standardization (2018), https:\/\/www.iso.org\/standard\/74528.html."},{"issue":"2","key":"3_CR45","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1109\/MSEC.2019.2947124","volume":"18","author":"P Jauernig","year":"2020","unstructured":"Jauernig, P., Sadeghi, A., Stapf, E.: Trusted execution environments: Properties, applications, and challenges. IEEE Secur. Priv. 18(2), 56\u201360 (2020). doi: 10.1109\/MSEC.2019.2947124.","journal-title":"IEEE Secur. Priv."},{"key":"3_CR46","doi-asserted-by":"crossref","unstructured":"Journault, M., Min\u00e9, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: Proc. VSTTE. pp. 1\u201318. LNCS 12031, Springer (2019). DOI: 10.1007\/978-3-030-41600-3_1.","DOI":"10.1007\/978-3-030-41600-3_1"},{"key":"3_CR47","doi-asserted-by":"crossref","unstructured":"Khoroshilov, A.V., Mutilin, V.S., Petrenko, A.K., Zakharov, V.: Establishing Linux driver verification process. In: Proc. Ershov Memorial Conference. pp. 165\u2013176. LNCS 5947, Springer (2009). DOI: 10.1007\/978-3-642-11486-1_14.","DOI":"10.1007\/978-3-642-11486-1_14"},{"key":"3_CR48","doi-asserted-by":"crossref","unstructured":"Krsti\u0107, S., Yang, J., Palmer, D.W., Osborne, R.B., Talmor, E.: Security of SoC firmware load protocols. In: Proc. HOST. pp. 70\u201375. IEEE (2014). DOI: 10.1109\/HST.2014.6855571.","DOI":"10.1109\/HST.2014.6855571"},{"key":"3_CR49","doi-asserted-by":"crossref","unstructured":"Kroning, D., Tautschnig, M.: Cbmc: C bounded model checker (competition contribution). In: Proc. TACAS. pp. 389\u2013391. LNCS 8413, Springer (2014). DOI: 10.1007\/978-3-642-54862-8_26.","DOI":"10.1007\/978-3-642-54862-8_26"},{"key":"3_CR50","doi-asserted-by":"crossref","unstructured":"Lal, A., Qadeer, S.: Powering the static driver verifier using Corral. In: Proc. FSE. pp. 202\u2013212. ACM (2014). DOI: 10.1145\/2635868.2635894.","DOI":"10.1145\/2635868.2635894"},{"key":"3_CR51","doi-asserted-by":"crossref","unstructured":"Lee, H., Kim, S., Cha, S.K.: Fuzzle: Making a puzzle for fuzzers. In: Proc. ASE. ACM (2022). DOI: 10.1145\/3551349.3556908.","DOI":"10.1145\/3551349.3556908"},{"key":"3_CR52","doi-asserted-by":"crossref","unstructured":"Leslie-Hurd, R., Caspi, D., Fernandez, M.: Verifying linearizability of Intel\u00ae software guard extensions. In: Proc. CAV. pp. 144\u2013160. LNCS 9207, Springer (2015). DOI: 10.1007\/978-3-319-21668-3_9.","DOI":"10.1007\/978-3-319-21668-3_9"},{"key":"3_CR53","unstructured":"Li, X., Li, X., Dall, C., Gu, R., Nieh, J., Sait, Y., Stockwell, G.: Design and verification of the Arm Confidential Compute Architecture. In: Proc. OSDI. pp. 465\u2013484. USENIX Association (2022). https:\/\/www.usenix.org\/conference\/osdi22\/presentation\/li."},{"issue":"3","key":"3_CR54","doi-asserted-by":"publisher","first-page":"352","DOI":"10.1109\/TST.2016.7488746","volume":"21","author":"R Ma","year":"2016","unstructured":"Ma, R., Wang, D., Hu, C., Ji, W., Xue, J.: Test data generation for stateful network protocol fuzzing using a rule-based state machine. Tsinghua Science and Technology 21(3), 352\u2013360 (2016). doi: 10.1109\/TST.2016.7488746.","journal-title":"Tsinghua Science and Technology"},{"key":"3_CR55","doi-asserted-by":"crossref","unstructured":"Ma, Y., Zhang, Q., Zhao, S., Wang, G., Li, X., Shi, Z.: Formal verification of memory isolation for the TrustZone-based TEE. In: Proc. APSEC. pp. 149\u2013158. IEEE (2020). DOI: 10.1109\/APSEC51365.2020.00023.","DOI":"10.1109\/APSEC51365.2020.00023"},{"key":"3_CR56","doi-asserted-by":"crossref","unstructured":"Malik, S., Subramanyan, P.: Invited - Specification and modeling for systems-on-chip security verification. In: Proc. DAC. pp. 66:1\u201366:6. ACM (2016). DOI: 10.1145\/2897937.2911991.","DOI":"10.1145\/2897937.2911991"},{"key":"3_CR57","doi-asserted-by":"crossref","unstructured":"McKeen, F., Alexandrovich, I., Berenzon, A., Rozas, C.V., Shafi, H., Shanbhogue, V., Savagaonkar, U.R.: Innovative instructions and software model for isolated execution. In: Proc. HASP. ACM (2013). DOI: 10.1145\/2487726.2488368.","DOI":"10.1145\/2487726.2488368"},{"issue":"1","key":"3_CR58","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1109\/TDSC.2021.3133576","volume":"20","author":"X Miao","year":"2023","unstructured":"Miao, X., Chang, R., Zhao, J., Zhao, Y., Cao, S., Wei, T., Jiang, L., Ren, K.: CVTEE: A compatible verified TEE architecture with enhanced security. IEEE Trans. Dependable Secure Comput. 20(1), 377\u2013391 (2023). doi: 10.1109\/TDSC.2021.3133576.","journal-title":"IEEE Trans. Dependable Secure Comput."},{"key":"3_CR59","doi-asserted-by":"publisher","unstructured":"Moloney, C., Dyer, R., Sherman, E.: Demonstrating ARG-V\u2019s generation of realistic Java benchmarks for SV-COMP. In: Proc. TACAS (2).  pp. 277\u2013285. LNCS 16506, Springer (2026). https:\/\/doi.org\/10.1007\/978-3-032-22749-2_14","DOI":"10.1007\/978-3-032-22749-2_14"},{"key":"3_CR60","doi-asserted-by":"publisher","unstructured":"Monat, R., Ouadjaout, A., Mine, A.: Mopsa-C with trace partitioning and autosuggestions (competition contribution). In: Proc. TACAS (3). pp. 229\u2013235. LNCS 15698, Springer (2025). https:\/\/doi.org\/10.1007\/978-3-031-90660-2_17","DOI":"10.1007\/978-3-031-90660-2_17"},{"key":"3_CR61","doi-asserted-by":"crossref","unstructured":"Mukherjee, R., Purandare, M., Polig, R., Kroening, D.: Formal techniques for effective co-verification of hardware\/software co-designs. In: Proc. DAC. pp. 35:1\u201335:6. ACM (2017). DOI: 10.1145\/3061639.3062253.","DOI":"10.1145\/3061639.3062253"},{"key":"3_CR62","doi-asserted-by":"crossref","unstructured":"Mulligan, D.P., Petri, G., Spinale, N., Stockwell, G., Vincent, H.J.M.: Confidential computing - A brave new world. In: Proc. SEED. pp. 132\u2013138. IEEE (2021). DOI: 10.1109\/SEED51797.2021.00025.","DOI":"10.1109\/SEED51797.2021.00025"},{"key":"3_CR63","doi-asserted-by":"crossref","unstructured":"Mu\u00f1oz, A., Rios, R., Rom\u00e1n, R., L\u00f3pez, J.: A survey on the (in)security of trusted execution environments. Comput. Secur. 129, 103180:1\u2013103180:26 (2023). DOI: 10.1016\/J.COSE.2023.103180.","DOI":"10.1016\/j.cose.2023.103180"},{"key":"3_CR64","doi-asserted-by":"crossref","unstructured":"Nguyen, M.D., Wedler, M., Stoffel, D., Kunz, W.: Formal hardware\/software co-verification by interval property checking with abstraction. In: Proc. DAC. pp. 510\u2013515. ACM (2011). DOI: 10.1145\/2024724.2024843.","DOI":"10.1145\/2024724.2024843"},{"key":"3_CR65","doi-asserted-by":"crossref","unstructured":"Novikov, E., Zakharov, I.S.: Towards automated static verification of GNU C programs. In: Proc. PSI. pp. 402\u2013416. LNCS 10742, Springer (2017). DOI: 10.1007\/978-3-319-74313-4_30.","DOI":"10.1007\/978-3-319-74313-4_30"},{"key":"3_CR66","doi-asserted-by":"crossref","unstructured":"Ray, S., Ghosh, N., Masti, R.J., Kanuparthi, A., Fung, J.M.: Formal verification of security critical hardware-firmware interactions in commercial SoCs. In: Proc. DAC. pp. 43:1\u201343:4. ACM (2019). DOI: 10.1145\/3316781.3323478.","DOI":"10.1145\/3316781.3323478"},{"key":"3_CR67","doi-asserted-by":"crossref","unstructured":"Sabt, M., Achemlal, M., Bouabdallah, A.: Trusted execution environment: What it is, and what it is not. In: Proc. TrustCom. pp. 57\u201364. IEEE (2015). DOI: 10.1109\/TRUSTCOM.2015.357.","DOI":"10.1109\/Trustcom.2015.357"},{"key":"3_CR68","doi-asserted-by":"crossref","unstructured":"Sardar, M.U., Fetzer, C.: Confidential computing and related technologies: A critical review. Cybersecur. 6(1), 10:1\u201310:7 (2023). DOI: 10.1186\/S42400-023-00144-1.","DOI":"10.1186\/s42400-023-00144-1"},{"key":"3_CR69","doi-asserted-by":"crossref","unstructured":"Sardar, M.U., Faqeh, R., Fetzer, C.: Formal foundations for Intel SGX data center attestation primitives. In: Proc. ICFEM. pp. 268\u2013283. Springer (2020). DOI: 10.1007\/978-3-030-63406-3_16.","DOI":"10.1007\/978-3-030-63406-3_16"},{"key":"3_CR70","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1109\/ACCESS.2023.3346501","volume":"12","author":"MU Sardar","year":"2023","unstructured":"Sardar, M.U., Fossati, T., Frost, S., Xiong, S.: Formal specification and verification of architecturally-defined attestation mechanisms in Arm CCA and Intel TDX. IEEE Access 12, 361\u2013381 (2023). doi: 10.1109\/ACCESS.2023.3346501.","journal-title":"IEEE Access"},{"key":"3_CR71","doi-asserted-by":"publisher","first-page":"83067","DOI":"10.1109\/ACCESS.2021.3087421","volume":"9","author":"MU Sardar","year":"2021","unstructured":"Sardar, M.U., Musaev, S., Fetzer, C.: Demystifying attestation in Intel Trust Domain Extensions via formal verification. IEEE Access 9, 83067\u201383079 (2021). doi: 10.1109\/ACCESS.2021.3087421.","journal-title":"IEEE Access"},{"key":"3_CR72","doi-asserted-by":"crossref","unstructured":"Sardar, M.U., Quoc, D.L., Fetzer, C.: Towards formalization of enhanced privacy ID (EPID)-based remote attestation in Intel SGX. In: Proc. DSD. pp. 604\u2013607. IEEE (2020). DOI: 10.1109\/DSD51259.2020.00099.","DOI":"10.1109\/DSD51259.2020.00099"},{"key":"3_CR73","doi-asserted-by":"crossref","unstructured":"Schmidt, B., Villarraga, C., Bormann, J., Stoffel, D., Wedler, M., Kunz, W.: A computational model for SAT-based verification of hardware-dependent low-level embedded system software. In: Proc. ASP-DAC. pp. 711\u2013716. IEEE (2013). DOI: 10.1109\/ASPDAC.2013.6509684.","DOI":"10.1109\/ASPDAC.2013.6509684"},{"issue":"5","key":"3_CR74","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: Synthesizing programs of realistic structure. Int. J. Softw. Tools Technol. Transfer 16(5), 465\u2013479 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"3_CR75","doi-asserted-by":"crossref","unstructured":"Subramanyan, P., Sinha, R., Lebedev, I., Devadas, S., Seshia, S.A.: A formal foundation for secure remote execution of enclaves. In: Proc. CCS. pp. 2435\u20132450. ACM (2017). DOI: 10.1145\/3133956.3134098.","DOI":"10.1145\/3133956.3134098"},{"key":"3_CR76","doi-asserted-by":"crossref","unstructured":"Westhofen, L., Berger, P., Katoen, J.P.: Benchmarking software model checkers on automotive code. In: Proc. NFM. pp. 133\u2013150. LNCS 12229, Springer (2020). DOI: 10.1007\/978-3-030-55754-6_8.","DOI":"10.1007\/978-3-030-55754-6_8"},{"key":"3_CR77","doi-asserted-by":"crossref","unstructured":"Wu, P., Shen, Q., Deng, R.H., Liu, X., Zhang, Y., Wu, Z.: ObliDC: An SGX-based oblivious distributed computing framework with formal proof. In: Proc. Asia CCS. pp. 86\u201399. ACM (2019). DOI: 10.1145\/3321705.3329822.","DOI":"10.1145\/3321705.3329822"},{"key":"3_CR78","doi-asserted-by":"crossref","unstructured":"Wu, T., Li, X., Manino, E., Menezes, R., Gadelha, M., Xiong, S., Tihanyi, N., Petoumenos, P., Cordeiro, L.: ESBMC v7.7: Efficient concurrent software verification with scheduling, incremental SMT and partial order reduction (competition contribution). In: Proc. TACAS (3). pp. 223\u2013228. LNCS 15698, Springer (2025). DOI: 10.1007\/978-3-031-90660-2_16.","DOI":"10.1007\/978-3-031-90660-2_16"},{"key":"3_CR79","doi-asserted-by":"publisher","unstructured":"Wu, T., Xiong, S., Manino, E., Stockwell, G., Cordeiro, L.C.: Verifying components of Arm \u00ae Confidential Computing Architecture with ESBMC. In: Proc. SAS. pp. 451\u2013462. LNCS 14995, Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-74776-2_18","DOI":"10.1007\/978-3-031-74776-2_18"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-22749-2_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,15]],"date-time":"2026-04-15T13:12:17Z","timestamp":1776258737000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-22749-2_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026]]},"ISBN":["9783032227485","9783032227492"],"references-count":79,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-22749-2_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2026]]},"assertion":[{"value":"15 April 2026","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The source code of TDX Module, the developed proof harnesses, and the derived verification tasks are archived on Zenodo\u00a0[\n                      \n                      ]. An artifact for reproducing the results presented in Sect.\u00a0\n                      \n                      is also available on Zenodo\u00a0[\n                      \n                      ]. In addition, a supplementary webpage is hosted at\n                      \n                      .","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Data-Availability Statement"}},{"value":"This project was funded by the Deutsche Forschungsgemeinschaft (DFG) \u2013\n                      \n                      (\n                      \n                      ) and\n                      \n                      (Bridge), and a research gift from Intel.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Funding Statement"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Turin","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2026","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2026","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 April 2026","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"32","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2026","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/about\/tacas\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}