DeepMind valida o protocolo Signal com inteligência artificial

Investigadores da Google DeepMind usaram uma plataforma 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 a matemática para confirmar que um software se comporta como previsto, em vez de testar uma amostra de casos.

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

O que provou, afinal, a DeepMind?

A equipa provou “várias” das garantias centrais do protocolo, não todas. A Wired esclarece que a análise não verificou formalmente toda a aplicação móvel do Signal, e os investigadores descrevem o resultado como um marco num processo mais vasto. “Estamos muito entusiasmados com este resultado, mas há um longo caminho até conseguirmos escalar isto para todo o software do mundo, e queremos fazê-lo”, disse à Wired Swarat Chaudhuri, investigador da DeepMind.

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

• Ferramenta: AlphaProof Code, uma nova plataforma de IA agêntica da 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 detetadas, e protocolo considerado não verificável.
• Publicação: a especificação e a prova estão a ser divulgadas para ajudar outros trabalhos de verificação formal.
• Custo: não divulgado; a análise foi feita gratuitamente, como projeto de investigação.

Como dividiram a IA e os humanos o trabalho?

Antes da era da IA, era preciso descrever as propriedades a provar, convertê-las em fórmulas e só depois desenvolver a prova. A Wired explica que a IA agêntica pode reduzir muito o tempo desta última etapa, o que tornou possível a avaliação do Signal em quatro semanas. Os investigadores da DeepMind acrescentam que partiram com vantagem, porque a Signal Foundation já tinha feito verificação formal de partes mais pequenas do código.

Ehren Kret, diretor de tecnologia do Signal, afirmou num comunicado citado pela Wired: “Enquanto a verificação formal anterior se concentrava em partes mais pequenas do código, a abordagem da Google DeepMind permite uma ampliação significativa”. Acrescentou que verificar rigorosamente a implementação reforça a confiança do Signal nas garantias de privacidade do seu código, à medida que crescem as ameaças de segurança alimentadas por IA.

A DeepMind aponta como principal avanço um “processo de colaboração humano-IA”: os agentes contribuem e autocorrigem-se em quase todas as fases, enquanto os humanos revêem 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, pelo que a revisão humana da especificação continua central.

Um esforço paralelo em torno do Signal

O trabalho da 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 a sua implementação em Rust com o assistente de provas Lean. Prevê traduzir o código Rust do Signal para Lean com a ferramenta Aeneas e enumera 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 esta iniciativa à da DeepMind: são dois esforços distintos.

O que continua incerto?

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

O que 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 a conceção do protocolo, não um certificado para cada aplicação que o usa: a aplicação Signal completa não foi verificada, e a implementação, os servidores e as configurações de um produto ficam fora da prova. A especificação e a prova publicadas dão às equipas 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 esta abordagem para verificar formalmente o código próprio, mas já é possível perguntar aos fornecedores de software crítico que propriedades estão especificadas e provadas.