Semicondutor
Verificação de Firmware para Silício
Verificação formal para microcódigo de processador, firmware de plataforma, root-of-trust e componentes TEE, o tipo de código de baixo nível em que uma única violação de propriedade pode comprometer toda uma linha de produtos.
O desafio
O firmware de silício é entregue uma vez e roda em todo lugar
Microcódigo, ROM de secure-boot, supervisores de TEE e firmware semelhante ficam abaixo do sistema operacional e além do alcance da maior parte da infraestrutura de testes. Uma vez entregues em silício, as correções são caras, e uma única violação de propriedade em um componente privilegiado pode minar as garantias de segurança de todos os dispositivos construídos sobre a peça.
O model checking limitado é a ferramenta apropriada para essa camada: ele produz ou uma prova matemática de que uma propriedade de segurança ou de proteção se mantém, ou um contraexemplo concreto mostrando exatamente como ela falha. O ESBMC foi aplicado a bases de código de firmware nessa escala em colaborações industriais publicadas.
Setores-alvo
Conformidade
Padrões que atendemos
Common Criteria (ISO/IEC 15408)
A verificação formal apoia os Evaluation Assurance Levels mais altos (EAL5+) tipicamente exigidos para firmware de elemento seguro, TEE e root-of-trust.
FIPS 140-3
O model checking limitado é uma técnica bem estabelecida para evidenciar a ausência de erros de segurança de memória e aritméticos em firmware de módulo criptográfico.
Arm PSA Certified / SESIP
Alinhado às expectativas de segurança por design impostas ao silício de dispositivos conectados e ao firmware de plataforma.
ISO/SAE 21434
Engenharia de cibersegurança para eletrônica de veículos rodoviários, relevante para semicondutores automotivos e o firmware com que são entregues.
ISO 26262
Segurança funcional para eletrônica automotiva, a verificação formal é altamente recomendada nos níveis ASIL mais altos.
NIST SP 800-193
Platform Firmware Resiliency Guidelines, os métodos formais apoiam os objetivos de proteção, detecção e recuperação.
Nosso papel
Como ajudamos
Firmware de microcódigo e de IP de processador
Model checking limitado em escala em microcódigo de processador e firmware de baixo nível. Nossa colaboração publicada com a Intel mostrou como a análise de intervalos torna viável uma base de código de firmware de 190.000 LOC em oito horas, onde antes havia excedido o tempo limite após três dias.
Componentes de root-of-trust e TEE
Verificação de propriedades de isolamento de memória, troca de mundos e autorização em componentes de firmware privilegiados. Nossa colaboração publicada com a Arm aplicou isso ao Realm Management Monitor no coração da Armv9 Confidential Computing Architecture.
Verificação pré-lançamento / pré-tape-out
Verificação formal de firmware antes do silício ser entregue, capturando violações de propriedade em harnesses representativos gerados a partir de especificações legíveis por máquina.
Integração de ferramenta de verificação em CI/CD
Ajudamos equipes de silício a incorporar o ESBMC em pipelines de CI existentes ao lado de outros model checkers, incluindo a reprodução de achados anteriores do CBMC e a revelação de violações adicionais que sobrevivem às toolchains existentes.
Geração de harness orientada por especificação
Onde existem especificações legíveis por máquina (por exemplo, a especificação RMM da Arm), geramos harnesses de verificação diretamente a partir da especificação para avaliar pré/pós-condições na implementação.
Otimização de tempo de verificação
Onde padrões redundantes de desreferência de ponteiro ou grandes espaços de estado disparam o custo da verificação, aplicamos otimizações do ESBMC como VO-GCSE e análise de intervalos, ambas presentes em builds de produção do ESBMC.
Colaborações publicadas
Onde isso já foi feito antes
Intel · Firmware
Verificação de firmware escalável
VO-GCSE e análise de intervalos aplicadas a código de firmware da Intel; firmware de 190.000 LOC verificado em oito horas versus um tempo limite de três dias sem análise de intervalos. Publicado no artigo de análise de intervalos (arXiv 2406.15281) e no FSE Companion 2025.
Arm · Computação Confidencial
Verificação do Realm Management Monitor
O ESBMC identificou 23 violações de propriedade adicionais no firmware RMM da Arm além daquelas já detectadas pelo CBMC, e contribuiu com uma correção de modelo de memória confirmada no upstream. Publicado no SAS 2024.
Verificando firmware de silício?
Vamos conversar sobre como a verificação formal baseada em ESBMC se encaixa no seu fluxo de garantia de firmware, do microcódigo ao root-of-trust e aos supervisores de TEE.