O motor
ESBMC
O Efficient SMT-based Context-Bounded Model Checker, uma ferramenta de verificação formal de nível de produção com mais de 50 prêmios em competições internacionais (SV-COMP e Test-Comp, 2012–2026) e estudos de caso industriais publicados na Intel, Arm, AWS e na Ethereum Foundation.
Procedência da pesquisa
Uma ferramenta de código aberto, construída abertamente desde 2008
O ESBMC começou em 2008 como parte da pesquisa de doutorado de Lucas Cordeiro na University of Southampton e tem sido desenvolvido continuamente desde então por uma comunidade aberta de contribuidores em Southampton, na Federal University of Amazonas e, desde 2018, na University of Manchester. A ferramenta está disponível publicamente como software de código aberto no GitHub, e os serviços de consultoria da Cyber-Reasoning Consultancy (CRC) são construídos em torno do mesmo lançamento público do ESBMC usado pela comunidade de pesquisa mais ampla. A CRC não é proprietária do ESBMC e não reivindica direitos exclusivos sobre ele; contribuímos e prestamos consultoria em torno de uma ferramenta com licença aberta.
Fundamentos
O que é verificação formal?
Um engenheiro estrutural não certifica uma ponte dirigindo um caminhão sobre ela. Ele aplica análise matemática para raciocinar sobre o comportamento da ponte sob todas as cargas. A verificação formal de software aplica o mesmo princípio ao código.
Os testes tradicionais verificam um conjunto finito de cenários. A verificação formal usa lógica matemática para raciocinar sobre toda execução possível de um programa; toda entrada, todo entrelaçamento de threads, todo caso extremo; e ou prova que as propriedades de segurança se mantêm, ou produz um contraexemplo concreto que mostra exatamente como elas podem falhar.
O ESBMC implementa verificação limitada de modelos (BMC) e k-indução, codificando seu programa como um conjunto de restrições lógicas e entregando-as a um solucionador SMT. O solucionador ou confirma que as restrições são satisfatíveis (encontrando um bug, com um traço de contraexemplo) ou prova que são insatisfatíveis, uma garantia formal de correção dentro do limite de verificação, estendida a provas ilimitadas via k-indução onde aplicável.
Analisar o código-fonte
O ESBMC analisa C, C++, Rust, Python e outras linguagens suportadas em uma representação intermediária GOTO interna.
Codificar como restrições SMT
O programa é desenrolado até um limite configurável e codificado como fórmulas de Satisfatibilidade Módulo Teorias (SMT).
Entregar a um solucionador SMT
Um solucionador SMT industrial (Z3, Bitwuzla, etc.) determina se existe um contraexemplo.
Relatar: prova ou bug
O ESBMC retorna um certificado formal de segurança, ou um traço de contraexemplo concreto que mostra exatamente como o bug é disparado.
Cobertura
Linguagens suportadas
C / C++
Alvo principal; suporte completo a MISRA e AUTOSAR
Python
ESBMC-Python: primeiro BMC baseado em SMT para Python
Rust
Via GOTO Transcoder; executa no CI do projeto verify-rust-std
Solidity
Verificação de contratos inteligentes
CUDA
Correção de kernels de GPU
Kotlin / Java
Via framework Soot
CHERI C
Verificação de plataforma de hardware com segurança de memória (suporte de pesquisa)
Detecção
Classes de erro detectadas
Backends
Suporte a solucionadores SMT
O ESBMC suporta múltiplos solucionadores SMT de nível industrial, permitindo selecionar o melhor backend para cada tarefa de verificação. Essa flexibilidade é fundamental para seu desempenho em grandes bases de código, como demonstrado pelo firmware Intel Core Power Management (190.000 LOC) verificado em menos de 8 horas.
Reconhecimento
Prêmios e reconhecimento
Distinguished Paper Award
ASE'24
Most Influential Paper Award
ASE'23
Mais de 50 prêmios de categoria
SV-COMP e Test-Comp
Distinguished Paper Award
ICSE'11
Veja o ESBMC em ação
Leia como o ESBMC identificou 23 violações de propriedade adicionais no firmware RMM da Arm além daquelas já detectadas pelo CBMC, ou explore nossos outros estudos de caso industriais.