Escuchar este artículo
Preparando audio…
¿Por qué importa?
Google DeepMind presentó AlphaProof Code, un sistema que combina expertos y agentes de inteligencia artificial para verificar propiedades de seguridad en el código del protocolo de mensajería Signal.
El desarrollo afecta a los usuarios de la aplicación al buscar reducir la distancia entre la seguridad prevista en el diseño de un protocolo y su implementación real. Sin embargo, la investigación no certifica toda una aplicación ni su sistema operativo, por lo que queda por definir el alcance práctico total de estas pruebas en los dispositivos.
Síntesis generada con IA.
Google DeepMind presentó el 10 de noviembre AlphaProof Code, un sistema que combina especialistas humanos y agentes de inteligencia artificial para demostrar matemáticamente propiedades de seguridad del código utilizado por el protocolo de mensajería Signal.
Según el anuncio de la compañía, el trabajo lleva la verificación hasta el código que ejecuta el dispositivo. El objetivo es reducir la distancia entre la seguridad prevista en el diseño de un protocolo y su implementación real.
Qué verificaron los investigadores
El estudio técnico se centra en libsignal, la implementación de referencia del protocolo. Abarca el mecanismo de establecimiento de conexión PQXDH y Triple Ratchet, componentes destinados a proteger las conversaciones, incluso ante determinados escenarios de compromiso de claves.
Los agentes generaron cerca de 6,5 millones de líneas de demostraciones en Lean, un lenguaje y verificador matemático. Las pruebas se aceptan únicamente cuando el núcleo de Lean confirma que satisfacen las especificaciones aprobadas.
La intervención humana sigue siendo decisiva
Los especialistas participan en la definición y revisión de lo que debe demostrarse. La confianza del resultado depende también de esas especificaciones y de los componentes que el estudio considera fiables.
Por ello, el alcance de las pruebas debe leerse con precisión: demostrar propiedades concretas de libsignal no equivale a certificar toda una aplicación, su sistema operativo o el uso que haga cada persona de su teléfono.
La investigación apunta a una aplicación empresarial de la IA distinta de la generación de contenido: ayudar a revisar software cuya seguridad exige un nivel de comprobación especialmente alto.
El anuncio y el estudio técnico de los investigadores permiten consultar el alcance del trabajo. Google DeepMind describe el sistema y el papel de los expertos.