Ferramenta do Google DeepMind verifica formalmente garantias de segurança do Signal Protocol
Aprofundamento CEVIU
Aprofundamento
Pesquisadores do Google DeepMind usaram o AlphaProof Code, framework baseado em agentes de IA, para verificar formalmente várias garantias criptográficas centrais do Signal Protocol. O trabalho foi feito como prova de conceito em quatro semanas. O protocolo protege comunicações no app Signal, no Google Messages e no WhatsApp.
A análise não achou vulnerabilidades novas nos trechos examinados. Quando o AlphaProof Code foi apontado para versões antigas do Signal, com falhas conhecidas e corrigidas há tempo, ele as identificou e mostrou que o protocolo naquela versão não poderia ser verificado formalmente. O escopo é limitado: o app móvel inteiro não foi verificado. A equipe teve uma vantagem inicial por causa de trabalhos anteriores de verificação formal da Signal Foundation, que cobriam partes menores do código. A especificação e a prova serão liberadas para apoiar outros trabalhos da área. O processo prevê colaboração entre humanos e IA, com revisão humana em pontos-chave. Segundo a fonte, o Google não informou o custo da análise nem se pretende lançar um produto comercial de verificação formal.
O que mudou
O CEVIU já havia coberto o anúncio. Em 10 de novembro de 2026, noticiou "Google DeepMind apresenta AlphaProof Code e verifica formalmente o código do protocolo Signal". Em 11 de novembro de 2026, publicou "DeepMind apresenta AlphaProof Code, que verifica propriedades de segurança do código criptográfico do Signal", que descrevia o uso de especificações revisadas por humanos e provas em Lean. O que esta matéria acrescenta são os limites do resultado: nenhum bug novo, reprodução de falhas antigas e o escopo parcial.
Por que isso importa
Para quem opera segurança, o resultado funciona como mais uma validação independente do Signal Protocol, não como prova de que o app inteiro está livre de falhas. A redução do tempo de prova com agentes é o ponto a acompanhar. Sem custo divulgado e sem produto anunciado, ainda é cedo para tratar isso como opção de auditoria no dia a dia.
Linha do tempo
O CEVIU noticia o anúncio do AlphaProof Code e da verificação formal do protocolo Signal.
Detalhes da análise: quatro semanas, nenhum bug novo e reprodução de falhas antigas em versões anteriores do Signal.
Perguntas frequentes
O que é verificação formal?
É o uso de matemática para provar que um software se comporta como especificado, ou seja, que não tem certas falhas críticas. Exige descrever as propriedades desejadas, transformá-las em fórmulas e construir a prova. Esse último passo é o que os agentes de IA aceleram.
A análise encontrou novas vulnerabilidades no Signal?
Não. Nos trechos analisados, nenhum bug novo apareceu. Em versões antigas com falhas conhecidas e já corrigidas, a ferramenta as identificou e mostrou que a verificação não fechava.
O app Signal inteiro foi verificado?
Não. O trabalho cobriu várias garantias criptográficas do protocolo, não o app móvel completo. Os próprios pesquisadores tratam o resultado como um marco dentro de um processo maior.
Isso já está disponível como produto?
Não há anúncio. O Google fez a análise gratuitamente, como pesquisa, e não informou o custo nem se pretende lançar um serviço comercial. A especificação e a prova do Signal serão liberadas para outros pesquisadores.
Fontes
- wired.comfonte original
- Categoria
- CEVIU Segurança da Informação
- Publicado
- 11 de novembro de 2026
- Editoria
- CEVIU Segurança da Informação