Google DeepMind verifica protocolo Signal com framework de IA

Pontos principais

• O Google DeepMind usou o AlphaProof Code, framework de agentes com vários modelos de linguagem, para verificação formal de código.
• A prova cobre propriedades de segurança do código executado nos dispositivos, entre elas a proteção das mensagens antes e depois do comprometimento temporário de um aparelho.
• Agentes com o modelo Gemini Carbon geraram mais de seis milhões de linhas de Lean, e especialistas humanos revisaram cada especificação.
• Os agentes apontaram cerca de 1% da base de código para revisão humana; o Lean verifica o restante.
• O processo levou quatro semanas, tempo que, segundo a DeepMind, equipes de especialistas levariam anos para cumprir.
• Dois bugs já corrigidos, reintroduzidos numa versão isolada, levaram o sistema a produzir prova verificada por máquina de que a versão era insegura.
• A DeepMind afirma que é a primeira vez que a implementação de um protocolo amplamente implantado é verificada formalmente por qualquer método.
• O CTO do Signal, Ehren Kret, diz que a verificação dá mais confiança nas garantias de privacidade do código.
• O material de verificação está sendo publicado como código aberto; a DeepMind não detalha as demais propriedades verificadas nem nomeia os bugs testados.