Una IA verificó el cifrado de Signal en cuatro semanas, no en años
Google DeepMind dice haber verificado formalmente el cifrado de Signal —su núcleo criptográfico— en cuatro semanas, un trabajo que normalmente toma años de especialistas. Lo hizo con AlphaProof Code, un sistema de agentes que escribió más de seis millones de líneas de pruebas matemáticas.
Si el resultado se sostiene, es una de las aplicaciones más concretas y menos ruidosas que hemos visto de esta tecnología.
Qué se verificó del cifrado de Signal
La verificación formal es demostrar matemáticamente que un programa hace lo que dice y nada más. No es probarlo mucho: es probar que no existe ninguna entrada posible que lo rompa. Por eso se usa en aviónica, en reactores y en criptografía, y por eso es tan cara: la escriben a mano especialistas, y tarda años.
Lo relevante de este caso es el alcance. Los intentos anteriores con Signal se habían quedado en el diseño teórico del protocolo. Según el reporte, aquí se verificó el código que realmente corre en los dispositivos.
Las cifras:
- Más de 6 millones de líneas de prueba escritas en Lean, el lenguaje de demostración formal.
- Cuatro semanas de trabajo.
- Agentes basados en un modelo de la familia Gemini.
- Cerca del 1 % del código quedó marcado para revisión humana.
Y un detalle de control que vale más que los millones de líneas: los investigadores plantaron dos errores a propósito y el sistema los detectó de inmediato.
Una precisión de fuentes: las coberturas no coinciden en el nombre exacto del modelo —aparece como «Gemini Carbon» y como «Gemini 4 Carbon»— y solo algunas afirman que la verificación bajó hasta el código máquina Arm. Nos quedamos con lo que coincide en todas las coberturas sobre el cifrado de Signal.
Lo que no significa
Conviene marcar el límite, porque es donde se va a exagerar.
Que el cifrado de Signal esté verificado no quiere decir que Signal sea inviolable. Una prueba formal garantiza que el código cumple unos requisitos de seguridad definidos de antemano. Si esos requisitos se escribieron mal, o si el ataque viene por un lado que nadie modeló —el teléfono comprometido, la copia de seguridad, la persona del otro lado de la conversación—, la prueba no dice nada al respecto.
Tampoco desaparece el trabajo humano. Los expertos definieron primero los requisitos formales; los agentes escribieron las demostraciones después. El cuello de botella se movió, no se eliminó.
Por qué verificar el cifrado de Signal cambia algo
La verificación formal era un lujo. Costaba tanto que solo se la podían pagar la industria aeroespacial, la militar y un puñado de proyectos críticos. Todo lo demás —el software de un banco, el de una EPS, el de una entidad pública— se audita a punta de pruebas y revisión manual, que encuentran errores pero nunca demuestran su ausencia.
Si el costo de verificar baja de años a semanas, la pregunta deja de ser técnica y pasa a ser presupuestal. Y eso llega a lugares donde hoy ni se plantea.
Google dice que quiere extender el método a infraestructura crítica como redes eléctricas y dispositivos médicos. Es exactamente el tipo de sistema que en Colombia se audita poco y se parchea tarde.
Para un equipo técnico de acá hay una lectura práctica más inmediata: si tu sistema maneja algo donde un error es caro —pagos, salud, identidad— vale la pena saber que la verificación formal dejó de ser inalcanzable. Todavía no es un botón, pero ya no es ciencia ficción presupuestal.
Lee también:
OpenAI dice que su IA resolvió tres problemas abiertos
EE.UU. acusa a seis empresas chinas de destilar sus modelos
Sitios oficiales:
Google DeepMind ·
Signal ·
Lean
Reportado por: Ars Technica — The Decoder
