Realizado como uma espécie de projeto de prova de conceito em apenas quatro semanas, o trabalho tem importância em duas frentes. Ele serve como mais uma validação independente da criptografia que protege uma enorme quantidade das comunicações do mundo em plataformas como o aplicativo Signal, o Google Messages e o WhatsApp. E demonstra as capacidades de verificação formal do Google DeepMind usando uma nova estrutura de inteligência artificial (IA) chamada AlphaProof Code.
De modo mais amplo, a verificação formal assistida por IA está em alta, mas não está claro o quão prática ela será para uso generalizado e o quão eficaz pode ser para proteger grandes volumes de código. Defensores da verificação formal há muito a chamam de uma espécie de santo graal da segurança de software, porque usa a matemática para checar e validar se o software funciona como previsto — em outras palavras, se não possui vulnerabilidades críticas.
Antes da era da IA, era extremamente demorado para as pessoas descreverem as características do software que queriam provar, transformarem esses resumos em fórmulas e, então, desenvolverem a prova. A IA agêntica pode reduzir significativamente o tempo dessa última etapa, viabilizando análises como a avaliação do Signal feita pela DeepMind. Mas mesmo essa análise teve escopo limitado — ela não verificou formalmente, por exemplo, todo o aplicativo móvel Signal — e os pesquisadores da DeepMind ressaltam que suas descobertas são apenas um marco em um processo maior.
“Estamos muito animados com esse resultado, mas ainda há uma longa distância a percorrer antes de conseguirmos escalar isso para todo o software do mundo, e queremos fazer isso”, diz Swarat Chaudhuri, cientista de pesquisa da DeepMind, em entrevista à WIRED.
A análise da DeepMind não encontrou novas vulnerabilidades nas partes do protocolo Signal que foram examinadas. No entanto, quando os pesquisadores usaram o AlphaProof Code em versões antigas do Signal que contêm vulnerabilidades conhecidas e corrigidas há muito tempo, a ferramenta as identificou corretamente e mostrou que o protocolo não podia ser formalmente verificado. Os pesquisadores vão divulgar a especificação e a prova que desenvolveram para a análise do protocolo Signal, a fim de auxiliar outros trabalhos de verificação formal.
Embora a velocidade do projeto tenha chamado atenção, os pesquisadores da DeepMind destacam que conseguiram sair na frente, em certa medida, graças a trabalhos anteriores de verificação formal conduzidos pela Signal Foundation.
“Enquanto a verificação formal anterior se concentrava em partes menores do código, a abordagem do Google DeepMind possibilita uma expansão significativa”, afirma Ehren Kret, diretor de tecnologia da Signal, em comunicado. “À medida que as ameaças de segurança impulsionadas por IA crescem, verificar rigorosamente a implementação do protocolo Signal nos dá ainda mais confiança nas garantias de privacidade do nosso código.”
Para serviços críticos usados em ambientes de alto risco, seria um sonho conseguir verificar formalmente todas as bases de código e cadeias inteiras de suprimento de software. “Se agora você pode verificar a corretude dessas implementações, então pode ficar tranquilo”, diz Pushmeet Kohli, cientista-chefe do Google Cloud e vice-presidente de pesquisa da DeepMind. “Imagine bancos, imagine todas as outras empresas que dependem de garantias e se preocupam com bugs, que agora poderiam dizer: ‘Eu posso provar essas propriedades.’”
A grande questão para todo o setor de tecnologia, porém, é se a verificação formal automatizada por IA pode realmente escalar e, além disso, se pode fazê-lo a um custo viável. A DeepMind conduziu a análise do Signal gratuitamente, como projeto de pesquisa, e o Google não divulgou quanto custou o trabalho. A empresa também não quis comentar se tem planos de lançar um produto ou serviço comercial de verificação formal.
Os pesquisadores afirmam que alguns de seus avanços cruciais estão no desenvolvimento de um “processo de colaboração humano-IA”, como Chaudhuri o descreve, que permite que agentes contribuam e se autocorrijam em quase todas as fases do processo, ao mesmo tempo em que buscam a contribuição e a revisão humana em momentos-chave. “Não queremos esse tipo de mundo de vibe em que a IA gera os objetivos, a IA gera as provas e basicamente faz testes que ela mesma escreveu”, diz Chaudhuri. “Existe um meio-termo.”
