Google ha ampliado el acceso a Gemini 4 Carbon e indica que agentes construidos sobre este modelo han contribuido a verificar formalmente garantías de seguridad centrales del código del protocolo Signal.
Los desarrolladores y empresas que pagan ya pueden usar Carbon a través de la API Gemini y Gemini for business, y los suscriptores de Google AI Ultra también tienen acceso. Se aplican tarifas de introducción de 2 $ y 10 $ por millón de tokens en entrada y salida hasta el 30 de noviembre, antes de duplicarse. Un token es una unidad de texto que el modelo procesa para leer o producir contenido.
Hasta ahora, solo algunos defensores de ciberseguridad miembros del programa Fairwind de Google podían usar Carbon. Siguen teniendo que pertenecer a este programa para acceder a Carbon for cyber, una versión que Google presenta como líder en los principales benchmarks de detección, explotación y corrección de vulnerabilidades.
Aplicaciones en ciberseguridad
Según Google, la empresa Wiz utilizó Carbon for cyber para encontrar fallas de tipo «zero-day» en dos grandes proveedores de SaaS, en dos horas. Por su parte, el equipo Cloud Vulnerability Research (CVR) de Google utilizó el modelo para confirmar que dos errores en un proyecto de código abierto popular eran explotables, con una gravedad comparable a la de PHP2Shell, un par de fallas PHP ya explotadas por atacantes.
«Al usar Carbon para construir una prueba de concepto, CVR ayudó a los mantenedores a reclasificar el error como crítico y a publicar rápidamente un parche», indica Google.
Verificar el código de Signal
Por otra parte, Google DeepMind ha presentado AlphaProof Code, que combina expertos humanos con agentes de IA para verificar formalmente software, es decir, demostrar matemáticamente que cumplen con requisitos definidos. El equipo lo aplicó a libsignal, la implementación de referencia del protocolo Signal. Versiones de este protocolo también funcionan en WhatsApp y Google Messages.
Humanos trabajaron con agentes ejecutados en Carbon y en Claude Opus 5.5 para redactar las especificaciones que describían lo que debía probarse. Luego, agentes basados en Carbon generaron la totalidad de las aproximadamente 6,5 millones de líneas de pruebas escritas en Lean, un asistente de pruebas que rechaza las inválidas. Según Google, las garantías probadas, que incluyen el secreto persistente (forward secrecy), la seguridad tras compromiso y la autenticación, son válidas para el código máquina compilado, mientras que la mayoría de las verificaciones de protocolos se centran solo en el diseño.
Cinco investigadores realizaron el trabajo de prueba en cuatro semanas, un trabajo que Google estima tradicionalmente reservado a especialistas durante años. Para verificar que el método detecta fallas reales, el equipo reintrodujo dos errores antiguos de libsignal, ya corregidos, y probó que esas versiones ya no cumplen las garantías de seguridad.
Los resultados se refieren a la versión del código compilada por Google, ejecutada mediante una pequeña herramienta de línea de comandos, y no a «las aplicaciones de Signal en sí». Algunos canales auxiliares también fueron excluidos de partes del análisis. «Los resultados sugieren que la IA puede hacer que la verificación formal, históricamente demasiado costosa para la mayoría del software, sea práctica para sistemas reales», escriben los investigadores. Ehren Kret, director técnico de Signal, declaró por su parte: «Mientras las amenazas de seguridad relacionadas con la IA se multiplican, la verificación rigurosa de la implementación del protocolo Signal nos da aún más confianza en las garantías de privacidad de nuestro código». Google publica además las especificaciones y las pruebas.
