Google usa IA para verificar matematicamente a segurança do código do Signal

O Google DeepMind usou um sistema de demonstração matemática para confirmar propriedades de segurança no código do mensageiro Signal. O trabalho, revelado em 10 de novembro de 2026, aponta um caminho diferente de testar software: provar, e não só testar.

O que o Google DeepMind fez com o código do Signal

O Google utilizou inteligência artificial para analisar e verificar propriedades de segurança do Signal, aplicativo de mensagens conhecido pela criptografia de ponta a ponta. O trabalho foi conduzido pelo Google DeepMind, divisão de pesquisa em IA da empresa, e divulgado em 10 de novembro de 2026 pelo Olhar Digital.

A ferramenta usada se chama AlphaProof Code, um sistema construído para trabalhar com demonstrações formais, o processo de provar matematicamente que um pedaço de código se comporta como deveria. Durante cerca de quatro semanas, ela examinou partes do código do Signal e ajudou pesquisadores humanos a confirmar se certas propriedades de segurança eram válidas sob premissas específicas.

Não se trata de um scanner de vulnerabilidades como os que times de segurança já usam no dia a dia. É um exercício de prova matemática aplicado a um software real, algo que até pouco tempo exigia meses de trabalho manual de especialistas em métodos formais.

A diferença entre testar código e provar código

Quem desenvolve está acostumado a validar segurança por teste: escrever casos de uso, rodar fuzzing, simular ataques, revisar pull request por pull request. Esse processo encontra muitos problemas, mas nunca garante que não sobrou nenhum: ele prova que o código falhou nos casos testados, não que vai funcionar em todos os casos possíveis.

A verificação formal segue outra lógica. Uma propriedade de segurança (por exemplo, "esta função nunca vaza a chave privada mesmo com entrada maliciosa") é escrita como uma afirmação matemática. Um verificador então confere se existe uma demonstração logicamente válida de que essa afirmação é sempre verdadeira, dadas certas premissas.

O trabalho do Google usou a linguagem Lean para isso, um ambiente de demonstração de teoremas que já era usado por matemáticos antes de chegar à verificação de software. É o mesmo tipo de infraestrutura por trás do AlphaProof, sistema anterior do DeepMind voltado para resolver problemas matemáticos complexos. Aplicar essa base a código de produção, como o do Signal, é um passo diferente: sair da matemática pura para instruções que rodam em servidores e celulares de verdade.

Um teste com bugs antigos escondidos de propósito

Para avaliar se o sistema funcionava de fato, os pesquisadores fizeram algo que qualquer time de QA reconhece: inseriram de volta vulnerabilidades antigas e já conhecidas em versões do código do Signal, de propósito. A pergunta era simples: a ferramenta consegue perceber que a propriedade de segurança deixou de valer quando o bug volta?

Segundo o relato da fonte, esse foi um dos critérios usados para avaliar a confiabilidade do processo, e não apenas confirmar que o código atual passa, mas que o sistema reage quando o código piora. É um teste de sanidade que faz sentido técnico: uma ferramenta de verificação só é útil se ela sabe dizer não quando a resposta é não.

O que muda para quem constrói ferramentas de segurança

Verificação formal não é novidade em si: diversos projetos de software crítico, de sistemas operacionais a bibliotecas criptográficas, já passaram por provas formais ao longo dos anos, usando linguagens e ferramentas especializadas nesse tipo de demonstração. O que muda aqui é o uso de um sistema de IA treinado para ajudar a montar essas provas, reduzindo o trabalho manual de especialistas que hoje é o principal gargalo da área.

Para quem desenvolve ou avalia software de segurança no Brasil, isso aponta algumas direções práticas:

• Onde já dá para aplicar hoje: componentes pequenos e bem isolados, como uma função de criptografia ou um protocolo de troca de chaves, são os candidatos mais realistas para verificação formal assistida por IA, não o aplicativo inteiro.
• O que fica mais barato: o gargalo histórico da verificação formal é o tempo de especialista humano escrevendo a prova linha por linha. Uma IA que ajuda a montar parte dessa demonstração pode encurtar ciclos que hoje levam meses.
• O que ainda exige julgamento humano: decidir QUAL propriedade vale a pena provar e sob quais premissas continua sendo trabalho de quem entende o sistema, a IA ajuda na demonstração, não na escolha do que demonstrar.

Os limites: o que a verificação formal não cobre

O próprio material da fonte faz questão de deixar isso claro: verificar matematicamente uma propriedade específica do código não significa que o aplicativo inteiro está livre de vulnerabilidades. Falhas de implementação em partes não cobertas pela prova, bugs na interface, ou ataques que comprometem o próprio dispositivo do usuário continuam sendo riscos reais e fora do escopo desse tipo de verificação.

Isso importa para quem avalia relatórios de segurança desse tipo: uma prova formal cobre exatamente a propriedade que foi declarada, nada além dela. Um sistema pode ter uma função matematicamente comprovada como segura e, ainda assim, sofrer um ataque por um canal completamente diferente, como engenharia social ou um bug numa dependência de terceiros que nunca entrou na análise.

O Signal não divulgou publicamente, pelo que consta na reportagem original, se vai adotar esse processo de forma recorrente ou se foi um experimento pontual do Google DeepMind. Fica em aberto também se o AlphaProof Code vai ganhar alguma forma de acesso para outros projetos de código aberto auditarem seus próprios componentes críticos da mesma maneira.

Fonte: Olhar Digital — IA