DeepMind prova a segurança do protocolo Signal com IA agêntica

Pesquisadores do Google DeepMind usaram uma estrutura de IA agêntica chamada AlphaProof Code para provar matematicamente várias garantias criptográficas centrais do protocolo Signal, segundo a Wired. O trabalho, uma prova de conceito concluída em quatro semanas, é um exercício de verificação formal: um método que usa matemática para checar se um software se comporta como deveria, em vez de testar uma amostra de casos.

O protocolo Signal é o esquema de criptografia do aplicativo Signal e, como lembra a Wired, também protege as comunicações do Google Messages e do WhatsApp. A análise é apresentada, portanto, como mais uma validação independente de uma criptografia que protege um volume enorme de mensagens. A Wired a descreve como um marco para a criptografia e para a própria IA, mas ressalta que o alcance é limitado.

O que exatamente o DeepMind provou?

A equipe provou “várias” das garantias centrais do protocolo, não todas. A Wired deixa claro que a análise não verificou formalmente todo o aplicativo móvel do Signal, e os pesquisadores descrevem o resultado como um marco em um processo maior. “Estamos muito animados com esse resultado, mas há um longo caminho até conseguirmos escalar isso para todo o software do mundo, e queremos fazer isso”, disse à Wired Swarat Chaudhuri, pesquisador do DeepMind.

Segundo a mesma reportagem, a análise não encontrou nenhuma vulnerabilidade nova nas partes do protocolo examinadas. Os pesquisadores também rodaram o AlphaProof Code em versões antigas do Signal com vulnerabilidades conhecidas e corrigidas há muito tempo: a ferramenta as identificou corretamente e mostrou que essas versões não podiam ser verificadas formalmente. O teste importa porque mostra que o método pode falhar quando há um defeito, e não apenas ter sucesso quando não há.

• Ferramenta: AlphaProof Code, uma nova estrutura de IA agêntica do Google DeepMind.
• Duração: quatro semanas, como projeto de prova de conceito.
• Resultado: garantias criptográficas centrais provadas; nenhuma vulnerabilidade nova nas partes analisadas.
• Versões antigas: falhas conhecidas e já corrigidas detectadas, e protocolo considerado não verificável.
• Publicação: a especificação e a prova estão sendo divulgadas para ajudar outros trabalhos de verificação formal.
• Custo: não divulgado; a análise foi feita gratuitamente, como projeto de pesquisa.

Como a IA e os humanos dividiram o trabalho?

Antes da era da IA, era preciso descrever as propriedades a provar, transformá-las em fórmulas e só então desenvolver a prova. A Wired explica que a IA agêntica pode reduzir bastante o tempo dessa última etapa, o que viabilizou a avaliação do Signal em quatro semanas. Os pesquisadores do DeepMind acrescentam que largaram com vantagem, pois a Signal Foundation já havia feito verificação formal de partes menores do código.

Ehren Kret, diretor de tecnologia do Signal, disse em comunicado citado pela Wired: “Enquanto a verificação formal anterior se concentrava em partes menores do código, a abordagem do Google DeepMind permite uma ampliação significativa”. Ele acrescentou que verificar rigorosamente a implementação aumenta a confiança do Signal nas garantias de privacidade do seu código, à medida que crescem as ameaças de segurança movidas por IA.

O DeepMind aponta como principal avanço um “processo de colaboração humano-IA”: os agentes contribuem e se autocorrigem em quase todas as fases, enquanto humanos revisam nos momentos-chave. “Não queremos um mundo em que a IA gere os objetivos e gere as provas”, disse Chaudhuri. Uma prova formal só garante as propriedades que foram escritas, por isso a revisão humana da especificação continua central.

Um esforço paralelo em torno do Signal

O trabalho do DeepMind não é a única tentativa de provar a criptografia do Signal. A Beneficial AI Foundation, com Rolfe Schmidt, do Signal, e o Lean FRO, lançou o “Signal Shot”, um projeto público para verificar o protocolo e sua implementação em Rust com o assistente de provas Lean. Ele prevê traduzir o código Rust do Signal para Lean com a ferramenta Aeneas e lista componentes a verificar, como a troca de chaves pós-quântica PQXDH, o Double Ratchet e o SPQR/Triple Ratchet. A Wired não liga essa iniciativa à do DeepMind: são dois esforços distintos.

O que ainda é incerto?

A pergunta em aberto, observa a Wired, é se a verificação formal automatizada por IA consegue escalar a um custo viável. O Google se recusou a informar o custo da análise do Signal e a dizer se planeja um produto ou serviço comercial de verificação formal. Pushmeet Kohli, cientista-chefe do Google Cloud e vice-presidente de pesquisa do DeepMind, imagina que bancos e outras empresas preocupadas com bugs poderiam dizer que conseguem provar certas propriedades de seus softwares. É uma visão, não uma oferta anunciada.

O que isso muda para as empresas

Para uma empresa que escolhe uma ferramenta de mensagens ou constrói sobre o protocolo Signal, o resultado é um sinal tranquilizador sobre o desenho do protocolo, não um certificado para cada aplicativo que o usa: o aplicativo Signal completo não foi verificado, e a implantação, os servidores e as configurações de um produto ficam fora da prova. A especificação e a prova publicadas dão às equipes de segurança material para estudar e reutilizar. Como o custo e qualquer oferta comercial são desconhecidos, ainda não convém contar com essa abordagem para verificar formalmente o próprio código, mas já é possível perguntar aos fornecedores de software crítico quais propriedades estão especificadas e provadas.