Verifying NVIDIA OpenSMA
Firmware with ESBMC
A reproducible proof-of-concept by Cyber-Reasoning Consultancy (CRC) verifying selected modules of NVIDIA OpenSMA — the open-source MCXN556S microcontroller firmware NVIDIA ships as the System Management Agent for its data-centre boards. ESBMC found an exploitable out-of-bounds write in the MCTP validator that NVIDIA's OpenSMA team confirmed and fixed upstream.
F-1
Out-of-bounds finding confirmed and fixed upstream by the NVIDIA OpenSMA team (2026-05-11)
17
Distinct findings graded by proof rigor across NVIDIA's open-source firmware
~30
Production C++23 modules verified by ESBMC on macOS aarch64
22+
ESBMC upstream issues filed and merged in the course of the PoC
Context
OpenSMA is NVIDIA's open-source firmware for the NXP MCXN556S microcontroller, deployed as the System Management Agent on NVIDIA data-centre boards. It is real production C++23, exercising the Management Component Transport Protocol (MCTP), NVIDIA System Management (NSM) types 2 / 3 / 5, I²C device drivers, sensor stacks (EMC1812, TMP1075, TMP461, NTC thermistors), power-smoothing SMA filters, SSIF, and a PCA9555 GPIO expander emulator. Bugs at this layer are remote — they sit between the host and the rest of the board — and difficult to reach with unit tests alone.
We wanted to show that ESBMC can be pointed at this codebase as-is, without rewriting it, and produce both proofs (for the safe modules) and concrete counterexamples (for the unsafe ones), with enough fidelity that the upstream maintainers would accept the findings.
Approach
We built bounded model-checking harnesses for roughly 30 modules across
corepdk/
(MCTP packet, router, validator) and
src/nv/
(NSM, telemetry, bitmask, SPI, I²C, fixed-point, NTC table, power-smoothing
presets, FRU, SMA filters, sensor drivers, C2C mailbox, SSIF, event dispatch).
Each target runs three profiles: Phase 1 language-safety, Phase 2 k-induction
functional contracts, and a volatile-check profile, plus negative tests that
deliberately drive the unsafe path.
Phase 1 enables
--memory-leak-check --overflow-check --unsigned-overflow-check --nan-check
with per-target --unwind
overrides; Phase 2 turns on
--k-induction --interval-analysis
with --max-k-step 6
(16 for the MCTP validator) and the
-DESBMC_FUNCTIONAL=1
contract assertions. Findings are graded on a published Tier A–G ladder, with
Tier A reserved for findings whose full reachability has been proved through the
production dispatch chain.
The harness, results, run scripts and report are open at
lucasccordeiro/NVIDIA-OpenSMA
(branch vr_sma).
Results
F-1 (Tier A) confirmed and fixed upstream by NVIDIA on 2026-05-11. Validator::validate()
guarded interface >= Interface::End (=18),
but the routing-table cursor array
RoutingTable::ec.cur_eid
has size Interface::UsEnd (=2).
Any interface in [2, 17]
passes validation and writes out of bounds in
set_cur_eid();
production builds with -fno-exceptions,
so the OOB hits
abort().
NVIDIA's OpenSMA team accepted the report and applied the recommended fix
(NVIDIA/OpenSMA issue #1).
16 additional latent findings across NSM, SSIF, telemetry and event
dispatch — including unchecked enum stores
(errorInjectionMode),
a signed-to-unsigned cast clamping
percent = −1024
to stored = 255
in the debug-telemetry SMA channel, an event-source bitmask OOB at
event_id ≥ 64,
and a size_t
underflow in the SSIF
smbus_block_read
else-branch. Each is documented with a concrete counterexample.
Three findings retracted with proof, not handwaving. F-2, F-3
and F-14 (signed-shift / unsigned-wrap / a PCA9555
return
vs break
question) were demonstrated benign — for the PCA9555 case, by an ESBMC run of
405 verification conditions showing observable equivalence.
22+ ESBMC upstream issues filed and merged in the course of
the PoC — switch fall-through normalisation, std::array
aggregate value-init, packed-bitfield member-initialiser false positives,
--overflow-check
negative-shift coverage, and more. Largest single proof in the suite: the
PCA9555 GPIO expander emulator, verified with 1292 verification conditions
under Phase 1.
What this means
A single engineer can take an unfamiliar, open-source, production firmware codebase — written in modern C++23, targeting a microcontroller they do not own — and use ESBMC to produce vendor-actionable findings within weeks. The result on OpenSMA is a real out-of-bounds write fixed upstream, sixteen further latent defects with concrete counterexamples, three honest retractions backed by proof, and a measurable contribution back to the open-source verification tooling that made it possible.
References
-
lucasccordeiro/NVIDIA-OpenSMA — public PoC repository (branch
vr_sma: harnesses, stubs, run scripts, findings ledger, ESBMC bug reproducers). github.com/lucasccordeiro/NVIDIA-OpenSMA/tree/vr_sma/verification - NVIDIA/OpenSMA — upstream firmware project; F-1 confirmation and fix in issue #1. github.com/NVIDIA/OpenSMA/issues/1
- ESBMC — open-source bounded model checker. github.com/esbmc/esbmc
Note. This page describes an independent proof-of-concept led by CRC's founder and ESBMC creator and lead developer, Prof. Lucas Cordeiro (University of Manchester). CRC Ltd is not in a commercial partnership with NVIDIA; the F-1 report and fix went through NVIDIA's public OpenSMA issue tracker. No CVE was filed because the fix was applied through the project's normal maintenance process. Numbers, counterexamples and tier assignments are reproducible from the public repository.