Software and Computational Systems Lab

Publications about Firmware verification

1. Dirk Beyer, Po-Chun Chien, Bo-Yuan Huang, Nian-Ze Lee, and Thomas Lemberger. A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module. In Proceedings of the 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2026, Turin, Italy, April 11-16), LNCS, 2026. Springer. Keyword(s): Software Model Checking, Software Testing, Firmware verification Funding: DFG-CONVEY, DFG-BRIDGE, Intel Supplement
   Artifact(s)

   1. doi:10.5281/zenodo.18371342
   Abstract

   Firmware underpins system security but remains challenging to verify due to hardware dependency, specialized coding idioms, and limited open-source examples. Manual verification approaches, while common in industry, are labor-intensive and difficult to scale. This paper presents a detailed case study on applying automatic formal methods for software to a security-critical firmware component in Intel Trust Domain Extensions (TDX), known as TDX Module. In this study, we employ six state-of-the-art C-program analyzers on the production TDX Module firmware, leveraging techniques ranging from bounded model checking and symbolic execution to abstract interpretation. Our empirical evaluation identifies obstacles unique to firmware, highlights harness-design decisions essential for verifying industry-scale code bases, and demonstrates opportunities in advanced slicing for more scalable verification. Although the case study focuses on TDX Module, the findings are broadly applicable to large-scale, low-level programs and have already influenced the software-verification community, such as standardizing nondeterministic object initialization. All verification tasks and proof harnesses are publicly released to foster reproducible research and future tool development.
   BibTeX Entry

   @inproceedings{TACAS26a, author = {Dirk Beyer and Po-Chun Chien and Bo-Yuan Huang and Nian-Ze Lee and Thomas Lemberger}, title = {{A} Case Study in Firmware Verification: {Applying} Formal Methods to {Intel TDX Module}}, booktitle = {Proceedings of the 31th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS~2026, Turin, Italy, April 11-16)}, pages = {}, year = {2026}, series = {LNCS}, publisher = {Springer}, doi = {}, url = {https://www.sosy-lab.org/research/tdx-module-firmware-verification/}, abstract = {Firmware underpins system security but remains challenging to verify due to hardware dependency, specialized coding idioms, and limited open-source examples. Manual verification approaches, while common in industry, are labor-intensive and difficult to scale. This paper presents a detailed case study on applying automatic formal methods for software to a security-critical firmware component in Intel Trust Domain Extensions (TDX), known as TDX Module. In this study, we employ six state-of-the-art C-program analyzers on the production TDX Module firmware, leveraging techniques ranging from bounded model checking and symbolic execution to abstract interpretation. Our empirical evaluation identifies obstacles unique to firmware, highlights harness-design decisions essential for verifying industry-scale code bases, and demonstrates opportunities in advanced slicing for more scalable verification. Although the case study focuses on TDX Module, the findings are broadly applicable to large-scale, low-level programs and have already influenced the software-verification community, such as standardizing nondeterministic object initialization. All verification tasks and proof harnesses are publicly released to foster reproducible research and future tool development.}, keyword = {Software Model Checking, Software Testing, Firmware verification}, annote = {A preprint is available upon request and an <a href="https://www.sosy-lab.org/research/tdx-module-firmware-verification/tacas26-appendix.pdf">appendix</a> to this article is available on our supplementary webpage.}, artifact = {10.5281/zenodo.18371342}, funding = {DFG-CONVEY, DFG-BRIDGE, Intel}, }
   Additional Infos

   A preprint is available upon request and an appendix to this article is available on our supplementary webpage.