A Google alargou o acesso ao Gemini 4 Carbon e indica que agentes construídos sobre este modelo contribuíram para verificar formalmente garantias de segurança centrais do código do protocolo Signal.
Os desenvolvedores e empresas que pagam podem agora usar o Carbon através da API Gemini e do Gemini for business, e os subscritores Google AI Ultra também têm acesso. Aplicam-se tarifas de introdução de 2 e 10 dólares por milhão de tokens de entrada e saída até 30 de novembro, antes de serem duplicadas. Um token é uma unidade de texto que o modelo processa para ler ou produzir conteúdo.
Até agora, apenas alguns defensores em cibersegurança membros do programa Fairwind da Google podiam usar o Carbon. Continuam a ter de pertencer a este programa para aceder ao Carbon for cyber, uma versão que a Google apresenta como líder nos principais benchmarks de deteção, exploração e correção de vulnerabilidades.
Aplicações em cibersegurança
Segundo a Google, a empresa Wiz usou o Carbon for cyber para encontrar falhas do tipo «zero-day» em dois grandes fornecedores de SaaS, em duas horas. A equipa Cloud Vulnerability Research (CVR) da Google, por seu lado, usou o modelo para confirmar que dois bugs de um projeto open source popular eram exploráveis, com uma gravidade comparável à do PHP2Shell, um par de falhas PHP já exploradas por atacantes.
«Ao usar o Carbon para construir uma prova de conceito, a CVR ajudou os mantenedores a reclassificar o bug como crítico e a publicar rapidamente um patch», indica a Google.
Verificar o código do Signal
Por outro lado, a Google DeepMind apresentou o AlphaProof Code, que associa peritos humanos a agentes de IA para verificar formalmente software, ou seja, demonstrar matematicamente que este cumpre requisitos definidos. A equipa aplicou-o ao libsignal, a implementação de referência do protocolo Signal. Versões deste protocolo funcionam também no WhatsApp e no Google Messages.
Humanos trabalharam com agentes executados no Carbon e no Claude Opus 5.5 para redigir as especificações que descreviam o que precisava de ser provado. Agentes baseados no Carbon geraram depois a totalidade das cerca de 6,5 milhões de linhas de provas escritas em Lean, um assistente de provas que rejeita as inválidas. Segundo a Google, as garantias provadas, incluindo o sigilo persistente (forward secrecy), a segurança após compromisso e a autenticação, valem para o código máquina compilado, enquanto a maioria das verificações de protocolos incide apenas na conceção.
Cinco investigadores realizaram o trabalho de prova em quatro semanas, um trabalho que a Google estima tradicionalmente reservado a especialistas durante anos. Para verificar que o método deteta falhas reais, a equipa reintroduziu dois bugs antigos do libsignal, já corrigidos, e provou que essas versões não cumprem mais as garantias de segurança.
Os resultados referem-se à versão do código compilada pela Google, executada através de uma pequena ferramenta de linha de comandos, e não às «próprias aplicações do Signal». Alguns canais auxiliares foram também excluídos de partes da análise. «Os resultados sugerem que a IA pode tornar a verificação formal, historicamente demasiado dispendiosa para a maioria do software, praticável para sistemas reais», escrevem os investigadores. Ehren Kret, diretor técnico do Signal, declarou por sua vez: «À medida que as ameaças de segurança ligadas à IA se multiplicam, a verificação rigorosa da implementação do protocolo Signal dá-nos ainda mais confiança nas garantias de confidencialidade do nosso código.» A Google publica ainda as especificações e as provas.
