DeepMind verificou parte da criptografia do Signal com IA em um mês

Os testes passam, a revisão não encontra problemas, mas ainda assim falta confiança no código crítico. Para a criptografia, isso é especialmente incômodo: uma combinação rara de condições pode pesar mais do que mil execuções bem-sucedidas. Segundo a ZDNET, o Google DeepMind aplicou o AlphaProof Code a parte do código criptográfico do Signal e concluiu a verificação em um mês. O interesse prático está na tentativa de reduzir o trabalho manual de construção de provas matemáticas.

Vale deixar claro o limite do resultado: a publicação não indica que os pesquisadores provaram a segurança de todo o mensageiro. Trata-se de partes específicas da implementação e de propriedades que a equipe decidiu verificar. Para o desenvolvedor, a diferença é fundamental: a prova responde a uma pergunta concreta sobre o programa, e não emite um certificado universal de confiabilidade.

O que se verifica matematicamente

Imagine uma função que atualiza o estado criptográfico depois do processamento de uma mensagem. Um teste comum passa a ela dados escolhidos e compara o resultado com o esperado. É possível adicionar entradas aleatórias, valores-limite e longas sequências de chamadas. Mesmo assim, cada execução verifica um cenário específico.

Na verificação formal, primeiro se escreve o requisito exato para o comportamento da função. Depois, prova-se que o código o cumpre em todos os casos abrangidos pelo modelo definido. Um exemplo hipotético: a operação deve preservar determinada relação entre o estado antigo e o novo. É uma ilustração do método, não a descrição de uma propriedade específica provada pela equipe da DeepMind.

A parte mais cara desse trabalho muitas vezes começa antes da prova. É preciso decidir o que exatamente o programa promete, quais premissas são aceitáveis e onde termina o trecho verificado. Se o requisito for formulado de forma incorreta ou incompleta, mesmo uma prova correta não responderá à pergunta real sobre a segurança do produto.

Como o trabalho foi dividido entre humanos e agentes

Segundo a ZDNET, os pesquisadores se basearam em trabalhos anteriores da Signal Foundation. Humanos, junto com os agentes, definiram quais afirmações seriam provadas. Em seguida, vários agentes construíram as provas; separadamente, o sistema ajudou a verificar o resultado e destacou trechos que exigiam atenção humana.

O veículo informa que cerca de 1% da base de código foi marcado para nova verificação manual. Esse número deve ser lido com cautela: o texto não deixa claro como o denominador foi definido nem o que foi considerado um trecho verificado. Isso não significa que a IA tenha confirmado, por conta própria, a segurança dos outros 99% de todo o aplicativo Signal.

Outro resultado informado é o trabalho com dois erros do Signal corrigidos anteriormente. Esse tipo de teste é útil: a ferramenta precisa distinguir uma implementação correta de uma com defeito. No entanto, um resumo curto não basta para reconstruir o experimento, entender suas condições e avaliar quais classes de erros o sistema realmente consegue detectar.

O prazo de um mês também exige contexto. A ZDNET o compara a um trabalho que poderia levar anos para especialistas, mas não apresenta um projeto comparável, o custo computacional nem um registro detalhado do trabalho humano. Por isso, ainda é cedo para prometer às equipes a mesma aceleração.

O que fazer como desenvolvedor e product manager

Se a abordagem se confirmar com os materiais disponíveis, ela será especialmente interessante para módulos pequenos, em que um erro custa caro e os requisitos podem ser formulados com precisão. Dá para começar com uma única função, descrevendo suas entradas válidas, as propriedades esperadas e as dependências. Depois disso, ficará mais claro se há aqui uma tarefa para verificação formal e que resultado a equipe poderá aceitar.

Para o product manager, é útil definir antecipadamente os limites da promessa ao usuário. Uma propriedade comprovada de um módulo criptográfico não diz automaticamente nada sobre a proteção do dispositivo, a interface, os backups ou a correção das atualizações. Essas questões exigem verificações próprias.

Segundo a publicação, a DeepMind planeja abrir o código do AlphaProof Code. Para avaliar a adequação da ferramenta, serão necessários o próprio repositório, as especificações, as provas verificáveis e a descrição das limitações. Por ora, é um exemplo relevante da aplicação de IA a uma tarefa de engenharia: os agentes podem ajudar a preparar provas, mas a qualidade dos requisitos e os limites do resultado continuam sendo responsabilidade das pessoas.