An Industrial Challenge for Firmware Verification:
The Intel TDX Module Benchmark Set
The benchmark set is available on
1.5.05),
and the derived verification tasks.
The task-generation process is automated using
HarnessForge.
This work is supported by a research gift from Intel.
A detailed technical report describing the project is also available upon request.
Abstract
Firmware plays a critical role in system security,
yet its verification remains underexplored due to challenges
such as hardware dependency, limited tool support, and the
scarcity of open-source examples. Compared to higher-level
programs, firmware exhibits unique characteristics that limit the
effectiveness of off-the-shelf software analyzers. To address these
barriers, we introduce the first open-source, publicly available
benchmark set for firmware verification, derived from a key
firmware component in the Intel Trust Domain Extensions (TDX)
technology. This benchmark set features the distinct traits of
firmware, representative security-relevant properties, and proof-harness
designs that reflect the verification demands in industry.
Our benchmark set contains automatically generated tasks that
comply with the rules of the Competition on Software Verification,
enabling the use and evaluation of 29 analyzers for C programs.
We conduct an extensive evaluation of tool readiness for firmware
verification, analyzing how firmware-specific traits, property types,
and harness engineering affect tool performance. Notably, our
findings have already sparked discussion within the verification
community, motivating efforts toward standardizing a mechanism
for nondeterministic object initialization. By making realistic
verification tasks that reflect the unique characteristics of firmware
publicly available, our work lowers the barrier to firmware-verification
research and provides a foundation for advancing
tool development in this critical domain.