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.
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.
