Rafael NazarO Google utilizou inteligência artificial (IA) para analisar propriedades de segurança do Signal, um dos aplicativos de mensagens conhecidos por seus recursos de privacidade. O trabalho foi conduzido pelo Google DeepMind, divisão de pesquisa em IA da empresa, com o uso de demonstrações matemáticas aplicadas a partes do código do mensageiro.
A análise utilizou o AlphaProof Code, sistema desenvolvido para trabalhar com demonstrações formais. Durante aproximadamente quatro semanas, a ferramenta examinou o código do Signal e ajudou os pesquisadores a verificar se determinadas propriedades de segurança eram matematicamente válidas.
O trabalho foi realizado com a linguagem de programação Lean, utilizada na construção de provas matemáticas formais. Nesse ambiente, uma propriedade de segurança pode ser descrita matematicamente e submetida a um verificador, que confere se a demonstração está correta.
Diferentemente de uma análise convencional, baseada na busca por possíveis vulnerabilidades em testes e inspeções, a verificação formal permite demonstrar que determinadas propriedades são atendidas sob condições e premissas específicas.
Os pesquisadores também analisaram versões do código que receberam, de forma proposital, vulnerabilidades antigas. O objetivo era avaliar se o sistema conseguiria identificar problemas conhecidos e verificar as propriedades de segurança estabelecidas. O processo envolveu componentes do aplicativo e durou cerca de quatro semanas.
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 auxiliar na identificação de falhas e na verificação formal de que sistemas computacionais seguem regras definidas.
Segundo o Olhar Digital, a verificação formal pode ajudar desenvolvedores a encontrar problemas que passariam despercebidos em revisões tradicionais. O método também pode aumentar a confiança em componentes importantes de softwares usados para proteger informações pessoais.
No caso do Signal, a pesquisa tem relevância porque a privacidade é um dos principais pilares do aplicativo. O mensageiro utiliza criptografia de ponta a ponta para proteger as conversas e impedir que terceiros acessem o conteúdo das mensagens durante a transmissão.
Ainda assim, a verificação matemática de determinadas propriedades do código não comprova que todo o aplicativo esteja livre de vulnerabilidades. Problemas em outros componentes, falhas de implementação ou ataques aos dispositivos dos usuários continuam sendo possibilidades.
O trabalho do Google DeepMind mostra como sistemas de IA podem contribuir para tornar softwares mais seguros, auxiliando especialistas na análise de códigos complexos e na construção de provas matemáticas que sustentem suas garantias de segurança.
