Serviço
Reparo de Bugs Assistido por IA
Modelos de linguagem de grande porte aceleram o desenvolvimento, mas introduzem dívida de segurança em escala. O ESBMC-AI atua como uma rede de segurança formal, revelando o que o LLM deixou passar e propondo patches candidatos para revisão por engenheiros.
O desafio
A IA gera código. O ESBMC o verifica.
Equipes de desenvolvimento que usam LLMs para gerar código entregam mais rápido, mas herdam as vulnerabilidades de segurança que os LLMs rotineiramente introduzem: vazamentos de memória, estouros de inteiro, desreferências de ponteiro nulo e comportamento indefinido. Em escala, isso cria uma dívida de segurança que os testes sozinhos não conseguem revelar.
O ESBMC-AI foi desenvolvido como parte do projeto NW CyberCom de £1.2M conduzido pela Lancaster University. Ele combina o motor de verificação formal do ESBMC com reparo guiado por IA para fechar o ciclo: detectar, corrigir e reverificar, automaticamente.
Fluxo de trabalho do ESBMC-AI
Capacidades
O que o ESBMC-AI entrega
Detecção de bugs
O ESBMC-AI ajuda a identificar erros de memória, estouros e comportamento indefinido tanto em código escrito por humanos quanto gerado por LLMs, usando a análise baseada em SMT subjacente do ESBMC.
Geração de patch candidato
Para cada violação identificada, o sistema propõe um patch candidato e o reverifica contra a propriedade de segurança original; os patches são apresentados aos seus engenheiros para revisão, não aplicados silenciosamente.
Integração com VSCode
Os desenvolvedores podem receber feedback inline do ESBMC-AI no editor como parte de seu fluxo normal de revisão.
Integração com CI do GitHub / GitLab
A verificação é executada como parte das checagens de pull request; propriedades que falham aparecem como comentários acionáveis no PR.
Verificação de regressão
Depois que um patch candidato é aceito, o ESBMC reverifica o código afetado para revelar regressões antes do merge.
Robustecimento de código gerado por IA
Uma rede de segurança de métodos formais para equipes que adotam LLMs em seu fluxo de desenvolvimento, o verificador que o próprio LLM não consegue executar.
Procedência da pesquisa
Construído sobre uma base de pesquisa publicada
O ESBMC-AI foi desenvolvido por nosso grupo de pesquisa como parte do projeto de £1.2M NW CyberCom do Connecting Capability Fund (Research England, conduzido pela Lancaster University com universidades parceiras, incluindo Manchester). A técnica subjacente está documentada em Tihanyi, Charalambous, Jain, Ferrag e Cordeiro, "A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification" (arXiv 2305.14752), e em trabalhos subsequentes do mesmo grupo.
O ESBMC-AI é uma ferramenta de nível de pesquisa cujos achados e patches propostos destinam-se à revisão por engenheiros; não é um sistema de remediação autônoma plug-and-play.
Preço
Retainer ou por projeto
Integramos o ESBMC-AI ao seu pipeline e fornecemos suporte contínuo de verificação. Entre em contato para conversar sobre sua configuração de CI/CD e o tamanho da sua equipe.