A Google DeepMind apresentou o AlphaProof Code, um sistema de agentes de inteligência artificial que conseguiu demonstrar matematicamente propriedades de segurança do código utilizado pelo protocolo Signal. A investigação foi além da análise teórica da criptografia e chegou ao código compilado, o que permite verificar se a implementação respeita determinadas garantias de proteção das comunicações.
O trabalho, anunciado a 10 de novembro, foi concluído em quatro semanas. Segundo a Google, os agentes produziram mais de seis milhões de linhas de provas matemáticas, posteriormente verificadas por um sistema independente dos modelos de IA. A empresa considera que esta abordagem poderá reduzir o tempo e os recursos necessários para analisar software crítico, embora os resultados não representem uma certificação de segurança de toda a aplicação Signal.
AlphaProof Code verifica o código compilado do Signal
A principal diferença do AlphaProof Code está na profundidade da análise. Tradicionalmente, a verificação formal de protocolos criptográficos concentra-se nas especificações, ou seja, nas regras matemáticas que definem como um sistema deve funcionar.
O problema é que uma implementação pode introduzir erros mesmo quando o protocolo foi corretamente concebido. Uma falha na programação ou na passagem para código executável pode comprometer propriedades de segurança previstas no desenho original.
O AlphaProof Code procura reduzir essa distância entre a teoria e a implementação. Segundo a publicação oficial da Google DeepMind, os investigadores utilizaram agentes baseados no Gemini Carbon para produzir provas matemáticas sobre o código compilado de componentes criptográficos do Signal.
O processo começou com a definição das propriedades que deveriam ser verificadas. Especialistas trabalharam com modelos de IA para transformar os objetivos de segurança em especificações matemáticas, que foram posteriormente revistas por humanos.
A partir dessas especificações, os agentes produziram as demonstrações na linguagem Lean. Este sistema verifica formalmente as provas e permite confirmar se as conclusões decorrem das premissas estabelecidas, sem depender da avaliação do próprio modelo de inteligência artificial.
De acordo com a Google, os agentes assinalaram cerca de 1% do código das provas para revisão humana adicional. A verificação automática permitiu concentrar o trabalho dos especialistas nos pontos identificados como mais exigentes.
Que garantias de segurança do protocolo Signal foram verificadas?
A investigação incidiu sobre propriedades fundamentais do protocolo criptográfico Signal, utilizado para proteger comunicações em diferentes aplicações.
Entre as garantias analisadas encontram-se a autenticação das comunicações, o sigilo futuro e a proteção após o comprometimento temporário de um dispositivo.
O sigilo futuro, conhecido como forward secrecy, procura impedir que a exposição de uma chave atual permita recuperar mensagens anteriores. A segurança após comprometimento, ou post-compromise security, diz respeito à capacidade de uma comunicação recuperar determinadas garantias de confidencialidade depois de um incidente, desde que estejam reunidas as condições previstas pelo protocolo.
Estas propriedades são particularmente importantes porque uma comunicação cifrada não depende apenas da resistência dos algoritmos criptográficos. Também depende da forma como as chaves são criadas, utilizadas, renovadas e protegidas.
Para testar a capacidade do AlphaProof Code de distinguir implementações seguras de versões vulneráveis, os investigadores reintroduziram duas falhas reais, anteriormente corrigidas, numa versão isolada do código.
Em ambos os casos, o sistema conseguiu produzir provas verificadas matematicamente de que as versões alteradas não cumpriam as propriedades de segurança exigidas.
O resultado sugere que a tecnologia pode servir não apenas para confirmar garantias previamente definidas, mas também para identificar situações em que alterações ao código comprometem essas garantias.
Quatro semanas para um trabalho que poderia demorar anos
A Google DeepMind afirma que a verificação demorou quatro semanas, enquanto trabalhos semelhantes, realizados através de métodos tradicionais, poderiam exigir vários anos de esforço especializado.
A diferença resulta sobretudo da automatização da produção das provas matemáticas, uma das etapas mais trabalhosas da verificação formal.
Contudo, esta comparação deve ser interpretada com cautela. O tempo necessário depende da dimensão do software, das propriedades analisadas e da existência de especificações anteriores. A Google também não divulgou os custos computacionais da investigação, pelo que ainda não é possível avaliar a viabilidade económica da abordagem em diferentes contextos.
A importância do trabalho foi reconhecida por Ehren Kret, diretor de tecnologia do Signal, que considera que a utilização de agentes de IA pode ampliar o alcance da verificação formal e reforçar a confiança nas garantias de privacidade do código.
O projeto também ilustra uma aplicação defensiva da inteligência artificial na cibersegurança. Em vez de procurar apenas vulnerabilidades conhecidas, os agentes procuram demonstrar que determinadas classes de falhas não existem no código analisado, dentro das condições estabelecidas.
Esta abordagem complementa os métodos tradicionais de auditoria, testes de segurança e análise de vulnerabilidades.
A verificação matemática não torna o Signal invulnerável
Apesar dos resultados, a investigação não demonstra que o Signal esteja protegido contra todos os ataques. As provas abrangem componentes e propriedades específicas do protocolo, não a totalidade da aplicação, dos sistemas operativos ou dos servidores envolvidos nas comunicações.
Também não eliminam riscos relacionados com dispositivos comprometidos, roubo de credenciais, engenharia social ou erros dos utilizadores.
Esta distinção é importante. Como o TecheNet noticiou no artigo sobre o ataque que comprometeu comunicações políticas na Alemanha através do Signal, a segurança de um protocolo criptográfico não impede que uma conta seja comprometida por outros meios.
A investigação da Google também depende das especificações matemáticas escolhidas pelos especialistas. Uma prova pode demonstrar que o código cumpre determinadas propriedades, mas não garante a ausência de vulnerabilidades fora desse âmbito.
A Google DeepMind disponibilizou as especificações e os materiais de verificação formal para consulta e análise da comunidade técnica. A publicação permite que outros investigadores examinem o trabalho e avaliem as condições em que as provas foram produzidas.
O AlphaProof Code permanece um projeto de investigação. A empresa não anunciou uma versão comercial nem esclareceu quando a tecnologia poderá ser integrada em ferramentas de desenvolvimento de software.
Outros artigos interessantes:
