Verificando o Firmware NVIDIA
OpenSMA com ESBMC
Uma prova de conceito reproduzível pela Cyber-Reasoning Consultancy (CRC) verificando módulos selecionados do NVIDIA OpenSMA, o firmware open-source para o microcontrolador MCXN556S que a NVIDIA distribui como System Management Agent para suas placas de data center. O ESBMC encontrou uma escrita fora dos limites explorável no validador MCTP, que a equipe OpenSMA da NVIDIA confirmou e corrigiu upstream.
F-1
Descoberta de acesso fora dos limites confirmada e corrigida upstream pela equipe NVIDIA OpenSMA (2026-05-11)
17
Descobertas distintas graduadas por rigor de prova no firmware open-source da NVIDIA
~30
Módulos C++23 de produção verificados pelo ESBMC em macOS aarch64
22+
Issues upstream do ESBMC reportadas e integradas ao longo da PoC
Contexto
O OpenSMA é o firmware open-source da NVIDIA para o microcontrolador NXP MCXN556S, implantado como System Management Agent nas placas de data center da NVIDIA. É C++23 de produção real, exercitando o Management Component Transport Protocol (MCTP), os tipos 2 / 3 / 5 do NVIDIA System Management (NSM), drivers de dispositivos I²C, pilhas de sensores (EMC1812, TMP1075, TMP461, termistores NTC), filtros SMA de suavização de potência, SSIF e um emulador de expansor GPIO PCA9555. Bugs nesta camada são remotos, ficam entre o host e o resto da placa, e difíceis de alcançar apenas com testes unitários.
Quisemos mostrar que o ESBMC pode ser apontado para esta base de código como está, sem reescrevê-la, e produzir tanto provas (para os módulos seguros) quanto contraexemplos concretos (para os inseguros), com fidelidade suficiente para que os mantenedores upstream aceitassem as descobertas.
Abordagem
Construímos harnesses de verificação limitada de modelos para cerca de 30 módulos em
corepdk/
(pacote, roteador e validador MCTP) e
src/nv/
(NSM, telemetria, bitmask, SPI, I²C, ponto fixo, tabela NTC, presets de suavização de
potência, FRU, filtros SMA, drivers de sensores, mailbox C2C, SSIF, despacho de
eventos). Cada alvo executa três perfis: Fase 1 de segurança da linguagem, Fase 2 de
contratos funcionais por k-induction e um perfil de verificação de volatile, além de
testes negativos que deliberadamente acionam o caminho inseguro.
A Fase 1 habilita
--memory-leak-check --overflow-check --unsigned-overflow-check --nan-check
com sobrescritas de --unwind
por alvo; a Fase 2 ativa
--k-induction --interval-analysis
com --max-k-step 6
(16 para o validador MCTP) e as asserções de contrato
-DESBMC_FUNCTIONAL=1.
As descobertas são graduadas em uma escala publicada de Tiers A–G, com o Tier A
reservado a descobertas cuja alcançabilidade completa foi provada através da cadeia de
despacho de produção.
O harness, os resultados, os scripts de execução e o relatório estão abertos em
lucasccordeiro/NVIDIA-OpenSMA
(branch vr_sma).
Resultados
F-1 (Tier A) confirmada e corrigida upstream pela NVIDIA em 2026-05-11. Validator::validate()
protegia interface >= Interface::End (=18),
mas o array de cursores da tabela de roteamento
RoutingTable::ec.cur_eid
tem tamanho Interface::UsEnd (=2).
Qualquer interface em [2, 17]
passa pela validação e escreve fora dos limites em
set_cur_eid();
builds de produção usam -fno-exceptions,
então o acesso fora dos limites cai em
abort().
A equipe OpenSMA da NVIDIA aceitou o relatório e aplicou a correção recomendada
(NVIDIA/OpenSMA issue #1).
16 descobertas latentes adicionais em NSM, SSIF, telemetria e despacho de
eventos, incluindo armazenamentos de enum sem verificação
(errorInjectionMode),
um cast de signed para unsigned limitando
percent = −1024
a stored = 255
no canal SMA de telemetria de depuração, um acesso fora dos limites do bitmask de
fonte de evento em
event_id ≥ 64,
e um underflow de size_t
no ramo else do
smbus_block_read
do SSIF. Cada uma documentada com um contraexemplo concreto.
Três descobertas retratadas com prova, não com achismo. F-2, F-3
e F-14 (deslocamento com sinal / wrap sem sinal / uma questão de
return
vs break
no PCA9555) foram demonstradas benignas, no caso do PCA9555, por uma execução do
ESBMC com 405 condições de verificação mostrando equivalência observável.
22+ issues upstream do ESBMC reportadas e integradas ao longo da
PoC, normalização de fall-through em switch,
std::array
value-init de agregado, falsos positivos de inicializador de membro em bitfield
packed, cobertura de
--overflow-check
para deslocamento negativo, e mais. Maior prova individual da suíte: o emulador de
expansor GPIO PCA9555, verificado com 1292 condições de verificação na Fase 1.
O que isso significa
Um único engenheiro pode pegar uma base de código de firmware de produção open-source desconhecida, escrita em C++23 moderno, voltada para um microcontrolador que ele não possui, e usar o ESBMC para produzir descobertas acionáveis pelo fornecedor em poucas semanas. O resultado no OpenSMA é uma escrita fora dos limites real corrigida upstream, dezesseis outros defeitos latentes com contraexemplos concretos, três retratações honestas respaldadas por prova, e uma contribuição mensurável de volta ao ferramental de verificação open-source que tornou tudo possível.
Referências
-
lucasccordeiro/NVIDIA-OpenSMA, repositório público da PoC (branch
vr_sma: harnesses, stubs, scripts de execução, registro de descobertas, reprodutores de bugs do ESBMC). github.com/lucasccordeiro/NVIDIA-OpenSMA/tree/vr_sma/verification - NVIDIA/OpenSMA, projeto de firmware upstream; confirmação e correção da F-1 na issue #1. github.com/NVIDIA/OpenSMA/issues/1
- ESBMC, verificador limitado de modelos open-source. github.com/esbmc/esbmc
Nota. Esta página descreve uma prova de conceito independente liderada pelo fundador da CRC e criador e desenvolvedor líder do ESBMC, Prof. Lucas Cordeiro (University of Manchester). A CRC Ltd não mantém parceria comercial com a NVIDIA; o relatório e a correção da F-1 passaram pelo rastreador de issues público do OpenSMA da NVIDIA. Nenhum CVE foi registrado porque a correção foi aplicada pelo processo normal de manutenção do projeto. Números, contraexemplos e atribuições de tier são reproduzíveis a partir do repositório público.