IA do Google analisa código do Signal em busca de falhas de segurança

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.

• Google lança chips de IA para proteger dados e ampliar memória
• Google é processado por conversas sobre suicídio entre IA e garota de 13 anos
• Google, Meta e TikTok processam Califórnia para barrar lei de proteção a menores

[tpd_news_ad]

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 é jornalista formado pela Universidade Metodista de São Paulo (UMESP) e, atualmente, é redator do Olhar Digital.