Mensagens de texto cruzam a tela do celular o dia inteiro sem que ninguém pense na matemática que tranca a conversa. Nesta terça-feira (10), pesquisadores do Google DeepMind (abre em nova aba), o laboratório de inteligência artificial do Google, divulgaram o resultado de um projeto de quatro semanas: uma nova ferramenta de IA provou matematicamente que garantias essenciais de segurança do protocolo Signal (abre em nova aba) funcionam como planejado.
O protocolo Signal não vive apenas dentro do aplicativo de mesmo nome. Esse protocolo é o motor de criptografia (a técnica que embaralha os dados para que só quem envia e quem recebe consigam ler o conteúdo) utilizado também pelo WhatsApp (abre em nova aba) e pelo Google Mensagens. Quando alguém envia um comprovante bancário ou um áudio no grupo da família, é esse protocolo que protege a mensagem no caminho. A análise da DeepMind serve como uma validação independente dessa blindagem e não encontrou nenhuma vulnerabilidade nova nos trechos examinados.
O experimento estreou uma estrutura chamada AlphaProof Code, baseada em IA agêntica (sistemas de inteligência artificial que executam sequências de tarefas com autonomia, gerando e testando etapas sem depender de comandos humanos a cada passo). A equipe aplicou um método conhecido na ciência da computação como verificação formal. Na rotina comum da indústria, programadores procuram falhas rodando testes práticos, como um motorista que pisa no freio e olha os pneus antes de pegar a estrada. A verificação formal exige outra prova: ela traduz o funcionamento do programa em fórmulas matemáticas para atestar, pela lógica pura, que determinadas falhas críticas são impossíveis ali.
Como a IA encurtou anos de cálculo e pegou erros antigos
Especialistas em segurança digital costumam chamar a verificação formal de "santo graal" da proteção de programas, mas o método sempre esbarrou no tempo de execução. Antes da ajuda da IA, pesquisadores humanos precisavam descrever cada regra do código, converter esses resumos em equações e construir a prova matemática linha por linha. O AlphaProof Code acelerou justamente essa última etapa de desenvolvimento da prova.
A velocidade de quatro semanas também teve ajuda do passado. Os cientistas da DeepMind partiram de trabalhos anteriores de verificação formal que a própria Signal Foundation já havia conduzido em pedaços menores do sistema. Em comunicado, o diretor de tecnologia do Signal, Ehren Kret, afirmou que a abordagem da DeepMind permitiu expandir de forma significativa o alcance daquelas análises prévias.
Para confirmar que o AlphaProof Code não estava apenas distribuindo aprovações automáticas, os pesquisadores testaram o sistema no sentido contrário. Eles colocaram a ferramenta para analisar versões antigas do protocolo Signal que continham falhas de segurança já conhecidas (e corrigidas há bastante tempo). A IA identificou os defeitos antigos e demonstrou matematicamente por que aquelas versões não podiam receber o selo de verificação formal. O grupo liberou a especificação e a prova criadas no estudo para que outros cientistas possam reutilizar o material.
O que muda na prática e onde estão os limites
Para quem conversa pelo celular, os aplicativos continuam funcionando do mesmo jeito, e o próprio laboratório avisa que o resultado não significa segurança absoluta. O trabalho foi uma demonstração de pesquisa com alcance limitado. O AlphaProof Code auditou partes centrais do protocolo de criptografia, mas não verificou o aplicativo móvel inteiro do Signal (o que deixaria de fora a interface de tela, o uso da câmera, o salvamento de arquivos e milhares de outras linhas de código, como quem comprova em laboratório que o miolo da fechadura é indestrutível sem vistoriar as janelas da casa).
Swarat Chaudhuri, cientista pesquisador da DeepMind, disse à revista WIRED que a equipe está empolgada com o resultado, mas ressaltou que ainda há uma longa distância até conseguir escalar essa técnica para todos os programas do mundo, objetivo declarado do grupo. O custo e a viabilidade prática de aplicar a verificação formal auxiliada por IA em códigos gigantescos continuam sem resposta definida.
O avanço ocorre no ano em que o Google transformou a segurança digital em um de seus maiores negócios de inteligência artificial: em março de 2026, a empresa concluiu a compra da companhia de segurança em nuvem Wiz por US$ 32 bilhões (a maior aquisição da história do Google) e, em maio, lançou o sistema de proteção AI Threat Defense no Google Cloud (abre em nova aba). Pois é: quatro dias antes de validar a defesa do Signal, em 6 de novembro, outra equipe da mesma DeepMind havia anunciado que agentes de IA guiados por criptógrafos humanos encontraram duas novas fraquezas teóricas no padrão antigo de criptografia RSA de 1024 bits, ainda esquecido em equipamentos velhos. A mesma categoria de modelos matemáticos capaz de provar que um protocolo moderno está trancado avança na mesma velocidade para encontrar brechas onde invasores também procuram entrar.