Tudo sobre Google
Tudo sobre Inteligência Artificial
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.Continua após a publicidadeA 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/Shutterstock
Leia mais:O 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.
Rodrigo Mozelli
Rodrigo Mozelli é jornalista formado pela Universidade Metodista de São Paulo (UMESP) e, atualmente, é redator do Olhar Digital.
Ver todos os artigos →
