Verificação Formal Escalável
de Firmware
Uma aceleração de verificação de 1.500% em um padrão de código de firmware representativo, e um firmware de 190.000 LOC que antes sofria timeout após três dias verificado em oito horas.
1.500%
Aceleração em um padrão de código de firmware representativo (105 s → <7 s)
8 hrs
Verificando firmware de 190.000 LOC com análise de intervalos (vs. timeout de 3 dias sem ela)
CI
ESBMC integrado ao pipeline de CI da Intel para microcódigo da família Core (segundo estudo de caso publicado)
94%
Contexto da indústria: CVEs de firmware de plataforma que a Intel atribui a esforços proativos (Intel 2024 Product Security Report)
Desafio
A Intel tem usado o ESBMC para automatizar a análise de firmware, incluindo o microcódigo da família de processadores Core, onde o ESBMC foi integrado ao pipeline de CI, e trabalhos anteriores no Authenticated Code Module que revelaram mais de 30 problemas durante a verificação pré-lançamento. À medida que a complexidade do firmware crescia, padrões repetidos de desreferência de ponteiros em código C voltado para hardware faziam com que o modelo de memória simbólica do ESBMC refizesse as mesmas computações de alvo muitas vezes, elevando os tempos de verificação além do que era operacionalmente útil.
Um problema distinto surgiu quando a Intel avaliou o ESBMC no Core Power Manager, um componente de proteção térmica que limita a frequência da CPU. A base de código tem cerca de 190.000 linhas de código (60 arquivos C e 50 headers) com aproximadamente 300 variáveis globais sinalizando eventos de hardware e um harness orientado a eventos modelado como um laço infinito não determinístico. Sem a análise de intervalos, o ESBMC sofria timeout após três dias; o firmware estava efetivamente fora de alcance.
Abordagem
Desenvolvedores da Intel vinham otimizando manualmente o código C do firmware, armazenando em cache desreferências de ponteiros repetidas em variáveis intermediárias, para tornar a verificação tratável. Trabalhando com esses especialistas de domínio, generalizamos e automatizamos o padrão como VO-GCSE: um algoritmo de eliminação de subexpressões comuns globais orientado à verificação que roda no nível da representação intermediária GOTO do ESBMC, eliminando computações redundantes de desreferência e de subexpressões antes da execução simbólica. A otimização foi contribuída ao upstream do projeto open-source ESBMC e passou a ser distribuída a partir do ESBMC 7.5.
Para o firmware Core Power Management, estendemos o ESBMC com análise de intervalos, interpretação abstrata que estreita os limites das variáveis do programa, remove caminhos inalcançáveis e fornece invariantes mais fortes à k-induction. Com a análise de intervalos habilitada no nível GOTO, o ESBMC chega a um veredicto sobre a base de código de 190.000 LOC (60 arquivos C e 50 headers, cerca de 300 variáveis globais de eventos de hardware) em oito horas, contra um timeout de três dias sem ela.
Resultados
Aceleração de 1.500% em um padrão de código de firmware representativo, o tempo de verificação caiu de 105 segundos (270.015 atribuições simbólicas) para menos de 7 segundos assim que o VO-GCSE eliminou as computações redundantes de desreferência.
O firmware Core Power Management (190.000 LOC), que sofria timeout após três dias sem a análise de intervalos, foi verificado em menos de oito horas com ela.
O VO-GCSE passou a ser distribuído no ESBMC a partir da versão 7.5; a análise de intervalos a partir da v7.4. Ambos estão disponíveis nos mesmos builds do ESBMC que a Intel utilizou para análise de firmware, incluindo o pipeline de CI reportado para o microcódigo da família Core.
Contexto da indústria. O Intel 2024 Product Security Report registra 374 CVEs tratadas em 2024 e atribui a descoberta e mitigação de 94% das vulnerabilidades de firmware de plataforma daquele ano ao seu programa proativo de garantia de segurança de produtos. O relatório da Intel não nomeia ferramentas específicas, e a Cyber-Reasoning Consultancy (CRC) não faz nenhuma afirmação de contribuição para esse número; ele é incluído apenas como pano de fundo do mercado de verificação de firmware no qual o ESBMC atua. Fonte: Intel 2024 Product Security Report (PDF).
Referências
- 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