DeepMind verificó en un mes parte del código criptográfico de Signal con ayuda de la IA

Las pruebas pasan, la revisión de código no detecta problemas y, aun así, sigue faltando confianza en el código crítico. En criptografía, esto resulta especialmente preocupante: una combinación poco frecuente de condiciones puede importar más que mil ejecuciones de prueba satisfactorias. Según ZDNET, Google DeepMind aplicó AlphaProof Code a parte del código criptográfico de Signal y completó la verificación en un mes. El interés práctico reside en el intento de reducir el trabajo manual necesario para construir demostraciones matemáticas.

Conviene delimitar el alcance del resultado desde el principio: la publicación no permite concluir que los investigadores hayan demostrado la seguridad de toda la aplicación de mensajería. El trabajo se refiere a partes concretas de la implementación y a las propiedades que el equipo decidió verificar. Para un desarrollador, la diferencia es fundamental: una demostración responde a una pregunta concreta sobre un programa, pero no otorga un certificado universal de fiabilidad.

Qué se comprueba matemáticamente

Imaginemos una función que actualiza el estado criptográfico después de procesar un mensaje. Una prueba convencional le proporciona unos datos elegidos y compara el resultado con el esperado. Se pueden añadir entradas aleatorias, valores límite y largas secuencias de llamadas. Pero cada ejecución sigue comprobando un escenario concreto.

En la verificación formal, primero se formula un requisito preciso sobre el comportamiento de la función. Después se demuestra que el código lo cumple en todos los casos contemplados por el modelo establecido. Un ejemplo hipotético: una operación debe preservar una determinada relación entre el estado anterior y el nuevo. Esto ilustra el método; no describe una propiedad concreta demostrada por el equipo de DeepMind.

La parte más costosa de este trabajo suele empezar antes de la propia demostración. Hay que decidir qué promete exactamente el programa, qué supuestos son admisibles y dónde termina el ámbito que se va a verificar. Si el requisito es incorrecto o incompleto, ni siquiera una demostración válida responderá a la verdadera pregunta sobre la seguridad del producto.

Cómo se repartió el trabajo entre personas y agentes

Según el relato de ZDNET, los investigadores se apoyaron en trabajos anteriores de Signal Foundation. Las personas, junto con los agentes, determinaron qué afirmaciones había que demostrar. Después, varios agentes construyeron las demostraciones; por separado, el sistema ayudó a comprobar los resultados y señaló las áreas que requerían atención humana.

El medio informa de que se marcó alrededor del 1% de la base de código para una nueva revisión manual. Esta cifra debe interpretarse con cautela: el texto no aclara cómo se definió el denominador ni qué se consideró exactamente una sección verificada. No significa que la IA confirmara por sí sola la seguridad del 99% restante de toda la aplicación Signal.

Otro de los resultados comunicados fue el trabajo con dos errores de Signal que ya se habían corregido. Estas comprobaciones son útiles: una herramienta debe distinguir una implementación correcta de otra defectuosa. Sin embargo, un relato breve no basta para reconstruir el experimento, entender sus condiciones y evaluar qué clases de errores puede detectar realmente el sistema.

El plazo de un mes también necesita contexto. ZDNET lo compara con un trabajo que podría haber llevado años a los expertos, pero no aporta un proyecto comparable, los costes de cómputo ni un desglose detallado del trabajo humano. Por tanto, aún es pronto para prometer a otros equipos una aceleración similar.

Qué pueden hacer los desarrolladores y los responsables de producto

Si el enfoque se valida con materiales accesibles, resultará especialmente interesante para módulos pequeños en los que los errores salen caros y los requisitos pueden formularse con precisión. Se puede empezar por una sola función y describir sus entradas válidas, las propiedades esperadas y sus dependencias. Así será más fácil determinar si hay un problema que abordar mediante verificación formal y qué resultado podrá aceptar el equipo.

A los responsables de producto les conviene definir de antemano los límites de lo que se promete al usuario. Una propiedad demostrada de un módulo criptográfico no dice nada automáticamente sobre la protección del dispositivo, la interfaz, las copias de seguridad o la corrección de las actualizaciones. Estas cuestiones requieren sus propias comprobaciones.

Según la publicación, DeepMind tiene previsto publicar el código de AlphaProof Code como código abierto. Para evaluar la idoneidad de la herramienta harán falta el propio repositorio, las especificaciones, las demostraciones comprobables y una descripción de sus limitaciones. Por ahora, es un ejemplo sustancial de la aplicación de la IA a un problema de ingeniería: los agentes pueden ayudar a preparar demostraciones, pero la calidad de los requisitos y el alcance del resultado siguen siendo responsabilidad de las personas.