Google DeepMind usa IA para verificar matematicamente partes do protocolo Signal

Pesquisadores do Google DeepMind usaram IA com agentes para provar matematicamente, no que se chama de verificação formal, várias garantias criptográficas centrais do protocolo Signal. O trabalho foi feito como prova de conceito em apenas quatro semanas, com um novo framework chamado AlphaProof Code.

O resultado vale por dois motivos. Ele funciona como mais uma validação independente da criptografia que protege uma enorme quantidade de comunicações, no app Signal, no Google Messages e no WhatsApp. E mostra do que a DeepMind é capaz em verificação formal.

A análise não encontrou vulnerabilidades novas nos trechos do protocolo que examinou. Quando a ferramenta foi aplicada a versões antigas do Signal, que tinham falhas conhecidas e já corrigidas, ela as identificou e mostrou que o protocolo naquelas versões não poderia ser verificado formalmente. A DeepMind vai divulgar a especificação e a prova desenvolvidas, para ajudar outros trabalhos na área.

Há limites. A análise não cobriu o aplicativo móvel do Signal inteiro, e os pesquisadores dizem que é só um marco num processo maior. Eles também tiveram uma vantagem inicial, por causa de trabalhos anteriores de verificação formal feitos pela Signal Foundation, que se concentraram em partes menores do código. Para Ehren Kret, diretor de tecnologia do Signal, a abordagem da DeepMind permite uma expansão significativa dessa verificação.

A verificação formal usa matemática para checar se um software faz o que deveria, e há tempos é vista como um ideal da segurança de software. Antes da IA, descrever as propriedades desejadas, traduzi-las em fórmulas e construir a prova tomava muito tempo. Os agentes de IA reduzem sobretudo o tempo da última etapa. Pushmeet Kohli, do Google Cloud e da DeepMind, imagina bancos e outras empresas podendo afirmar que conseguem provar certas propriedades de seus sistemas.

Resta saber se isso escala e a que custo. A análise do Signal foi gratuita, como projeto de pesquisa, e o Google não revelou quanto ela custou nem disse se pretende lançar um produto ou serviço comercial de verificação formal. Swarat Chaudhuri, pesquisador da DeepMind, afirmou que ainda há "uma longa distância" até aplicar isso a todo o software do mundo. Ele defende um processo de colaboração entre humanos e IA, com revisão humana em etapas-chave, em vez de a IA gerar sozinha tanto os objetivos quanto as provas.