Google DeepMind diz que IA verificou partes-chave do protocolo Signal
🎧 Ouça esta notícia
Pesquisadores da Google DeepMind dizem ter usado agentes de IA e o AlphaProof Code para verificar formalmente garantias criptográficas importantes da implementação do protocolo Signal. O protocolo protege conversas no Signal e no Google Messages e sustenta a criptografia do WhatsApp. Segundo o Xataka, os agentes geraram mais de seis milhões de linhas em Lean, enquanto especialistas humanos revisaram as especificações e cerca de 1% do código sinalizado para nova análise; o trabalho levou quatro semanas.
A análise não encontrou novas vulnerabilidades nas partes examinadas. Quando a equipe reinseriu duas falhas reais já corrigidas em uma versão isolada do código, o sistema identificou que as versões vulneráveis não eram seguras, segundo a Google DeepMind. O projeto não verificou todo o aplicativo móvel do Signal, e a viabilidade de ampliar a abordagem e fazê-lo a um custo prático continua em aberto. A Signal Foundation já havia realizado trabalhos anteriores de verificação em partes menores do código, de acordo com o Wired e o Xataka.
Por que importa · interpretação editorial
O trabalho sugere que agentes de IA podem ampliar a verificação formal de software criptográfico, mas a revisão humana continuou necessária e a viabilidade de escalar o método a um custo prático ainda é uma questão em aberto. Como a análise cobriu apenas partes do código, ela não equivale à verificação completa do aplicativo Signal.
Fontes
PesquisaSegurançaCódigo