DeepMind provou matematicamente a segurança do código do Signal em 4 semanas, em vez de anos

Quem já escreveu criptografia conhece uma verdade desagradável: um protocolo pode ser provado de forma elegante no papel, e a vulnerabilidade ainda assim acabará aparecendo no código. Entre o esquema e a implementação existe um abismo, e é ali que vivem os bugs de verdade. A Google DeepMind afirma ter ensinado agentes de IA a fechar esse abismo para um dos protocolos mais importantes do mundo, aquele que protege as conversas no Signal e no Google Messages.

O que exatamente foi feito

O sistema se chama AlphaProof Code. É um framework multiagente baseado em vários LLMs, que divide o trabalho da mesma forma que uma equipe de pesquisa dividiria. Primeiro, especialistas humanos, junto com os modelos, traduzem os objetivos de segurança do Signal em especificações matemáticas formais. Cada especificação é verificada manualmente por uma pessoa. Depois, os agentes baseados no Gemini Carbon escrevem as próprias provas na linguagem Lean, resultando em mais de seis milhões de linhas.

A seguir vem a parte mais prática. O próprio Lean verifica a correção de cada prova, então não é preciso confiar cegamente no modelo: uma conclusão incorreta simplesmente não passa na verificação. Os agentes também auditaram o resultado e apontaram os pontos que exigem o olhar de uma pessoa. Isso corresponde a cerca de 1% da base de código. Os especialistas se concentraram nesses trechos, em vez de reler milhões de linhas.

Por que isso não é mais uma auditoria

A verificação formal comum de protocolos para no nível do design: prova-se que o esquema é seguro. Aqui, os agentes foram além e provaram propriedades do código compilado que roda nos dispositivos. Por exemplo, que as mensagens permanecem protegidas antes e depois de um comprometimento temporário de um dispositivo.

Para testar a honestidade do sistema, os autores fizeram um teste simples. Em uma versão isolada do código do Signal, reintroduziram dois bugs reais que já haviam sido corrigidos. Nos dois casos, o sistema gerou uma prova verificável por máquina de que essa versão é insegura. Ou seja, a ferramenta distingue o código correto do incorreto, e não simplesmente «aprova» tudo.

Segundo a DeepMind, tudo levou quatro semanas, enquanto para equipes de especialistas esse tipo de trabalho tradicionalmente levava anos. O diretor técnico do Signal, Eren Kret, chamou a tradução automática de código de produção em teoremas de Lean de um grande avanço.

Limitações e conclusões práticas

É preciso olhar a escala com sobriedade. Trata-se de um único protocolo, estudado de forma longa e minuciosa, e a maior parte dos números declarados se baseia em autorrelato da DeepMind. Os humanos não foram removidos do processo: o que se considera «seguro» ainda é definido pelos especialistas, e um erro na especificação gera a prova de algo diferente do que se precisava. Os próprios autores dizem que são necessárias mais pesquisas para escalar. As áreas anunciadas, firmware de dispositivos médicos e software para redes elétricas, por enquanto são apenas planos.

O que isso significa para desenvolvedores e fundadores?

• O esquema «o LLM escreve, o verificador formal aceita ou rejeita» funciona para tarefas em que o custo do erro é alto. O modelo pode errar; o verificador, não.
• Se você desenvolve criptografia, lógica de pagamentos ou código embarcado crítico, a verificação formal deixa de ser privilégio de equipes acadêmicas com orçamento para anos.
• A habilidade de formular especificações se torna mais valiosa do que a de escrever provas. O gargalo se desloca para a pergunta «o que, afinal, queremos garantir?».

Um ponto positivo adicional é que a DeepMind abre os artefatos de verificação. Eles podem ser estudados e usados como modelo para experimentos próprios com Lean e agentes. Junto com ferramentas como o CodeMender, que encontram e corrigem vulnerabilidades, as provas formais passam a fazer parte do perímetro de defesa comum, e não de uma rara excentricidade acadêmica.