Pesquisadores do Google DeepMind conseguiram usar 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 publicado
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, o que responde a um desafio lançado pela Beneficial AI Foundation em abril deste ano.
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 (linguagem de programação especial) para testar a correção de software.
Pesquisador da Google DeepMind e professor da Universidade do Texas, nos Estados Unidos, Swat Chaudhuri destacou, ao veículo especializado The Register, a importância da colaboração humano-máquina nesse processo:
O desafio da era quântica
Ao passo em que computadores quânticos avançam com ameaças potenciais à criptografia tradicional baseada em curvas elípticas, o Signal implementou defesas para proteger dados atuais e futuros.
