Serviço · Oferta âncora
Verificação de Firmware e Silício
Bounded model checking em escala na camada de código que é entregue uma vez e roda em todo lugar; microcódigo, raiz de confiança, supervisores de TEE, secure boot e firmware de plataforma.
Por que esta oferta
O firmware de silício é entregue uma vez e roda em todo lugar
Microcódigo, ROM de secure-boot, supervisores de TEE e firmware similar ficam abaixo do sistema operacional e fora 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 todo dispositivo construído sobre a peça.
Esta é a área em que a verificação formal tem o maior retorno por hora-engenheiro, e a área em que a Cyber-Reasoning Consultancy (CRC) tem o histórico publicado mais profundo.
Histórico comprovado
Duas colaborações industriais publicadas
- Intel. Em nossa colaboração publicada, a análise de intervalos levou um firmware de Core Power Management de 190.000 LOC de um timeout de 3 dias a um veredito em 8 horas; o VO-GCSE entregou um speedup de 1.500% em um padrão de código de firmware representativo (arXiv 2406.15281; FSE Companion 2025).
- Arm. Em nossa colaboração no SAS 2024 com engenheiros da Arm, o ESBMC identificou 23 violações de propriedade adicionais no Realm Management Monitor, o firmware privilegiado na raiz de confiança da Armv9 Confidential Computing Architecture, além daquelas já detectadas pelo CBMC, e contribuiu com uma correção confirmada de modelo de memória upstream.
O que verificamos
Classes de firmware-alvo
Como entregamos
As técnicas por trás dos estudos de caso
Geração de harness orientada por especificação
Onde existem especificações legíveis por máquina (por exemplo, Arm RMM), geramos harnesses de verificação diretamente da especificação para avaliar pré/pós-condições na implementação. Demonstrado em nosso estudo de caso Arm CCA do SAS 2024.
Análise de intervalos no nível GOTO
Interpretação abstrata que aperta os limites das variáveis do programa e fornece invariantes mais fortes à k-induction. Levou um código de firmware Intel de 190.000 LOC de um timeout de 3 dias a um veredito em 8 horas (arXiv 2406.15281).
GCSE Orientado à Verificação
Uma passagem de Global Common Subexpression Elimination direcionada à verificação que roda no IR GOTO do ESBMC, eliminando computações redundantes de desreferência de ponteiro e de subexpressão antes da execução simbólica. Disponível no ESBMC 7.5+ (FSE Companion 2025).
Integração entre ferramentas
O GOTO Transcoder permite ao ESBMC consumir arquivos GOTO produzidos por Kani / CBMC, de modo que podemos nos conectar a fluxos de CI existentes ao lado de um verificador já em uso e revelar achados complementares (como fizemos no projeto model-checking/verify-rust-std).
Adequação por setor
Onde isto se encaixa
Semicondutores
Integração de CI de microcódigo, verificação de firmware de secure-element / TEE, apoio à resiliência de firmware de plataforma NIST SP 800-193. Comprovado por nossas colaborações publicadas com Intel e Arm.
Automotivo
Capacidade-alvo para verificação de firmware com classificação ASIL, engenharia de cibersegurança ISO/SAE 21434 para SoCs automotivos e verificação de componentes AUTOSAR, combinada com nosso serviço de Apoio à Qualificação de Ferramentas e Certificação.
Aeroespacial
Capacidade-alvo para verificação de firmware de classe DO-178C DAL A/B (FMS, FADEC e outros firmwares embarcados), combinada com nosso serviço de Apoio à Qualificação de Ferramentas e Certificação para a evidência de qualificação DO-330.
Verificando firmware de silício?
Conte-nos sobre a família de firmware e o padrão de segurança ou de segurança da informação que você está buscando alcançar. Vamos escopar um engajamento de descoberta que mapeia de forma limpa sobre nossos manuais publicados de Intel e Arm.