Scalable Formal Verification
of Firmware
A 1,500% verification speedup on a representative firmware code pattern — and a 190,000-LOC firmware that previously timed out after three days verified in eight hours.
1,500%
Speedup on a representative firmware code pattern (105 s → <7 s)
8 hrs
Verifying 190,000-LOC firmware with interval analysis (vs. 3-day timeout without it)
CI
ESBMC integrated into Intel's CI pipeline for Core-family microcode (per published case study)
94%
Industry context: platform firmware CVEs Intel attributes to proactive efforts (Intel 2024 Product Security Report)
Challenge
Intel has used ESBMC to automate firmware analysis — including microcode for the Core family of processors, where ESBMC has been integrated into the CI pipeline, and earlier work on the Authenticated Code Module that uncovered more than 30 issues during pre-release verification. As firmware complexity grew, repeated pointer-dereference patterns in hardware-facing C code caused ESBMC's symbolic memory model to redo the same target computations many times over, pushing verification times beyond what was operationally useful.
A separate problem arose when Intel assessed ESBMC on the Core Power Manager — a thermal-protection component that throttles CPU frequency. The codebase is around 190,000 lines of code (60 C files and 50 headers) with roughly 300 global variables flagging hardware events and an event-driven harness modelled as a non-deterministic infinite loop. Without interval analysis, ESBMC timed out after three days; the firmware was effectively beyond reach.
Approach
Intel developers had been hand-optimising firmware C code — caching repeated pointer dereferences in intermediate variables — to make verification tractable. Working with these domain experts, we generalised and automated the pattern as VO-GCSE: a verification-oriented global common subexpression elimination algorithm that runs at ESBMC's GOTO intermediate-representation level, eliminating redundant dereference and subexpression computations before symbolic execution. The optimisation was contributed upstream to the open-source ESBMC project and has shipped from ESBMC 7.5 onward.
For the Core Power Management firmware, we extended ESBMC with interval analysis — abstract interpretation that tightens the bounds on program variables, removes unreachable paths, and supplies stronger invariants to k-induction. With interval analysis enabled at the GOTO level, ESBMC reaches a verdict on the 190,000-LOC codebase (60 C files and 50 headers, around 300 global hardware-event variables) in eight hours — versus a three-day timeout without it.
Results
1,500% speedup on a representative firmware code pattern — verification time dropped from 105 seconds (270,015 symbolic assignments) to under 7 seconds once VO-GCSE eliminated the redundant dereference computations.
Core Power Management firmware (190,000 LOC) — which timed out after three days without interval analysis — verified in under eight hours with it.
VO-GCSE shipped in ESBMC from version 7.5; interval analysis from v7.4. Both are available in the same ESBMC builds Intel has used for firmware analysis, including the CI pipeline reported for Core-family microcode.
Industry context. Intel's 2024 Product Security Report records 374 CVEs addressed in 2024, and attributes the discovery and mitigation of 94% of platform firmware vulnerabilities that year to its proactive product security assurance programme. The Intel report does not name specific tools, and Cyber-Reasoning Consultancy (CRC) makes no claim of contribution to this figure — it is included only as background to the firmware-verification market in which ESBMC operates. Source: Intel 2024 Product Security Report (PDF).
References
- Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov, Mohannad Aldughaim, Rosiane de Freitas, Lucas C. Cordeiro. Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study. CoRR abs/2406.15281 (2024). arxiv.org/abs/2406.15281
- Rafael Sá Menezes, Norbert Tihanyi, Ridhi Jain, Alexander Levin, Rosiane de Freitas, Lucas C. Cordeiro. VO-GCSE: Verification Optimization through Global Common Subexpression Elimination. SIGSOFT FSE Companion 2025: 1060–1064. doi.org/10.1145/3696630.3728581