Criptografia do Signal passa em prova de 6,5 milhões de linhas feita por IA

O código de criptografia do Signal agora tem algo que quase nenhum software amplamente usado pode reivindicar: uma prova matemática de que faz o que promete. Uma equipe de agentes de IA analisou o libsignal, a biblioteca que implementa o protocolo do Signal, e provou que as conversas individuais permanecem secretas, confirmam quem está do outro lado e voltam a impedir o acesso de um invasor depois que uma chave é roubada. Nenhuma nova falha foi encontrada.

Isso importa muito além dos próprios usuários do Signal. O protocolo é o padrão global para mensagens com criptografia de ponta a ponta, e variantes dele protegem conversas no WhatsApp, no Messenger e no Google Messages. Verificar código real, já lançado, com esse nível de profundidade costumava ser tão demorado que quase ninguém tentava: um dos maiores feitos da área, a verificação de um kernel de sistema operacional, levou vinte anos de trabalho de uma pessoa. Esse trabalho levou quatro semanas.

A ferramenta, desenvolvida pelo Google DeepMind, chama-se AlphaProof Code. Primeiro, especialistas humanos e modelos de IA transformaram os objetivos de segurança do Signal em enunciados formais na linguagem Lean, criada para provas matemáticas, e uma pessoa revisou cada um deles. Em seguida, equipes de 40 a 80 agentes, impulsionadas pelo Gemini Carbon, escreveram as provas, trabalhando de 24 a 72 horas seguidas em uma única máquina. O resultado tem cerca de 6,5 milhões de linhas de Lean.

Ninguém precisa confiar nessas milhões de linhas. O núcleo do Lean verifica cada etapa e rejeita qualquer prova que não se sustente; por isso, não faz diferença qual modelo a escreveu nem quantas vezes ele errou pelo caminho. O que as pessoas precisam de fato aceitar é bem menor: cerca de 26 mil linhas de especificações e um modelo de como um processador ARM executa código.

As provas abrangem as partes do Signal que protegem uma conversa: o handshake PQXDH, que inicia uma conversa, e o Triple Ratchet, que troca a chave a cada mensagem, incluindo a camada pós-quântica, projetada para resistir a futuros computadores quânticos. Na prática, isso significa que roubar as chaves atuais de um celular não permite acessar mensagens antigas, e o ladrão perde o acesso novamente assim que os dois lados trocam novas chaves.

Para mostrar que o sistema consegue distinguir código correto de código defeituoso, os pesquisadores reintroduziram dois bugs antigos do libsignal, já corrigidos. Um deles fazia a biblioteca manter uma cópia de uma chave secreta que deveria ter descartado. Nos dois casos, o AlphaProof Code produziu uma prova verificada por máquina de que a versão com o bug era insegura.

Há limites concretos. A prova abrange apenas sessões individuais, e o DeepMind aponta as mensagens em grupo como um trabalho futuro. Ela se aplica à versão 0.105.4 do libsignal, compilada com o compilador padrão de Rust para ARM Linux dentro de um pequeno programa de teste, e não aos aplicativos completos do Signal para iPhone, Android ou computador. Pressupõe-se que os componentes criptográficos de baixo nível sejam seguros; eles não foram provados. Um erro nas especificações aprovadas por humanos enfraqueceria a garantia, e o WhatsApp e os outros aplicativos usam suas próprias versões do protocolo, então o resultado não se aplica automaticamente a eles. O Google também se recusou a dizer à Wired quanto custou a análise ou se pretende oferecê-la como serviço.

O Signal comemorou o resultado. “À medida que as ameaças à segurança impulsionadas por IA aumentam, verificar rigorosamente a implementação do protocolo do Signal nos dá ainda mais confiança nas garantias de privacidade do nosso código”, disse em comunicado Ehren Kret, diretor de tecnologia do Signal. Swarat Chaudhuri, pesquisador do DeepMind, foi mais cauteloso e disse à Wired que ainda há “um longo caminho a percorrer” antes que o método possa ser ampliado “para todo o software do mundo”.

Para quem usa o Signal, não há nada para instalar nem nenhuma configuração a alterar. A prova diz respeito ao código que já está no aplicativo.

O DeepMind publicou o trabalho em 10 de novembro, junto com um artigo técnico, e disponibilizou as especificações e provas como código aberto no GitHub. A empresa descreve o projeto do Signal como um marco em direção a um grande desafio de verificação formal lançado em abril e cita o firmware de dispositivos médicos e os softwares de redes elétricas como exemplos de sistemas que pretende verificar em seguida.

Chaudhuri também estabeleceu um limite para a parcela do trabalho que deve caber às máquinas. “Não queremos esse tipo de mundo, nessa vibe, em que a IA gera os objetivos e também gera as provas”, disse à Wired. Os humanos continuam decidindo o que é considerado seguro; a IA apenas prova isso.

Tags: cibersegurança, Google DeepMind, AlphaProof Code, criptografia de ponta a ponta, libsignal, Signal