Resumen Técnico: Veritas

Enunciado del Problema

Detectar vulnerabilidades de corrupción de memoria (MCV) en binarios despojados presenta un desafío fundamental de reconstrucción semántica. A diferencia del análisis de código fuente, el análisis de binarios debe recuperar cómo se asignan, propagan, restringen y acceden los objetos de memoria a través de funciones, a partir de artefactos que han perdido la estructura de alto nivel, los límites de los objetos y el flujo de control explícito debido a la compilación y el despojo.

Los enfoques recientes basados en Modelos de Lenguaje Grande (LLM) han mejorado la comprensión del código, pero luchan con la detección de MCV en binarios por tres razones principales:

1. Rastreo de Estado Compartido: Las vulnerabilidades a menudo surgen de suposiciones inconsistentes sobre regiones de memoria compartidas a través de funciones disjuntas que carecen de aristas directas en la cadena de llamadas. La expansión estándar de la gráfica de llamadas falla al capturar estas dependencias.
2. Pérdida Semántica: Las representaciones recuperadas están fragmentadas. El IR de LLVM elevado preserva los patrones de acceso a memoria de bajo nivel, pero está oscurecido por artefactos del compilador (variables SSA, conversiones de tipo), mientras que el C descompilado proporciona una estructura de alto nivel pero colapsa las operaciones de memoria en expresiones de desplazamiento genéricas, borrando la identidad del objeto.
3. Verificación de Restricciones: El análisis estático a menudo no puede determinar si un acceso sospechoso es alcanzable bajo condiciones de camino factibles. Sin evidencia ejecutable, los LLM dependen de proxies sintácticos en lugar de la prueba de cómo los datos controlados por el atacante se propagan hacia operaciones sensibles a la memoria, lo que conduce a un razonamiento frágil y altas tasas de falsos positivos.

Los marcos de trabajo de agentes existentes diseñados para código fuente (que dependen de la resumen o la expansión de la gráfica de llamadas) no resuelven el problema de recuperación semántica planteado por los binarios despojados, donde la estructura semántica requerida está parcialmente ausente por construcción.

Metodología

Veritas es un marco de trabajo de agentes híbrido y semánticamente fundamentado diseñado para restringir el razonamiento de los LLM a la semántica del programa verificable y al comportamiento ejecutable. Organiza el análisis en tres etapas alineadas con dos capas de fundamentación: Fundamentación Estática (hechos del programa recuperados) y Fundamentación en Tiempo de Ejecución (evidencia de ejecución concreta).

1. Cortador de Contexto Impulsado por Semántica (Fundamentación Estática)

El Cortador opera sin LLMs para extraer flujos de fuente a sumidero compactos y respaldados por testigos desde el IR de LLVM elevado.

• Gráfica de Propagación Interprocedimental: Eleva el binario a IR de LLVM utilizando RetDec y construye una gráfica de propagación interprocedimental tipada ($G_P$) que codifica dependencias de llamadas, retornos y globales. Esta gráfica rastrea cómo los valores relevantes para la taint (punteros, desplazamientos, longitudes) se propagan a través de las funciones.
• Extracción de Flujos Basada en Testigos: En lugar de tratar todos los pares fuente-sumidero alcanzables como significativos, el Cortador verifica testigos interprocedimentales acotados. Rastrea tokens taintados desde fuentes de entrada (por ejemplo, fread) hasta sumideros de riesgo de memoria (por ejemplo, argumentos de API peligrosos), validando la propagación en cada límite de función utilizando cadenas de definición-uso y metadatos.
• Construcción de Objetos de Flujo: Los testigos aceptados se convierten en objetos de flujo compactos que contienen funciones ordenadas, tokens relevantes para la taint y "pistas de anclaje" (clases de procedencia y anotaciones de punto final). Esto reemplaza el binario completo con un contexto pequeño y semánticamente completo para el análisis posterior.

2. Detector de Vulnerabilidades de Doble Vista (Razonamiento Controlado de LLM)

El Detector realiza un razonamiento paso a paso sobre los flujos respaldados por testigos, utilizando una representación de entrada de doble vista para superar la pérdida semántica.

• Representación de Doble Vista: Para las funciones fuente y sumidero, el LLM recibe tanto el código C descompilado (para el razonamiento del flujo de control) como el IR de LLVM elevado (para desambiguar las operaciones de memoria y la semántica del sumidero). Para las funciones intermedias, utiliza principalmente el código descompilado, guiado por las pistas de anclaje.
• Razonamiento Paso a Paso: El LLM analiza el flujo una función a la vez, manteniendo un estado de razonamiento acumulado (inventario de valores propagados, alias y límites). Actualiza este estado basándose en asignaciones y decisiones de flujo de control, evitando los límites de contexto de procesar todo el flujo de una vez.
• Memorización Basada en Trie: Para reducir la redundancia, el sistema memoriza los estados de razonamiento para los prefijos de flujo compartidos, invocando al LLM solo en el sufijo único de un flujo.
• Verificación de Consistencia: Antes de informar un candidato, el Detector realiza una verificación final sensible al camino para asegurar que el valor taintado permanezca relevante para la vulnerabilidad y que el acceso al sumidero viole la seguridad de la memoria bajo condiciones factibles.

3. Validador Automático de Vulnerabilidades (Fundamentación en Tiempo de Ejecución)

El Validador traduce las hipótesis del detector en comprobaciones ejecutables para confirmar o refutar candidatos.

• Preparación de Artefactos: Mapea las hipótesis del detector a coordenadas ejecutables (RVAs, símbolos) utilizando Radare2, cerrando la brecha entre las vistas del descompilador y la depuración en tiempo de ejecución.
• Colaboración de Múltiples Agentes: Tres agentes orquestan la validación:
  • Estratega: Planifica la validación, seleccionando objetivos de instrumentación, puntos de interrupción y modalidades de activación (archivo, red, CLI).
  • Verificador: Ejecuta el plan, generando Pruebas de Concepto (PoC) y ejecutando el binario bajo depuradores (Radare2) o verificadores de memoria (Valgrind) para observar caídas o accesos inválidos.
  • Explorador: Si la evidencia inicial es insuficiente, sondea estados alternativos o funciones relacionadas para encontrar evidencia de apoyo.
• Confirmación: Una vulnerabilidad se confirma solo cuando la evidencia concreta de tiempo de ejecución (por ejemplo, una violación de segmento, un error de Valgrind o un estado de memoria específico) corrobora el sumidero reportado, el patrón de acceso y la causa raíz.

Contribuciones Clave

1. Marco de Trabajo Veritas: Un marco de trabajo de agentes semánticamente fundamentado que unifica el análisis estático de programas y la validación en tiempo de ejecución para detectar corrupción de memoria en binarios despojados.
2. Arquitectura de Tres Etapas:
   • Un Cortador que extrae flujos respaldados por testigos desde IR elevado sin LLMs.
   • Un Detector de Doble Vista que razona sobre flujos utilizando soporte selectivo de IR para resolver ambigüedad semántica.
   • Un Validador que confirma hipótesis utilizando artefactos visibles para el depurador y ejecución concreta.
3. Benchmark de Alta Granularidad: Un conjunto de datos curado de 20 casos reales de corrupción de memoria en binarios con verdad fundamental a nivel de trazas, construido para evaluar la detección de binarios fundamentada.
4. Rendimiento: La evaluación muestra que Veritas logra un 90% de recuperación en el benchmark, superando significativamente a los analizadores estáticos (0% de recuperación), fuzzing (10% de recuperación) y líneas base de agentes (25–35% de recuperación). Produjo cero falsos positivos en una validación exhaustiva de 623 candidatos y solo 2 falsos positivos en una auditoría muestreada más grande.
5. Descubrimiento en el Mundo Real: Veritas descubrió una lectura fuera de límites de día cero previamente desconocida en la biblioteca Universal Scene Description de Apple (libusd_ms.dylib), la cual fue confirmada y asignada un CVE.

Resultados y Significancia

El artículo argumenta que la efectividad del descubrimiento de vulnerabilidades basado en LLM no depende únicamente de la capacidad intrínseca del modelo, sino de la capacidad de la infraestructura circundante para recuperar la estructura semántica requerida para el razonamiento.

• Fundamentación Semántica como Principio de Diseño: Los resultados apoyan la fundamentación semántica como un principio de diseño operativo. Al restringir el razonamiento de los LLM a hechos explícitos relevantes para la memoria (fundamentación estática) y validar las conclusiones contra el comportamiento ejecutable (fundamentación en tiempo de ejecución), Veritas evita la fragilidad de la especulación de modelos sin restricciones.
• Superioridad sobre Líneas Base: Las herramientas tradicionales fallan debido a la falta de fundamentación semántica a través de funciones. Las líneas base de agentes fallan porque carecen de modelos explícitos de los ciclos de vida de los objetos de memoria y dependen de exploración no guiada o patrones sintácticos. Veritas cierra esta brecha utilizando análisis determinista para precalcular la propagación y LLMs para interpretar semánticas complejas, seguido de una confirmación rigurosa en tiempo de ejecución.
• Compromiso Costo-Precisión: Aunque la validación en tiempo de ejecución es el principal cuello de botella de costos (requiriendo generación de PoC y depuración), el marco demuestra que una alta precisión es alcanzable en el análisis de binarios despojados solo a través de evidencia ejecutable. El sistema prioriza la fiabilidad de la detección sobre el rendimiento, un compromiso necesario para el análisis de binarios críticos para la seguridad.

El artículo concluye que para la detección práctica de vulnerabilidades en binarios, el razonamiento debe estar anclado tanto en la semántica del programa recuperada como en la evidencia ejecutable, un principio que Veritas implementa a través de su arquitectura híbrida y modular.