Google DeepMind usa IA para verificar segurança do Signal

Pesquisadores do Google DeepMind utilizaram inteligência artificial (IA) para realizar a verificação formal da segurança das mensagens do Signal. A conquista marca a primeira vez que sistemas automatizados ajudam a criar uma prova matemática que liga garantias de segurança de um protocolo à implementação real em código. A descoberta foi divulgada por meio de um relatório técnico.

O trabalho utilizou o AlphaProof Code, um sistema baseado em agentes de IA criado para especificação e verificação de software. Com a ajuda dessa tecnologia, a equipe validou que o aplicativo protege as conversas e roubos de dados, respondendo a um desafio lançado pela Beneficial AI Foundation. O processo envolveu transformar metas de segurança em especificações matemáticas revisadas por humanos, enquanto o modelo de IA gerou milhões de linhas de código em Lean, uma linguagem de programação especial, para testar a correção de software.

O desafio da era quântica

Ao passo em que computadores quânticos avançam com ameaças potenciais à criptografia tradicional, o Signal implementou defesas para proteger dados atuais e futuros. A introdução do Sparse Post Quantum Ratchet (SPQR) junto ao sistema atual forma o chamado Triple Ratchet, misturando chaves tradicionais e pós-quânticas por meio de funções de derivação. Essa proteção forma um sistema reforçado para manter os dados mais seguros.

A verificação desse tipo de protocolo complexo costumava exigir esforço humano passivo, como os anos investidos em sistemas anteriores. Com o AlphaProof Code, a equipe reduziu prazos e custos operacionais e manteve a verificação integrada ao fluxo de desenvolvimento do software no GitHub.

IA na segurança digital

A iniciativa representa uma aplicação da IA que vai além da geração de textos, imagens e programas. A tecnologia também pode ajudar a identificar falhas e conferir formalmente se sistemas computacionais seguem regras estabelecidas. Diferentemente de uma análise convencional, que procura possíveis vulnerabilidades por meio de testes e inspeções, a verificação formal permite demonstrar que determinadas propriedades são satisfeitas sob condições e premissas específicas.

Durante o trabalho, pesquisadores utilizaram versões do código com vulnerabilidades antigas inseridas propositalmente para avaliar se o sistema conseguia identificar problemas conhecidos. O processo durou cerca de quatro semanas e envolveu a análise de componentes do aplicativo.

O que significa para o futuro

A verificação formal pode ajudar desenvolvedores a encontrar problemas que passariam despercebidos em revisões tradicionais, aumentando a confiança em componentes importantes de softwares utilizados para proteger informações pessoais. No caso do Signal, o trabalho é especialmente relevante porque o aplicativo tem a privacidade como um de seus principais pilares, utilizando criptografia de ponta a ponta.

Ainda assim, é importante entender o alcance da pesquisa: verificar matematicamente determinadas propriedades do código não significa comprovar que todo o aplicativo está livre de vulnerabilidades. Problemas em outros componentes, falhas de implementação ou ataques aos próprios dispositivos dos usuários continuam sendo possibilidades. O pesquisador da Google DeepMind, Swat Chaudhuri, destacou a importância da colaboração humano-máquina e pontuou que o sonho é escalar essa tecnologia para a fase de design de novas ferramentas em sistemas digitais.