O Google utilizou inteligência artificial (IA) para analisar e verificar propriedades de segurança do Signal, um dos aplicativos de mensagens mais conhecidos por seus recursos de privacidade. O trabalho foi conduzido pelo Google DeepMind, divisão de pesquisa em IA da empresa, e empregou demonstrações matemáticas para examinar 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.A iniciativa representa aplicação da IA que vai além da geração de textos, imagens e programas: a tecnologia também pode ajudar a identificar falhas e conferir formalmente se sistemas computacionais seguem regras estabelecidas.Como a IA verificou a segurança do Signal?O trabalho utilizou a linguagem de programação Lean, empregada na construção de provas matemáticas formais. Nesse ambiente, uma propriedade de segurança pode ser descrita matematicamente e submetida a um verificador capaz de conferir se a demonstração está correta;Diferentemente de uma análise convencional, que procura possíveis vulnerabilidades por meio de testes e inspeções, a verificação formal permite demonstrar que determinadas propriedades são satisfeitas sob condições e premissas específicas;Durante o trabalho, os pesquisadores também utilizaram versões do código com vulnerabilidades antigas inseridas propositalmente. A ideia era avaliar se o sistema conseguia identificar problemas conhecidos e verificar as propriedades de segurança estabelecidas;O processo durou cerca de quatro semanas e envolveu a análise de componentes do aplicativo.Trabalho foi conduzido pelo Google DeepMind, divisão de pesquisa em IA do Google – Imagem: Poetra.RH/ShutterstockLeia mais:Google lança chips de IA para proteger dados e ampliar memóriaGoogle é processado por conversas sobre suicídio entre IA e garota de 13 anosGoogle, Meta e TikTok processam Califórnia para barrar lei de proteção a menoresO que a descoberta significa para a segurança digital?A verificação formal pode ajudar desenvolvedores a encontrar problemas que passariam despercebidos em revisões tradicionais. Também permite aumentar a confiança em componentes importantes de softwares utilizados para proteger informações pessoais.No caso do Signal, o trabalho é especialmente relevante porque o aplicativo tem a privacidade como um de seus principais pilares. O mensageiro utiliza criptografia de ponta a ponta para proteger as conversas, impedindo que terceiros tenham acesso ao conteúdo das mensagens durante a transmissão.Ainda assim, é importante entender o alcance da pesquisa: verificar matematicamente determinadas propriedades do código não significa comprovar que todo o aplicativo está livre de vulnerabilidades.Problemas em outros componentes, falhas de implementação ou ataques aos próprios dispositivos dos usuários continuam sendo possibilidades.A iniciativa do Google 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.O post IA do Google analisa código do Signal em busca de falhas de segurança apareceu primeiro em Olhar Digital.