Natural Language based Specification and Verification

Resumen Técnico: Especificación y Verificación Basadas en Lenguaje Natural (NLForge)

Enunciado del Problema
Las violaciones de seguridad de memoria en programas C y C++ —tales como desreferencias inválidas, uso después de liberación y acceso fuera de límites— siguen siendo una fuente principal de vulnerabilidades de software. Estos errores suelen derivar de interacciones interprocedimentales complejas que involucran asignación, liberación, inicialización y aliasing, las cuales las herramientas tradicionales de análisis estático tienen dificultades para verificar a gran escala. Aunque los Modelos de Lenguaje Grandes (LLM) han demostrado capacidades sólidas para identificar errores, enfrentan desafíos significativos en prevenir la introducción de nuevas vulnerabilidades mediante verificación formal. Las pipelines de verificación existentes suelen requerir especificaciones en lenguajes formales rígidos (por ejemplo, invariantes de bucle, precondiciones/postcondiciones), lo que genera una alta carga de anotación. Los intentos previos de utilizar LLM para sintetizar estas especificaciones formales han mostrado un éxito limitado. Además, las evaluaciones recientes indican que el rendimiento de los LLM disminuye precipitadamente al pasar de la verificación de una sola función al razonamiento composicional y multifuncional, debido en gran medida a las limitaciones de la ventana de contexto y a la dificultad de mantener la consistencia semántica global.

Metodología: NLForge
Los autores proponen NLForge, un marco de verificación composicional que aprovecha los LLM para generar y razonar sobre especificaciones en lenguaje natural en lugar de artefactos formales rígidos. El sistema opera mediante un análisis ascendente, priorizando a los llamados (callee-first) sobre el gráfico de llamadas del programa.

1. Arquitectura de la Pipeline:

   • Preprocesamiento: El sistema extrae definiciones de funciones, firmas y sitios de llamada del código C/C++ para construir un gráfico de llamadas. Las llamadas no resueltas se gestionan mediante stubs externos.
   • Análisis Ascendente: El marco realiza una secuencia de pasadas de análisis sobre el gráfico de llamadas en orden topológico (procesando a los llamados antes que a los llamadores).
   • Resúmenes en Lenguaje Natural: En lugar de generar lógica formal, el LLM produce resúmenes estructurados en lenguaje natural (codificados como JSON tipado con descripciones en lenguaje natural) para propiedades específicas:
     • Asignación/Liberación/Inicialización: Resumen de la creación de objetos en el heap, efectos de la liberación y la inicialización de parámetros de salida.
     • Contratos de Seguridad de Memoria: Inferencia de precondiciones (por ejemplo, no nulo, no liberado, tamaño del búfer) y postcondiciones.
     • Resúmenes de Fugas y Enteros: Seguimiento de obligaciones no resueltas y riesgos de desbordamiento de enteros.
   • Verificación Composicional: En la pasada final de verificación, el LLM analiza una función utilizando sus propias precondiciones inferidas y los resúmenes en lenguaje natural de sus llamados. El modelo actúa como un agente de razonamiento que mantiene un estado de ejecución latente, verificando los requisitos de seguridad contra los contratos de los llamados sin integrar (inline) la implementación completa del llamado.

2. Racional de Diseño:
   Este enfoque se motiva por la observación de que los LLM, entrenados en código y documentación, pueden generar, interpretar y refinar resúmenes en lenguaje natural de manera más consistente que notaciones formales rígidas. Este diseño busca descomponer el problema de verificación en resúmenes semánticos reutilizables, permitiendo que el modelo razone sobre una función bajo suposiciones explícitas sobre sus llamados, en lugar de reanalizar el código fuente crudo para cada llamador.

Contribuciones Clave

• Marco Composicional: Un marco de verificación interprocedimental ascendente para C/C++ que utiliza LLM para inferir y verificar propiedades de seguridad de memoria.
• Representación Intermedia en Lenguaje Natural: La introducción de resúmenes semánticos en lenguaje natural como representación intermedia para la verificación, en contraste con trabajos previos que se centran en generar especificaciones formales para verificadores simbólicos externos.
• Pipeline de Análisis Escalonado: Una descomposición del razonamiento sobre seguridad de memoria en resúmenes reutilizables (asignación, liberación, inicialización y obligaciones del lado del llamador) que se retroalimentan al LLM en etapas posteriores.
• Evaluación Empírica: Un estudio comparativo del razonamiento composicional frente a una línea base de indicación de programa completo no composicional en las evaluaciones SV-COMP 2026.

Resultados
Los autores evaluaron NLForge en un subconjunto de las evaluaciones de seguridad de memoria SV-COMP 2026 utilizando cuatro núcleos de LLM (Claude Sonnet-4.6, GPT-5.4, Gemini-3.1-flash-lite y Qwen3.5-27B-UD-Q4) y los compararon con verificadores tradicionales (CPAchecker, Symbiotic, Ultimate Automizer).

• RQ1 (LLM como Verificadores): El análisis basado en LLM demuestra una alta recuperación (recall) y cobertura, identificando la mayoría de los verdaderos positivos (por ejemplo, Sonnet-4.6 alcanzó un 99,8% de recuperación en valid-memsafety). Sin embargo, producen significativamente más falsos positivos que las herramientas tradicionales y aún no pueden servir como verificadores independientes y sound. Las herramientas tradicionales a menudo devuelven "Desconocido" (UNK) para casos difíciles para evitar falsos positivos, mientras que los LLM proporcionan respuestas definitivas con tasas de error más altas.
• RQ2 (Verificación Composicional): El enfoque composicional supera significativamente a la línea base no composicional, particularmente en evaluaciones complejas del mundo real de flujo de control y estructuras de datos.
  • Las ejecuciones composicionales aumentaron los Verdaderos Positivos de 3.390 a 3.476 y redujeron los Falsos Negativos de 301 a 216 en todos los modelos.
  • La mejora fue más pronunciada para modelos más pequeños (por ejemplo, Qwen3.5-27B-Q4 vio caer los Falsos Negativos de 218 a 97) y en evaluaciones que requieren un fuerte razonamiento interprocedimental.
  • Las ganancias fueron menos consistentes en las pruebas sintéticas y localizadas de Juliet, donde los modelos no composicionales podían explotar patrones locales directamente.

Significado y Afirmaciones
El artículo aboga por un cambio en la forma en que se utilizan los LLM en la verificación: pasar de tratarlos únicamente como generadores de artefactos formales para motores externos a utilizarlos como agentes de razonamiento sobre resúmenes estructurados y reutilizables en lenguaje natural.

• Practicidad: El lenguaje natural sirve como una capa de especificación intermedia práctica que habilita la verificación composicional, especialmente para tareas donde la indicación de programa completo excede el presupuesto de razonamiento del modelo o la ventana de contexto.
• Limitaciones: Los autores reconocen que la informalidad del lenguaje natural conduce a problemas de calibración (mayores falsos positivos) y que el enfoque es sensible a la calidad de los resúmenes generados; los errores en los resúmenes pueden propagarse y amplificarse.
• Perspectiva Futura: El trabajo sugiere que, aunque los LLM aún no son un reemplazo para la verificación formal sound, ofrecen una dirección prometedora para la verificación de detección de errores escalable. El trabajo futuro debería centrarse en mejorar la calibración, combinar resúmenes con verificaciones simbólicas y manejar características complejas como llamadas indirectas e invariantes de heap de manera más robusta.

El estudio concluye que la pregunta no es meramente si los LLM pueden verificar la seguridad de la memoria, sino bajo qué representaciones y descomposiciones se vuelven más confiables, destacando que el lenguaje natural puede cerrar eficazmente la brecha entre la estructura modular del programa y las capacidades de razonamiento de los LLM.