Serviço
Auditoria de Segurança de Código
Aplicamos bounded model checking formal ao seu código e retornamos, dentro dos limites de verificação especificados, ou uma prova formal de que uma classe de bugs não ocorre ou um contraexemplo concreto mostrando exatamente como um deles pode ser disparado.
O problema com a análise estática
Avisos heurísticos não são prova
Ferramentas de análise estática geram avisos com base em heurísticas. Elas são rápidas, mas produzem falsos positivos, deixam passar bugs sutis e não dão garantia de que uma classe de erro está ausente. Engenheiros gastam horas triando avisos que se revelam inofensivos, e deixam passar os que importam.
Em nossa colaboração publicada com a Arm (SAS 2024), o ESBMC identificou 23 violações de propriedade
adicionais no Realm Management Monitor, além daquelas que o CBMC já havia detectado
no próprio CI do projeto. Em nossa colaboração publicada com a Ethereum (ISSTA 2024), nossa
ferramenta ESBMC-Python identificou uma divisão por zero no
integer_squareroot
helper da especificação de consenso, com a correção incorporada upstream como
ethereum/consensus-specs PR #3600.
Nossa abordagem
Toda violação confirmada é reproduzível
O ESBMC codifica seu programa como restrições SMT e as entrega a um solver industrial. Toda violação confirmada vem com um contraexemplo concreto, um traço preciso de execução que reproduz o bug, tornando-o trivialmente reproduzível por seus engenheiros.
Quando o ESBMC não encontra nenhum contraexemplo dentro dos limites de verificação especificados, ele fornece uma prova formal para aquele limite, não uma heurística do tipo "nenhum aviso encontrado hoje", mas uma afirmação matemática sobre o comportamento do programa para o espaço de execução limitado.
Cobertura
Classes de bugs que auditamos
Processo
Como funciona uma auditoria
Definição de escopo
Acordamos o código, as linguagens, as propriedades de segurança e os limites de verificação.
Análise com ESBMC
Executamos o ESBMC com configurações otimizadas para seu código e para as classes de erro de interesse.
Relatório de achados
Cada achado é ordenado por severidade e acompanhado de um traço concreto de contraexemplo.
Orientação de correção
Explicamos a causa raiz e recomendamos uma correção. Podemos reverificar após as mudanças sem custo adicional.
Preço
Preço fixo, escopado por KLOC
Acordamos escopo e um preço fixo antes de começar. Sem surpresas por hora. Entre em contato com o tamanho e a linguagem do seu código para receber um orçamento.