Investigadores da Google DeepMind usaram uma IA agentica para demonstrar matematicamente várias garantias criptográficas chave do protocolo Signal. Realizado em quatro semanas como um projeto de prova de conceito, este trabalho baseia-se numa nova estrutura de IA chamada AlphaProof Code.
- A DeepMind usou uma IA agentica para demonstrar matematicamente garantias criptográficas do protocolo Signal.
- Nas partes analisadas, os investigadores não encontraram novas vulnerabilidades.
- A ferramenta AlphaProof Code identificou corretamente falhas antigas em versões anteriores do Signal.
- A análise não cobriu a totalidade da aplicação móvel Signal, pelo que o alcance permanece limitado.
O protocolo Signal garante a encriptação das comunicações na aplicação Signal, mas também, segundo a fonte, no Google Messages e no WhatsApp. Para o artigo, esta demonstração constitui uma nova validação independente desta criptografia, que protege uma quantidade enorme de mensagens em todo o mundo. Também ilustra as capacidades de verificação formal da Google DeepMind.
A verificação formal consiste em usar a matemática para verificar que um software funciona como esperado, ou seja, que não contém falhas críticas. Os seus defensores consideram-na há muito tempo o Santo Graal da segurança de software. Mas o seu uso em larga escala permanece incerto, assim como a sua eficácia face a grandes quantidades de código.
Uma análise direcionada
Antes da era da IA, era necessário um tempo considerável para descrever as características de um software, transformar essas descrições em fórmulas e depois elaborar a prova. Segundo a fonte, a IA agentica pode reduzir drasticamente a duração desta última etapa. O âmbito da análise permanece, no entanto, limitado: não verificou formalmente, por exemplo, a totalidade da aplicação móvel Signal.
Nas partes do protocolo examinadas, os investigadores não encontraram nenhuma nova vulnerabilidade. Por outro lado, quando aplicaram o AlphaProof Code a versões antigas do Signal que continham falhas conhecidas e há muito corrigidas, a ferramenta identificou-as corretamente e mostrou que o protocolo não podia ser verificado formalmente nessas versões. Os investigadores publicam a especificação e a prova elaboradas para a análise do protocolo Signal, para facilitar outros trabalhos de verificação formal.
A rapidez do projeto deve-se em parte a trabalhos anteriores da Signal Foundation nesta área, como salientam os investigadores da DeepMind. «Embora a verificação formal anterior tenha incidido em porções mais reduzidas do código, a abordagem da Google DeepMind permite uma extensão significativa», afirma Ehren Kret, diretor técnico da Signal, num comunicado. «À medida que as ameaças de segurança relacionadas com a IA se multiplicam, verificar rigorosamente a implementação do protocolo Signal dá-nos uma confiança ainda maior nas garantias de confidencialidade do nosso código.»
Uma questão de custo e escala
Para serviços críticos usados em contextos de alto risco, poder verificar formalmente cada base de código e toda a cadeia de fornecimento de software seria, segundo Pushmeet Kohli, diretor científico da Google Cloud e vice-presidente de investigação na DeepMind, um grande avanço. «Se agora podemos verificar a correção destas implementações, podemos ficar tranquilos. Imagine os bancos, e todas as outras empresas que dependem de garantias e que se preocupam com bugs, poderem agora afirmar: « posso provar estas propriedades »», afirma.
Permanente a questão, aberta para todo o setor tecnológico, da capacidade da verificação formal automatizada por IA de realmente passar à escala, e a um custo razoável. A DeepMind realizou a análise do Signal gratuitamente, no âmbito de um projeto de investigação, e a Google não quis divulgar o seu custo. A empresa também não especificou se planeia comercializar um produto ou serviço de verificação formal.
Os investigadores consideram que alguns dos seus avanços cruciais incidem sobre um «processo de colaboração humano-IA», nas palavras de Swarat Chaudhuri, investigador científico na DeepMind. Este processo permite que os agentes contribuam e se corrijam em quase todas as etapas, ao mesmo tempo que solicitam a opinião e validação humanas em momentos-chave. «Não queremos este mundo de ambiente, onde a IA define os objetivos, onde a IA produz as provas, e onde passamos nos testes que ela própria escreveu. Existe um meio-termo.»
