Signal: o que a IA provou realmente sobre o seu código

A Google DeepMind afirma ter utilizado o AlphaProof Code para provar certas propriedades do código compilado da libsignal. O resultado esclarece o potencial da IA, mas também os limites precisos de uma prova formal.

Para avaliar se um software encripta corretamente as mensagens, não basta executar testes e observar o seu comportamento em algumas situações. É também necessário poder demonstrar, através de um raciocínio verificável, que certas propriedades se mantêm em todas as execuções abrangidas pelo modelo. A Google DeepMind afirma ter utilizado o seu sistema AlphaProof Code para realizar este trabalho sobre código compilado do protocolo Signal, com agentes de IA e o verificador de provas Lean.

A experiência incide sobre garantias criptográficas específicas, não sobre a segurança absoluta da aplicação Signal. Mostra sobretudo como a IA pode participar numa verificação formal exigente, deixando escolhas importantes a cargo dos investigadores e confiando o controlo matemático final a um software especializado.

Do modelo criptográfico ao código executado

Um protocolo de encriptação descreve as regras que permitem, por exemplo, proteger uma comunicação e autenticar os interlocutores. Mas uma conceção correta não é suficiente: o programa que a implementa pode conter um erro. A verificação formal procura demonstrar matematicamente que o código respeita propriedades definidas previamente, sob hipóteses também elas explícitas.

A DeepMind indica que trabalhou sobre código compilado da libsignal, a biblioteca que implementa o protocolo Signal. Esta etapa é importante: a equipa não se ficou por uma descrição teórica do protocolo, mas procurou relacionar garantias de segurança com o código produzido após a compilação.

O sistema, baptizado AlphaProof Code, distribui o trabalho por vários modelos e agentes. Segundo a descrição publicada pela Google DeepMind, os investigadores começaram por traduzir os objetivos de segurança em especificações matemáticas e, depois, agentes alimentados pelo Gemini construíram provas formais. A publicação da DeepMind menciona mais de seis milhões de linhas produzidas na linguagem Lean. Este volume não significa que a IA tenha escrito seis milhões de linhas de software: trata-se dos artefactos utilizados para formalizar e verificar as demonstrações.

O que o Lean verifica e o que os investigadores decidem

O Lean é um assistente de provas. Verifica se uma demonstração respeita as regras lógicas do sistema e estabelece efetivamente o resultado formulado. Por si só, não decide se as propriedades escolhidas correspondem a todas as expectativas de um utilizador, nem se as hipóteses de partida descrevem corretamente o mundo real.

Esta distinção é fundamental. Segundo a DeepMind, os especialistas participaram na definição do que deveria ser provado e reviram as especificações. Os agentes exploraram depois possíveis vias de demonstração, enquanto o Lean verificava a sua validade formal. Assim, o sistema pode reduzir parte do trabalho de investigação necessário para encontrar uma prova, mas o âmbito da prova continua a ser uma escolha humana.

Uma demonstração formal não é, portanto, uma auditoria universal. Se uma propriedade não estiver incluída nas especificações, a prova não a abrange. Se se considerar segura uma função criptográfica sem verificar a sua implementação, essa hipótese continua a ser um elo exterior ao resultado. A conclusão correta é condicional: o código satisfaz as propriedades formalizadas, no quadro definido e sob as hipóteses adotadas.

Quatro semanas, dois erros reintroduzidos

A DeepMind anuncia que a experiência durou quatro semanas. Para testar se o método conseguia distinguir código conforme de uma versão defeituosa, a equipa também reintroduziu dois erros conhecidos, anteriormente corrigidos, numa versão isolada do código. Segundo a empresa, o sistema produziu então provas verificadas por máquina que demonstravam que essas variantes já não respeitavam as garantias analisadas.

Este teste é útil porque confronta o método com erros concretos, em vez de medir apenas a sua capacidade de produzir uma demonstração sobre uma versão correta. Mas não constitui uma taxa de deteção generalizável: dois defeitos reintroduzidos não representam todas as categorias de vulnerabilidades, todos os softwares, nem todas as formas como um sistema poderia falhar.

Os limites da prova continuam bem definidos

As garantias analisadas dizem respeito ao núcleo criptográfico e a comunicações individuais. O âmbito descrito deixa de fora a aplicação no seu conjunto, as conversas de grupo e a utilização em vários dispositivos. Também não constituem uma verificação do WhatsApp ou do Google Messages, embora estes serviços utilizem elementos do protocolo Signal. Uma biblioteca ou um protocolo partilhado não torna idênticas as aplicações que os integram, as respetivas versões ou configurações.

A verificação também não significa que não subsistam vulnerabilidades desconhecidas. Reduz a incerteza quanto a propriedades definidas e ao código incluído na análise. Outros componentes, as interfaces, os sistemas operativos, a gestão de chaves ou as funções deixadas fora do âmbito podem levantar questões distintas.

Para os utilizadores, o interesse imediato não é, portanto, tanto uma nova definição como um método de controlo capaz de tornar certas garantias mais difíceis de contestar ou de infringir inadvertidamente. Para as equipas que concebem software crítico, a questão é saber se os agentes podem reduzir o custo humano de provas que até agora exigiam um trabalho especializado significativo. A DeepMind aponta possíveis aplicações a outros softwares, mas a capacidade de alargar esta abordagem a sistemas de maior dimensão ainda está por demonstrar.

As especificações e provas publicadas pela DeepMind permitem que outros especialistas analisem e reproduzam o trabalho. É esta possibilidade de controlo, associada a um âmbito claramente definido, que permite avaliar o contributo da IA: não uma certificação geral de «segurança», mas uma ajuda para estabelecer certas propriedades do código, com humanos a escolher o que importa e um verificador formal a controlar a demonstração.