AlphaProof Code: la IA de Google verifica la seguridad de libsignal

Demostrar en lugar de probar

Las pruebas y auditorías pueden indicar que no se halló ningún fallo, pero no que no exista ninguno. La verificación formal, en cambio, demuestra matemáticamente, como un teorema, que el código no puede violar ciertas propiedades. Es un método muy costoso: la verificación del núcleo seL4, lograda en 2009, requirió el equivalente a veinte años de trabajo de una persona.

En este caso, expertos humanos definieron qué demostrar a partir de trabajos académicos sobre Signal. Los agentes, basados en Gemini 4 Carbon, escribieron cerca de 6,5 millones de líneas de demostración en el lenguaje Lean, cuyo verificador comprueba cada paso de forma automática. Según los investigadores, ninguno escribió personalmente una línea de prueba.

El objetivo principal era el «ratchet», el mecanismo que renueva continuamente las claves. Las pruebas establecen que un atacante que robe las claves almacenadas en un teléfono no podría leer los mensajes anteriores, porque cada clave deriva de la anterior y luego se borra. También muestran que la conversación vuelve a ser segura cuando ambos interlocutores intercambian mensajes nuevos y que nadie puede suplantar a ninguno. Para validar el método, reintrodujeron dos antiguos errores ya corregidos y el sistema demostró que esas versiones no ofrecían las garantías esperadas.

Límites claros

El director técnico de Signal, Ehren Kret, lo calificó de «un avance importante». Google advierte, no obstante, que la prueba solo cubre conversaciones entre dos personas, da por supuesto que los componentes criptográficos básicos funcionan sin verificarlos y se aplica a una versión de prueba en Linux, no a las apps móviles.

Los autores concluyen que, ahora que las pruebas son baratas, la pregunta difícil es qué demostrar.