Pesquisadores do Google DeepMind usaram um novo sistema de inteligência artificial chamado AlphaProof Code para "verificar formalmente" parte das garantias criptográficas do protocolo do Signal, método usado pelo app de mensagens homônimo e também pelo WhatsApp e pelo Google Messages, segundo a Wired e a ZDNet. Verificação formal é a técnica que usa matemática para provar que um software funciona exatamente como deveria, sem as falhas que testes convencionais podem não encontrar.

O trabalho levou cerca de quatro semanas, segundo as duas fontes. A Wired descreve o projeto como uma espécie de prova de conceito, e a ZDNet detalha que humanos trabalharam ao lado de agentes de IA para decidir o que precisava ser provado, enquanto múltiplos agentes rodando o modelo Gemini Carbon, o mais recente do Google, executavam a verificação.

Por que a verificação formal é difícil

A Wired explica que a verificação formal é vista há tempos como uma espécie de "santo graal" da segurança de software, porque usa matemática para comprovar que um programa funciona exatamente como deveria, sem vulnerabilidades críticas escondidas. Antes da IA, o processo era extremamente demorado: alguém precisava descrever manualmente as características do software que queria provar, transformar essa descrição em fórmulas e só então desenvolver a prova — um trabalho que podia levar anos para sistemas complexos.

Agentes de IA reduzem boa parte desse tempo, segundo a Wired, o que tornou viável uma análise como a do protocolo do Signal. A ZDNet acrescenta que outras empresas de IA, como a OpenAI, também têm usado modelos para resolver problemas matemáticos complexos — alguns com quase um século de existência —, um sinal de que sistemas de IA vêm acelerando esse tipo de trabalho manual que antes só matemáticos e especialistas em segurança conseguiam fazer.

Nenhuma falha nova, mas identificou bugs antigos conhecidos

A análise não encontrou nenhuma vulnerabilidade nova nas partes do protocolo que avaliou, segundo a Wired. Como teste de controle, os pesquisadores também aplicaram o AlphaProof Code a versões antigas do Signal que já tinham falhas conhecidas e corrigidas há tempos — nesses casos, o sistema identificou corretamente os problemas e mostrou que aquelas versões não passavam pela verificação formal, segundo a mesma fonte.

Segundo a ZDNet, os agentes também auditaram as próprias provas que geraram e apontaram os trechos que precisavam de uma segunda checagem humana — apenas 1% do código analisado, segundo os pesquisadores citados pelo veículo.

Trabalho não cobriu o aplicativo completo

A verificação ficou limitada a partes do protocolo e não cobriu, por exemplo, o aplicativo móvel completo do Signal, segundo a Wired. Swarat Chaudhuri, cientista pesquisador do DeepMind, disse à publicação que o resultado é apenas "um marco em um processo maior" até que a técnica possa ser aplicada em escala a todo tipo de software.

O avanço também se apoiou em verificações formais anteriores que a própria Signal Foundation já havia feito em partes menores do código, segundo as duas fontes. Ehren Kret, diretor de tecnologia do Signal, disse à Wired que a abordagem do DeepMind "permite uma expansão significativa" em relação a esse trabalho anterior, e que, com o crescimento das ameaças de segurança ligadas à IA, verificar rigorosamente a implementação do protocolo dá à empresa "ainda mais confiança" nas garantias de privacidade do seu código.

DeepMind planeja abrir o código do sistema

Segundo a ZDNet, o Google DeepMind pretende disponibilizar o AlphaProof Code como código aberto, com o objetivo de ajudar outros projetos a verificar sistemas críticos. A Wired acrescenta que os pesquisadores também vão divulgar a especificação e a prova que desenvolveram para o Signal, para apoiar outros trabalhos de verificação formal.

Na prática

  • O que foi provado: partes das garantias criptográficas do protocolo do Signal, usado também pelo WhatsApp e pelo Google Messages, foram matematicamente verificadas pela primeira vez, segundo os pesquisadores citados pela Wired.
  • O que não foi coberto: a verificação não incluiu o aplicativo móvel completo do Signal.
  • Quando aconteceu: o trabalho foi conduzido em cerca de quatro semanas e divulgado nesta semana pela Wired e pela ZDNet.
  • O que vem a seguir: o Google DeepMind planeja abrir o código do AlphaProof Code e publicar a especificação e a prova usadas no Signal, para uso por outros projetos.