IA da DeepMind prova que o código de encriptação do Signal cumpre as suas garantias

A Google DeepMind afirma que os seus agentes de IA provaram matematicamente que o código de encriptação do Signal para conversas individuais cumpre as suas principais promessas de segurança. O trabalho, apresentado a 10 de novembro, usou um novo sistema chamado AlphaProof Code e verificou o próprio programa compilado, ou seja, o código que é realmente executado. Segundo a DeepMind, é a primeira vez que a implementação de um protocolo criptográfico tão difundido é verificada formalmente por qualquer método, com ou sem IA. Não foram encontradas novas falhas nas partes analisadas.

O que foi provado

A verificação formal consiste em escrever uma propriedade de segurança como um enunciado matemático e provar que o programa a cumpre sempre, em vez de o testar com exemplos. A maior parte das análises de protocolos como o Signal fica pelo desenho. A DeepMind desceu até ao código máquina: a equipa pegou na libsignal na versão 0.105.4 e na biblioteca spqr, compilou-as para Linux em ARM de 64 bits com o compilador Rust padrão e raciocinou sobre o executável resultante, segundo a descrição técnica.

Primeiro, os investigadores, com vários modelos de IA, traduziram os objetivos de segurança do Signal em especificações formais, e uma pessoa reviu cada uma. Depois, agentes baseados no Gemini Carbon escreveram as provas em Lean, uma linguagem cujo verificador confirma cada passo automaticamente. O resultado são cerca de 6,5 milhões de linhas. Os agentes assinalaram perto de 1% para revisão humana, e o projeto inteiro levou quatro semanas. Entre os dez teoremas provados estão o sigilo futuro, que protege mensagens antigas se uma chave vazar mais tarde, e a segurança pós-comprometimento, que repõe a proteção depois de um dispositivo ter sido temporariamente invadido.

Para confirmar que o sistema distingue código correto de código com erros, a equipa voltou a introduzir dois erros reais do Signal, corrigidos há muito, numa cópia isolada do código. Em ambos os casos, o AlphaProof Code produziu uma prova verificada por máquina de que a versão com o erro era insegura.

O que ficou fora da prova

A descrição enumera os limites em detalhe. As aplicações móveis não foram verificadas diretamente, e os autores apenas esperam que os resultados se apliquem se as aplicações executarem o código do protocolo sem alterações. As conversas de grupo ficam para trabalho futuro. Os canais laterais, como fugas pelo tempo de execução ou pelo consumo de energia, ficaram de fora, tal como a geração de chaves e o uso em vários dispositivos. As provas assumem ainda que os blocos criptográficos de base são sólidos. O diretor de tecnologia do Signal, Ehren Kret, disse que o trabalho «dá ainda mais confiança» nas garantias de privacidade do código.

O blog da DeepMind refere o Signal e o Google Messages entre as aplicações que usam este protocolo. O WhatsApp adotou o protocolo Signal há anos, mas a prova incidiu sobre o código libsignal do Signal e não sobre o software do WhatsApp, por isso não diz nada de novo sobre o WhatsApp. O trabalho apoiou-se em parte numa verificação formal anterior do Signal feita sem IA. O método é também caro: a Google disse à Wired que exige muita computação, e o investigador Swarat Chaudhuri afirmou que há «um longo caminho a percorrer» até se poder aplicá-lo a todo o software do mundo, relata o 9to5Mac. A DeepMind publicou as provas no GitHub para que especialistas externos as possam verificar.