# DeepMind usou IA para verificar o código criptográfico do Signal

> O AlphaProof Code verificou propriedades importantes de segurança no código compilado do Signal em quatro semanas. A prova cobre garantias específicas, não todos os componentes do Signal.

Oossa · 2026-11-11 · https://oossa.com/pt/deepmind-used-ai-to-verify-signal-s-cryptographic-code

O Google DeepMind afirma ter usado o AlphaProof Code para verificar matematicamente propriedades importantes de segurança da libsignal, implementação de referência do protocolo de mensagens Signal. O trabalho levou quatro semanas. Segundo a DeepMind, verificações semelhantes costumavam levar anos para equipes especializadas.

O sistema combinou pesquisadores humanos com agentes de IA. Pesquisadores e IA ajudaram a traduzir os objetivos de segurança do Signal em especificações matemáticas, que foram revisadas por pessoas. Em seguida, agentes com tecnologia Gemini Carbon geraram cerca de 6,5 milhões de linhas de código de prova em Lean. Lean é uma linguagem de programação cujo verificador pode confirmar se uma prova matemática segue suas regras. Os agentes sinalizaram cerca de um por cento da base de código para revisão humana.

## O que a prova abrange?

Os pesquisadores verificaram o código de máquina compilado do handshake pós-quântico PQXDH e do Triple Ratchet da libsignal. Eles provaram propriedades específicas, incluindo sigilo futuro, autenticação e proteção após o comprometimento de um dispositivo. O artigo da pesquisa diz que o código foi compilado a partir de Rust sem modificações, usando um compilador padrão, e depois verificado como código de máquina AArch64.

Isso vai além de provar que um projeto abstrato é seguro: vincula garantias de segurança especificadas ao código compilado. A DeepMind chama o trabalho de primeira verificação formal, nesse nível de profundidade, da implementação de um protocolo criptográfico amplamente utilizado. A equipe também reintroduziu dois bugs já corrigidos em uma versão isolada do código; o sistema produziu provas de que as versões com os bugs não atendiam às propriedades de segurança especificadas.

## A prova tem limites

Isso não é uma garantia matemática de que todos os componentes do Signal, ou todos os aplicativos que usam o protocolo, estejam livres de problemas de segurança. A prova abrange propriedades selecionadas da libsignal, não o aplicativo inteiro. Ela também depende de especificações aprovadas, do verificador do Lean e de contratos para rotinas criptográficas de baixo nível. O The Register observa que o resultado não prova o sigilo computacional dos bytes das mensagens reais; o artigo da DeepMind descreve provas em modelos simbólicos e computacionais, que dependem de pressupostos sobre as primitivas criptográficas subjacentes.

A DeepMind afirma que está disponibilizando os materiais de verificação para que outras pessoas possam usá-los. A empresa espera aplicar a abordagem a áreas como firmware de dispositivos médicos e software de redes elétricas, mas diz que será preciso pesquisar mais para ampliar o método. O trabalho é um passo rumo à verificação de mais código usado no mundo real, não uma evidência de que esses outros sistemas tenham sido verificados.

## Os fatos

- O Google DeepMind anunciou o AlphaProof Code em 10 de novembro de 2026.
- O sistema gerou cerca de 6,5 milhões de linhas de código de prova em Lean no trabalho com a libsignal.
- A verificação abrangeu o handshake PQXDH e o Triple Ratchet em código de máquina AArch64 compilado.
- Os pesquisadores reintroduziram dois bugs já corrigidos, e o sistema provou que as versões afetadas não atendiam às propriedades de segurança especificadas.

## Por que importa

Para quem usa o Signal, o trabalho acrescenta uma prova verificada por máquina de propriedades específicas de segurança na implementação do protocolo central. Ele não demonstra que o aplicativo inteiro esteja livre de bugs, e a prova depende de pressupostos sobre componentes criptográficos.

## Fontes e referências

1. [Google Deepmind's AlphaProof Code verified Signal's cryptographic core in four weeks instead of years](https://the-decoder.com/google-deepminds-alphaproof-code-verified-signals-cryptographic-core-in-four-weeks-instead-of-years/) – The Decoder, 2026-11-11
2. [Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/) – Google DeepMind, 2026-11-10
3. [Google DeepMind](https://google-deepmind.github.io/code-verification/) – Google DeepMind
4. [The Register](https://www.theregister.com/ai-and-ml/2026/11/10/google-deepmind-melds-humans-and-ai-agents-to-vet-signals-secure-messaging-techniques/5308625) – The Register

Última atualização: 2026-11-11