💻 ciencias de la computación

State-inferer: LLM-Driven State Machine Extraction and Formal Verification for Secure Protocol Implementations

Este artículo presenta State-inferer, un marco de trabajo de caja blanca que integra el segmentado de programas (program slicing), modelos de lenguaje de gran escala y verificación de modelos formales para extraer y verificar con precisión las máquinas de estado de protocolos a partir del código fuente, logrando una precisión superior a nivel de transición y descubriendo cuatro vulnerabilidades de seguridad previamente desconocidas en implementaciones de TLS, IKEv2 y SSH.

Autores originales: MengCheng Ju, Xi Chen, XieLi Zhang, Mingliang Zhu, Guanping Zhang, Dongliang Zhao, ChunXiang Gu

Publicado 2026-11-09

📖 7 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: MengCheng Ju, Xi Chen, XieLi Zhang, Mingliang Zhu, Guanping Zhang, Dongliang Zhao, ChunXiang Gu

Artículo original bajo licencia CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

La seguridad del mundo digital depende en gran medida de las reglas invisibles que gobiernan cómo las computadoras se comunican entre sí. Estas reglas, conocidas como protocolos de red, están diseñadas para asegurar que los datos viajen de forma segura desde un emisor hasta un receptor, verificando identidades y manteniendo secretos. En su esencia, estos protocolos funcionan como un guion estricto: una computadora debe estar en una condición específica, recibir un mensaje específico y luego pasar a una nueva condición antes de poder proceder. Si una computadora se salta un paso o acepta un mensaje mientras está en la condición incorrecta, todo el sistema puede verse comprometido, permitiendo que los atacantes eludan los controles de seguridad o roben información sensible. Durante décadas, los expertos en seguridad han intentado verificar que el código real que se ejecuta en los servidores siga este guion perfectamente. Sin embargo, el código suele ser desordenado, lleno de variables ocultas y una lógica compleja que las herramientas de prueba estándar luchan por mapear. Cuando el comportamiento real de un programa diverge de su diseño escrito, fallos peligrosos pueden esconderse a plena vista, esperando ser explotados.

Un equipo de investigadores de la Universidad de Ingeniería de Información de la PLA ha desarrollado un nuevo método para resolver este problema, creando una herramienta llamada State-inferer que actúa como un traductor entre el complejo código de la computadora y las reglas lógicas que se supone debe seguir. En lugar de intentar leer todo el código base a la vez o adivinar cómo se comporta un programa enviándole mensajes aleatorios, esta herramienta descompone el código en piezas diminutas y manejables. Utiliza una técnica llamada segmentación de programas (program slicing) para rastrear exactamente cómo cambia una pieza específica de datos a medida que se mueve a través del software, aislando la lógica precisa que causa que una computadora cambie de estado. Este proceso es como rastrear un solo hilo a través de una bola de lana enredada para ver exactamente hacia dónde conduce, ignorando el resto del desorden. Al enfocarse en estos hilos específicos, el sistema puede reconstruir la secuencia exacta de eventos que sigue un programa, incluyendo las condiciones internas ocultas que las herramientas estándar suelen pasar por alto.

Los investigadores luego alimentaron estas secuencias reconstruidas en un modelo de lenguaje de gran tamaño, un tipo de inteligencia artificial entrenada para comprender y razonar sobre el código. A diferencia de los intentos anteriores que simplemente pedían a la IA que leyera grandes fragmentos de texto, este sistema proporcionó a la IA un fragmento de código pequeño y enfocado para cada una de las transiciones del protocolo. Esto permitió que la IA viera el contexto completo de un cambio de estado sin verse abrumada por información irrelevante. La IA construyó entonces un mapa completo del comportamiento del programa, anotando no solo qué mensajes activaron un cambio, sino también las variables internas que debían ser ciertas para que ese cambio ocurriera. Finalmente, los investigadores utilizaron un motor de verificación formal para cotejar este mapa con las reglas de seguridad oficiales. Este motor actúa como un auditor riguroso, probando sistemáticamente cada posible ruta que el programa podría tomar para ver si alguna vez viola las reglas, como enviar datos antes de que se establezca completamente una conexión segura.

Cuando se probó en siete implementaciones de código abierto de los principales protocolos de seguridad, incluidos TLS, IKEv2 y SSH, el nuevo método demostró ser notablemente preciso. Identificó correctamente el comportamiento del código con una precisión del 95.2 por ciento, superando significativamente a las mejores herramientas existentes, que lograron solo alrededor del 78.9 por ciento. La diferencia no fue solo una cuestión de errores menores; la nueva herramienta capturó con éxito la lógica interna compleja que otros métodos omitieron por completo, como transiciones impulsadas por temporizadores internos o verificaciones de recursos en lugar de mensajes externos. De hecho, los investigadores descubrieron que los métodos antiguos a menudo no veían casi la mitad de las transiciones críticas porque dependían de una visión simplificada del programa que ignoraba estos detalles internos. Al capturar el panorama completo, la nueva herramienta pudo descubrir cuatro vulnerabilidades previamente desconocidas en el software. Estos fallos, que nunca habían sido descubiertos antes, eran lo suficientemente graves como para recibir identificadores de seguridad oficiales y ser reportados a los mantenedores del software para su corrección.

Uno de los hallazgos más significativos fue que los fallos no eran solo posibilidades teóricas, sino debilidades reales y explotables. En un caso, la herramienta descubrió que un servidor podía ser engañado para aceptar un mensaje de seguridad crítico antes de haber terminado el intercambio de claves necesario, eludiendo efectivamente la autenticación. En otro caso, una verificación ausente permitió que un servidor procesara un flujo interminable de mensajes, agotando potencialmente sus recursos. Estos descubrimientos resaltan una brecha crítica en cómo se analiza el software actualmente: mirar solo la entrada y la salida no es suficiente para entender cómo funciona realmente un programa. Los investigadores demostraron que, al combinar el análisis de código preciso con el poder de razonamiento de la inteligencia artificial, es posible construir un modelo completo y preciso de la lógica interna de un programa. Este enfoque no requiere que el software sea modificado ni que los investigadores rastreen manualmente cada línea de código, lo que lo convierte en una forma escalable de auditar los complejos sistemas que protegen nuestra infraestructura digital.

El estudio también abordó las limitaciones de los enfoques previos que dependían de la recuperación de código basada en la similitud de texto. Esos métodos a menudo fallaban porque no podían conectar los puntos entre diferentes funciones que trabajaban juntas para cambiar el estado de un programa. El nuevo sistema, por el contrario, sigue el flujo real de datos y control, asegurando que el contexto proporcionado a la inteligencia artificial sea completo y conectado. Esto permitió que el sistema generara verificaciones de seguridad que estaban adaptadas específicamente a las variables y la lógica de cada implementación única, en lugar de aplicar una plantilla genérica que podría no dar en el blanco. El resultado es un marco que puede adaptarse a las peculiaridades de diferentes estilos de codificación y, aun así, producir un modelo fiable del comportamiento del sistema.

En última instancia, este trabajo representa un cambio en cómo abordamos la seguridad del software. Nos alejamos de la idea de que debemos inspeccionar manualmente cada línea de código o depender de pruebas de caja negra que solo pueden ver la superficie. En su lugar, ofrece una forma de ver dentro de la máquina, comprendiendo exactamente cómo piensa y reacciona. Los investigadores descubrieron que, al tratar el código como un conjunto de pasos lógicos que pueden ser segmentados, analizados y verificados, podían encontrar errores que habían estado escondidos durante años. Aunque la herramienta fue probada en proyectos de código abierto, el método sugiere un camino a seguir para asegurar la vasta gama de sistemas propietarios que ejecutan internet. La capacidad de extraer y verificar automáticamente las máquinas de estado de protocolos complejos significa que la seguridad puede verificarse de manera más exhaustiva y rápida que nunca, previniendo potencialmente los tipos de brechas que han plagado el mundo digital durante décadas. Los hallazgos confirman que la brecha entre lo que un protocolo debe hacer y lo que realmente hace es donde reside el peligro, y que cerrar esta brecha requiere una mirada más profunda y precisa al código mismo.

Resumen Técnico: State-inferer

Declaración del Problema

La seguridad de las implementaciones de protocolos de red depende de la corrección de las máquinas de estados finitos (FSM) realizadas por su código. Sin embargo, las implementaciones del mundo real a menudo se desvían de sus especificaciones RFC debido a requisitos mal interpretados o lógica específica del proveedor, lo que conduce a vulnerabilidades de la máquina de estados, como la elusión de la autenticación. Recuperar la FSM real a partir del código fuente es un desafío debido a tres limitaciones principales en los enfoques existentes:

Desalineación Semántica (C1): Los métodos existentes suelen construir máquinas de estados impulsadas por mensajes que abstraen los detalles internos de la implementación. Los estados reales de los protocolos dependen de variables internas (p. ej., banderas, contadores) y condiciones de flujo de control que, al ser ignoradas, resultan en modelos gruesos que no pueden expresar los comportamientos a nivel de implementación necesarios para la verificación.
Restricciones de Contexto (C2): Las bases de código de protocolos son demasiado grandes para las ventanas de contexto de los Modelos de Lenguaje Extensos (LLM) actuales. Los enfoques de Generación Aumentada por Recuperación (RAG) suelen depender de la similitud textual, lo cual falla al recuperar la cadena completa de llamadas entre funciones y archivos necesaria para entender una transición de estado como una unidad unificada. Esto provoca la pérdida de precondiciones y un análisis de alcanzabilidad incorrecto.
Especialización de Propiedades (C3): Las propiedades de seguridad de los RFC se declaran a un nivel semántico sin referencia a variables de implementación específicas. Traducir estas propiedades genéricas en fórmulas de Lógica Temporal Lineal (LTL) para la verificación de modelos requiere mapear conceptos abstractos a variables de código específicas, un paso que las herramientas existentes dejan a la intervención manual del analista.

Metodología: State-inferer

State-inferer es un marco de trabajo de caja blanca diseñado para extraer y verificar máquinas de estados de protocolos combinando el segmentado de programas (program slicing), LLMs y verificación de modelos. Su arquitectura consta de tres componentes principales:

1. Extractor de Código Relacionado (RCE)

Para abordar la restricción de contexto (C2) y evitar las alucinaciones por código irrelevante, el RCE no utiliza la recuperación basada en similitud. En su lugar, emplea segmentado de programas (program slicing) sobre el Grafo de Dependencia de Sistema (SDG).

Identificación de Variables de Estado: Se le solicita a un LLM que identifique las variables de estado clave y sus valores de enumeración a partir de los archivos de cabecera y de núcleo.
Segmentado de Profundidad Limitada: Partiendo de las asignaciones a las variables de estado, el sistema realiza búsquedas hacia adelante y hacia atrás en el SDG limitadas por la profundidad de flujo de datos ( $k_d$ ) y de flujo de control ( $k_c$ ). Esto extrae un fragmento de código compacto ("gadget") para cada transición de estado que abarca límites de funciones pero excluye código de bajo nivel no relacionado. Esto asegura que el LLM reciba la cadena de llamadas completa y las precondiciones para una transición.

2. Constructor de Modelo

Este componente transforma los fragmentos de código segmentados en un Sistema de Transición de Estados (STS) formal, $M = (V, S, s_0, \delta, A)$ .

Espacio de Estados ( $S$ ) y Estado Inicial ( $s_0$ ): El LLM extrae el espacio de estados discretos a partir de los tipos de enumeración e infiere las constantes del estado inicial basándose en las rutinas de arranque.
Función de Transición ( $\delta$ ) y Variables ( $V$ ): Para cada gadget de código, el LLM identifica los estados de origen y destino, extrae las condiciones de flujo de control y las traduce en expresiones booleanas formales. También recopila las variables internas involucradas.
Conjunto de Acciones ( $A$ ): Las transiciones se etiquetan con acciones externas (p. ej., recepción de mensajes) y acciones internas (p. ej., expiración de temporizador, derivación de claves).
Resultado: El resultado es un STS donde las transiciones portan guardas explícitas sobre las variables internas, abordando la desalineación semántica (C1).

3. Generador de Propiedades de Seguridad

Para resolver el problema de la especialización de propiedades (C3), este módulo convierte las meta-propiedades de los RFC en fórmulas LTL específicas de la implementación.

El LLM toma el STS extraído y una propiedad de seguridad del RFC como entrada.
Mapea los conceptos de seguridad abstractos a las variables de estado y predicados de transición específicos de la implementación concreta.
Genera la fórmula LTL correspondiente adaptada a la base de código.

4. Verificación

El STS extraído y las propiedades LTL se traducen al lenguaje SMV y se verifican utilizando nuXmv. Si una propiedad se viola, nuXmv genera un rastro de contraejemplo, el cual es revisado manualmente para identificar vulnerabilidades.

Contribuciones Clave

Construcción de Contexto Basada en Segmentado: Un método para recuperar transiciones de estado de protocolos mediante la realización de búsquedas hacia adelante y hacia atrás de profundidad limitada en el SDG. Esto extrae un fragmento de código compacto por cada transición, asegurando que el LLM vea la lógica completa entre funciones en lugar de fragmentos aislados.
Sistema de Transición de Estados con Guardas: Un flujo de trabajo que construye un STS a nivel de implementación donde las transiciones portan guardas sobre variables internas, permitiendo el modelado de comportamientos que dependen de configuraciones internas en lugar de solo mensajes externos.
Especialización de Propiedades Consciente del Modelo: Un enfoque automatizado para especializar las propiedades de seguridad de los RFC en fórmulas LTL sobre el modelo extraído, cerrando la brecha entre la semántica de la especificación y las variables de la implementación.
Evaluación Empírica: Una evaluación exhaustiva en siete implementaciones de código abierto de TLS, IKEv2 y SSH, demostrando una alta precisión en la recuperación de transiciones y el descubrimiento de vulnerabilidades previamente desconocidas.

Resultados

El marco fue evaluado en siete implementaciones (OpenSSL, WolfSSL, TLSE, strongSwan, Libreswan, OpenSSH, tinySSH) contra un modelo de referencia construido por expertos en el dominio.

Precisión: State-inferer logró un F-score de nivel de transición estricto de macro-promedio del 95.2%. Esto superó significativamente al baseline más fuerte, ProtocolGPT (46.2%), y a los agentes de codificación de propósito general (Codex: 78.9%, Claude Code: 77.1%).
Poder de Representación: A diferencia de las representaciones tipo Mealy utilizadas por los baselines, el STS de State-inferer pudo expresar todas las transiciones de referencia. Los métodos de baseline perdieron aproximadamente el 22% de las transiciones debido a limitaciones de representación (p. ej., incapacidad para distinguir estados basados en guardas internas o eventos internos).
Descubrimiento de Vulnerabilidades: State-inferer descubrió cuatro vulnerabilidades previamente desconocidas en implementaciones no modificadas:
1. WolfSSL (CVE-2026-2645): Una elusión de autenticación en TLS 1.2 donde un mensaje CertificateVerify podría procesarse antes de la completitud del intercambio de claves.
2. TLSE (CNVD-2026-27960): Una confusión de versión de protocolo causada por extensiones de intercambio de claves vacías en TLS .13.
3. TLSE (CNVD-2026-27959): Procesamiento sin límites de mensajes ChangeCipherSpec debido a una variable de estado faltante.
4. TLSE (CNVD-2026-27957): Desincronización entre el manejo de alertas de TLS y el estado de la capa de transporte, permitiendo la transmisión de datos después de una notificación de cierre.
  Todos los hallazgos fueron divulgados de manera responsable y recibieron identificadores CVE o CNVD.

Significancia y Reivindicaciones

El artículo afirma que State-inferer aborda las limitaciones fundamentales de los métodos actuales de extracción de máquinas de estados integrando el análisis estático (segmentado) con las capacidades de razonamiento de los LLM. Al construir el contexto mediante el segmentado de dependencias en lugar de la recuperación textual, el marco asegura que el LLM reciba la lógica necesaria entre funciones para inferir con precisión las guardas de transición y la alcanzabilidad. Además, al automatizar la especialización de las propiedades de los RFC en fórmulas LTL, permite la verificación formal de propiedades de seguridad específicas de la implementación sin mapeo manual.

Los autores aseguran que su enfoque proporciona una representación más fiel del comportamiento a nivel de implementación en comparación con el aprendizaje de caja negra o el modelado basado en especificaciones, permitiendo directamente el descubrimiento de vulnerabilidades que dependen de las configuraciones de estado internas. El alto F-score y el descubrimiento exitoso de vulnerabilidades del mundo real demuestran la eficacia práctica de combinar el segmentado de programas, los LLM y la verificación de modelos para el análisis seguro de protocolos.