Encriptação do Signal passa numa prova de 6,5 milhões de linhas feita por IA

O código de encriptação da Signal tem agora algo que quase nenhum software de utilização generalizada pode reivindicar: uma prova matemática de que faz aquilo que promete. Uma equipa de agentes de IA analisou a libsignal, a biblioteca que executa o protocolo Signal, e provou que as conversas individuais se mantêm secretas, confirmam a identidade da pessoa do outro lado e voltam a impedir o acesso de um atacante depois de uma chave ser roubada. Não foram encontradas novas falhas.

Isto é importante muito para além dos utilizadores da Signal. O protocolo é a norma mundial para mensagens com encriptação ponto a ponto, e variantes suas protegem as conversas no WhatsApp, no Messenger e no Google Messages. Verificar código real, já distribuído, com este nível de profundidade era tão lento que quase ninguém se aventurava: um dos maiores êxitos da área, um núcleo de sistema operativo formalmente verificado, exigiu vinte anos de trabalho de uma pessoa. Este trabalho demorou quatro semanas.

A ferramenta, desenvolvida pela Google DeepMind, chama-se AlphaProof Code. Primeiro, especialistas humanos e modelos de IA converteram os objetivos de segurança da Signal em enunciados formais em Lean, uma linguagem de programação criada para demonstrações matemáticas, e uma pessoa reviu cada um deles. Depois, equipas de 40 a 80 agentes, alimentadas pelo Gemini Carbon, escreveram as demonstrações, trabalhando durante períodos de 24 a 72 horas numa única máquina. O resultado são cerca de 6,5 milhões de linhas de Lean.

Não é preciso confiar nessas milhões de linhas. O núcleo do Lean verifica cada passo e rejeita qualquer demonstração que não seja válida, pelo que é indiferente qual foi o modelo que a escreveu ou quantas vezes errou pelo caminho. Aquilo em que as pessoas têm, de facto, de confiar é muito mais reduzido: cerca de 26 000 linhas de especificações e um modelo do modo como um processador ARM executa código.

As demonstrações abrangem as partes da Signal que protegem uma conversa: o handshake PQXDH, que estabelece a conversa, e o Triple Ratchet, que altera a chave em cada mensagem, incluindo a camada pós-quântica concebida para resistir aos futuros computadores quânticos. Na prática, isto significa que roubar as chaves atuais de um telemóvel não permite aceder a mensagens antigas, e que o ladrão volta a perder o acesso assim que os dois lados trocam chaves novas.

Para mostrar que o sistema consegue distinguir código correto de código defeituoso, os investigadores reintroduziram dois erros antigos da libsignal, já corrigidos. Um deles fazia com que a biblioteca guardasse uma cópia de uma chave secreta que devia ter eliminado. Nos dois casos, o AlphaProof Code produziu uma demonstração, verificada por máquina, de que a versão com o erro era insegura.

Há limites concretos. A demonstração abrange apenas sessões individuais, e a DeepMind aponta as mensagens de grupo como trabalho futuro. Aplica-se à versão 0.105.4 da libsignal, compilada com o compilador Rust padrão para ARM Linux no âmbito de um pequeno programa de teste, e não às aplicações completas da Signal para iPhone, Android ou computador. Parte-se do princípio de que os componentes criptográficos de baixo nível são seguros; isso não foi provado. Um erro nas especificações aprovadas por humanos enfraqueceria a garantia, e o WhatsApp e as outras aplicações usam as suas próprias versões do protocolo, pelo que o resultado não se aplica automaticamente a essas plataformas. A Google também não quis dizer à Wired quanto custou a análise nem se tenciona vendê-la como serviço.

A Signal recebeu o resultado com satisfação. «À medida que aumentam as ameaças à segurança impulsionadas pela IA, verificar rigorosamente a implementação do protocolo Signal dá-nos ainda mais confiança nas garantias de privacidade do nosso código», afirmou Ehren Kret, diretor de tecnologia da Signal, num comunicado. Swarat Chaudhuri, investigador da DeepMind, mostrou-se mais cauteloso e disse à Wired que «ainda há um longo caminho a percorrer» até que o método possa ser aplicado «a todo o software do mundo».

Para quem usa a Signal, não há nada para instalar nem qualquer definição a alterar. A prova diz respeito a código que já está na aplicação.

A DeepMind publicou o trabalho a 10 de novembro, juntamente com um artigo técnico, e disponibilizou em código aberto as especificações e as demonstrações no GitHub. Apresenta o projeto da Signal como um marco no caminho para um grande desafio de verificação formal lançado em abril, e aponta o firmware de dispositivos médicos e o software das redes elétricas como exemplos de sistemas que pretende verificar a seguir.

Chaudhuri também traçou um limite para a quantidade de trabalho que deve ser entregue às máquinas. «Não queremos este tipo de mundo de vibes em que a IA gera os objetivos e a IA gera as demonstrações», disse à Wired. Cabe aos humanos continuar a decidir o que é seguro; à IA, apenas prová-lo.

Etiquetas: cibersegurança, Google DeepMind, AlphaProof Code, encriptação ponta a ponta, libsignal, Signal