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.
