{"id":183972,"date":"2026-10-23T11:41:12","date_gmt":"2026-10-23T09:41:12","guid":{"rendered":"https:\/\/prohoster.info\/blog\/news\/anthropic-razvivaet-tehniku-dlya-formalnoj-verifikaczii-sushhestvuyushhego-po-pri-pomoshhi-ai"},"modified":"2026-10-23T11:41:16","modified_gmt":"2026-10-23T09:41:16","slug":"anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","status":"publish","type":"post","link":"https:\/\/prohoster.info\/pt\/blog\/news\/anthropic-develops-technique-for-formal-verification-of-existing-software-using-ai","title":{"rendered":"A Anthropic est\u00e1 desenvolvendo t\u00e9cnicas para verifica\u00e7\u00e3o formal de software existente com a ajuda de IA","gt_translate_keys":[{"key":"rendered","format":"text"}]},"content":{"rendered":"
A empresa Anthropic apresentou os resultados de experimentos sobre o uso de modelos de IA para verifica\u00e7\u00e3o formal da confiabilidade e seguran\u00e7a de projetos j\u00e1 existentes. Durante o experimento, foram geradas provas matem\u00e1ticas da aus\u00eancia de erros no gerenciamento de mem\u00f3ria utilizando modelos de IA em 123 bibliotecas abertas, testadas na infraestrutura OSS Fuzz. <\/p>\n
A verifica\u00e7\u00e3o foi realizada no n\u00edvel do c\u00f3digo assembly compilado para a arquitetura RISC-V. O volume total de provas geradas foi de cerca de 180 milh\u00f5es de linhas de c\u00f3digo para o sistema de verifica\u00e7\u00e3o Rocq Prover (aproximadamente 600 mil linhas por arquivo bin\u00e1rio com 18 mil instru\u00e7\u00f5es RISC-V). As provas foram formadas por meio da convers\u00e3o autom\u00e1tica de testes de fuzzing existentes em especifica\u00e7\u00f5es formais, ap\u00f3s o que o modelo de IA Claude provou que, para quaisquer entradas de at\u00e9 64 MB, n\u00e3o ocorriam falhas no programa. <\/p>\n
No processo de constru\u00e7\u00e3o das provas, o modelo de IA conseguiu identificar e preparar corre\u00e7\u00f5es para centenas de erros que anteriormente n\u00e3o foram detectados durante o teste de fuzzing. Entre outros, foram descobertas vulnerabilidades que levam a overflow de buffer ao processar certos dados de entrada (por exemplo, CVE-2026-56132 no libexpat), al\u00e9m de erros l\u00f3gicos. Al\u00e9m disso, o modelo de IA foi utilizado para provar a conformidade da implementa\u00e7\u00e3o do algoritmo zlib no n\u00facleo do Linux com a especifica\u00e7\u00e3o RFC 1950.<\/p>\n
Tamb\u00e9m foi gerador um interpretador em Rust para um subconjunto da linguagem Python, para o qual foi preparada uma prova formal de conformidade com a sem\u00e2ntica do CPython utilizando a ferramenta Verus. Para comparar o comportamento com o CPython, mais de 1,7 milh\u00f5es de programas Python aleatoriamente gerados foram executados. Em 99,95% dos casos, os resultados da execu\u00e7\u00e3o desses programas na nova implementa\u00e7\u00e3o e no CPython coincidiram, e as diverg\u00eancias identificadas se mostraram casos extremos conhecidos.<\/p>\n
A verifica\u00e7\u00e3o formal realizada garante conformidade com a especifica\u00e7\u00e3o, mas n\u00e3o elimina completamente a possibilidade de problemas de seguran\u00e7a, uma vez que n\u00e3o ficam formalizados os riscos causados por problemas de multithreading, vincula\u00e7\u00e3o din\u00e2mica e comportamento an\u00f4malo do hardware real. A principal vantagem da abordagem proposta \u00e9 o trabalho diretamente com arquivos bin\u00e1rios, o que permite evitar a necessidade de reescrever o c\u00f3digo existente em linguagens formalmente verific\u00e1veis. \n Fonte: opennet.ru<\/a> <\/p>","protected":false,"gt_translate_keys":[{"key":"rendered","format":"html"}]},"excerpt":{"rendered":"