Funding by Intel
Articles in conference or workshop proceedings
-
HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects.
In Proceedings of the 34th ACM International Conference on the Foundations
of Software Engineering (FSE Companion 2026, Montreal, Canada, July 5-9),
2026.
ACM.
Keyword(s):
Software Model Checking,
Software Testing,
Firmware verification
Funding:
DFG-CONVEY,
DFG-BRIDGE,
Intel
PDF
Video
Supplement
Artifact(s)
Abstract
We present HarnessForge, a command-line tool to streamline the extraction of verification tasks from industry-scale software projects written in C. Industry-scale code consists of multiple source and header files with various build processes, complicating the creation of verification tasks and hindering the applicability of off-the-shelf software verifiers. HarnessForge handles this complexity for verification engineers and tools, allowing harnesses to be structured independently from the code under verification. It automatically derives build commands, assembles relevant source files, and performs static program slicing to remove irrelevant components. To demonstrate its applicability, we use HarnessForge to create a total of 949 verification tasks from three projects: AWS C Common, GNU Coreutils, and Intel TDX Module. All created tasks were used in SV-COMP 2026. A demo video is available at youtu.be/wHPEfQ3NBFQ.BibTeX Entry
@inproceedings{FSE26, author = {Dirk Beyer and Po-Chun Chien and Bo-Yuan Huang and Nian-Ze Lee and Thomas Lemberger}, title = {HarnessForge: Automated Extraction of Verification Tasks from Industry-Scale Software Projects}, booktitle = {Proceedings of the 34th {ACM} International Conference on the Foundations of Software Engineering ({FSE} Companion 2026, Montreal, Canada, July 5-9)}, pages = {}, year = {2026}, publisher = {ACM}, url = {https://gitlab.com/sosy-lab/software/harnessforge}, pdf = {https://www.sosy-lab.org/research/pub/2026-FSE.HarnessForge_Automated_Extraction_of_Verification_Tasks_from_Industry-Scale_Software_Projects.pdf}, abstract = {We present HarnessForge, a command-line tool to streamline the extraction of verification tasks from industry-scale software projects written in C. Industry-scale code consists of multiple source and header files with various build processes, complicating the creation of verification tasks and hindering the applicability of off-the-shelf software verifiers. HarnessForge handles this complexity for verification engineers and tools, allowing harnesses to be structured independently from the code under verification. It automatically derives build commands, assembles relevant source files, and performs static program slicing to remove irrelevant components. To demonstrate its applicability, we use HarnessForge to create a total of 949 verification tasks from three projects: AWS C Common, GNU Coreutils, and Intel TDX Module. All created tasks were used in SV-COMP 2026. A demo video is available at <a href="https://youtu.be/wHPEfQ3NBFQ">youtu.be/wHPEfQ3NBFQ</a>.}, keyword = {Software Model Checking, Software Testing, Firmware verification}, artifact = {10.5281/zenodo.18348148}, doinone = {Unpublished: Last checked: 2026-03-22 (10.1145/3803437.3806420)}, funding = {DFG-CONVEY, DFG-BRIDGE, Intel}, video = {https://youtu.be/wHPEfQ3NBFQ}, } -
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), part 2,
LNCS 16506,
pages 42-64,
2026.
Springer.
doi:10.1007/978-3-032-22749-2_3
Keyword(s):
Software Model Checking,
Software Testing,
Firmware verification
Funding:
DFG-CONVEY,
DFG-BRIDGE,
Intel
Publisher's Version
PDF
Presentation
Poster
Supplement
Artifact(s)
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), part~2}, pages = {42-64}, year = {2026}, series = {LNCS~16506}, publisher = {Springer}, doi = {10.1007/978-3-032-22749-2_3}, url = {https://www.sosy-lab.org/research/tdx-module-firmware-verification/}, pdf = {https://www.sosy-lab.org/research/pub/2026-TACAS.A_Case_Study_in_Firmware_Verification_Applying_Formal_Methods_to_Intel_TDX_Module.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2026-04-13_TACAS_Intel_TDX_Nian-Ze.pdf}, poster = {https://www.sosy-lab.org/research/pst/2026-04-13_ETAPS_Firmware_Verification_TDX_Module_Poster.pdf}, 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 = {This article has been selected as an "<a href="https://etaps.org/2026/programme/">ETAPS Distinguished Paper</a>." 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
This article has been selected as an "ETAPS Distinguished Paper." An appendix to this article is available on our supplementary webpage.
Internal reports
-
A Case Study in Firmware Verification: Applying Formal Methods to Intel TDX Module (Appendix).
2026.
Keyword(s):
Software Model Checking,
Software Testing,
Firmware verification
Funding:
DFG-CONVEY,
DFG-BRIDGE,
Intel
PDF
Supplement
Artifact(s)
BibTeX Entry
@techreport{Appendix26, 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} (Appendix)}, year = {2026}, doi = {}, url = {https://www.sosy-lab.org/research/tdx-module-firmware-verification/}, pdf = {https://www.sosy-lab.org/research/tdx-module-firmware-verification/tacas26-appendix.pdf}, keyword = {Software Model Checking, Software Testing, Firmware verification}, annote = {This is an appendix to our <a href="https://www.sosy-lab.org/research/bib/All/index.html#TACAS26a">TACAS 2026 paper</a>.}, artifact = {10.5281/zenodo.18371342}, funding = {DFG-CONVEY, DFG-BRIDGE, Intel}, }Additional Infos
This is an appendix to our TACAS 2026 paper.
Disclaimer:
This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.