Resumen Técnico: La Guía del Viajero para el Análisis de Programas, Parte III: Mayormente Inofensivos LLMs

Planteamiento del Problema

Las herramientas de análisis estático son esenciales para encontrar errores en bases de código extensas como el kernel de Linux, pero sufren de altas tasas de falsos positivos. Enfoques recientes utilizan Modelos de Lenguaje de Gran Escala (LLMs) para filtrar estas advertencias mediante el razonamiento sobre el contexto del código y juzgando si un estado de error reportado es alcanzable. Sin embargo, el artículo argumenta que la efectividad empírica en el etiquetado de advertencias no equivale a una base sólida para la descarga de advertencias.

Existe una distinción crítica entre encontrar un error (existencial: un solo camino de ejecución factible que alcance el estado de error es suficiente) y descargar una advertencia (universal: el estado de error debe probarse como inalcanzable en el contexto del programa). Los LLMs pueden proporcionar explicaciones plausibles en lenguaje natural sobre por qué un error podría no ocurrir, pero estas explicaciones no constituyen una prueba formal de inalcanzabilidad. Confiar en los LLMs para el veredicto final conlleva el riesgo de descartar vulnerabilidades reales basándose en un razonamiento plausible pero no verificado, particularmente cuando el modelo sobre-constriñe las entradas controladas por el atacante o pasa por alto sutiles conversiones de tipos y comportamientos de frameworks.

Metodología: El Sistema Evident

Los autores proponen Evident, un sistema de análisis de errores que separa la asistencia de los LLMs del razonamiento del comportamiento del programa. El principio central es que los LLMs deben utilizarse para construir un harness de análisis (un artefacto de programa ejecutable y autónomo), mientras que la decisión final sobre el comportamiento del programa es tomada por un analizador de backend formal.

Flujo de Trabajo

1. Entrada: Evident recibe una advertencia de un detector estático de front-end, la cual incluye una fuente, un sumidero (sink), un camino reportado y un estado de error (por ejemplo, acceso fuera de límites).
2. Construcción de Harness Guiada por LLM:
   • El LLM tiene la tarea de construir un programa en C (el harness) que invoque un punto de entrada de driver específico e inicialice el estado necesario para ejercer el camino reportado.
   • Inicialización Abstracta Preservadora de Tipos: Crucialmente, el LLM no elige valores o rangos concretos para las entradas dependientes de la advertencia. En su lugar, inserta llamadas a una primitiva abstract_value(x), que inicializa la variable con un valor abstracto derivado estrictamente de su tipo en C. Esto asegura que el harness preserve el rango completo de entradas controladas por el atacante definidas por el tipo del programa, evitando que el LLM "corrija" inadvertidamente las entradas hacia valores benignos.
   • El LLM utiliza herramientas de navegación de código (por ejemplo, clangd) para resolver definiciones, cadenas de llamadas y estructuras de framework necesarias para conectar el harness.
3. Validación del Harness (Puerta de Admisión):
   • Antes de que el backend formal se ejecute, Evident valida el harness generado contra la advertencia original.
   • Las comprobaciones incluyen:
     • Alcanzabilidad: ¿El harness alcanza el sumidero reportado y los puntos de control relevantes en el testigo de flujo de valores?
     • Auditoría de Entrada Abstracta: ¿Se inicializan los valores dependientes de la advertencia mediante abstract_value (no restringidos por el tipo) en lugar de intervalos concretos?
     • Auditoría de Dependencias: ¿Evita el harness la fijación de estados globales o guardas que podrían influir en el estado de error?
   • Si un harness falla la validación (por ejemplo, si sobre-constriñe las entradas o no alcanza el sumidero), se descarta. El LLM puede recibir instrucciones para repararlo, pero no se deriva ningún veredicto de un harness fallido.
4. Análisis de Backend:
   • Los harnesses aceptados son analizados mediante Frama-C/Eva (un plugin de análisis de valores basado en interpretación abstracta).
   • El backend verifica si el estado de error reportado es inalcanzable bajo el harness construido.
   • Resultados:
     • Sin Error (No Bug): El backend demuestra que el estado de error es inalcanzable.
     • Aún con Alarma (Still Alarmed): El backend no puede demostrar la inalcanzabilidad (la advertencia permanece).
     • No Resuelto (Unresolved): No se generó un harness aceptado, o el análisis agotó el tiempo o falló.

Contribuciones Clave

1. Uso Principiado de LLMs: El artículo articula un rol para los LLMs que externaliza el contexto específico de la advertencia como un artefacto ejecutable (el harness) mientras descarta el veredicto final del LLM. La decisión de descargar una advertencia es tomada únicamente por el análisis formal del artefacto.
2. Validación para Harnesses Generados por LLM: Los autores introducen un conjunto de comprobaciones de admisión que imponen requisitos de preservación necesarios. Estas comprobaciones aseguran que un harness generado no altere el contexto del análisis de una manera que oculte el estado de error reportado (por ejemplo, al sobre-constriñir las entradas). Los harnesses que fallan estas comprobaciones son rechazados en lugar de ser utilizados para sustentar un veredicto.
3. Evaluación Empírica: El sistema se evalúa sobre 200 advertencias reales de drivers del kernel de Android provenientes de dos detectores estáticos (SUTURE y CodeQL-OOB).

Resultados

• Precisión: Evident clasifica correctamente 151 de los 200 casos (76%).
• Falsos Negativos: Evident descarga cero errores confirmados en el conjunto de datos. Todas las decisiones incorrectas fueron falsos positivos conservadores (advertencias que permanecieron en alarma a pesar de no ser errores) o casos no resueltos.
• Falsos Positivos: Evident descarga 111 falsas alarmas sin suprimir ningún error confirmado.
• Comparación con Baselines:
  • Comparado con los baselines de triaje basados únicamente en LLM (incluyendo agentes BugLens y Codex), Evident reduce significativamente los falsos negativos. Mientras que los baselines omitieron entre 14 y 18 errores reales (falsos negativos) al confiar en un razonamiento plausible pero insuficiente, Evident no omitió ninguno.
  • Los "fallos" de Evident son principalmente conservadores: deja 28 advertencias que no son errores en estado de alarma y 21 casos como no resueltos, en lugar de descartar incorrectamente errores reales.
• Sensibilidad del Modelo: El sistema funciona con varios LLMs (GPT-5.5, Claude Sonnet, GLM-5.1). Si bien los modelos más fuertes producen más harnesses aceptados (mayor cobertura), la regla de decisión (análisis de backend) asegura que incluso los modelos más débiles no produzcan veredictos de "no error" incorrectos.
• Descubrimiento de Vulnerabilidades: Evident redescubrió una vulnerabilidad confirmada que había sido pasada por alto tanto por el filtrado previo basado en LLM como por el triaje manual.

Significado y Reivindicaciones

El artículo sostiene que el razonamiento del comportamiento del programa debe fundamentarse en el análisis formal, no realizarse directamente por los LLMs.

• Frontera de Confianza: Evident establece una clara frontera de confianza donde el LLM actúa como un constructor de contexto y el analizador formal actúa como el juez. Esto evita el problema del "razonamiento plausible" donde un LLM podría descartar con confianza un error real debido a un chequeo local que ignora el contexto global (por ejemplo, el estrechamiento de tipo de long a int).
• Seguridad sobre Exactitud: El sistema prioriza la seguridad en la descarga de advertencias. Al requerir un harness aceptado y una prueba formal de inalcanzabilidad, Evident asegura que las decisiones de "no error" no se basen en alucinaciones del modelo o suposiciones sobre-constreñidas.
• Practicidad: El enfoque demuestra que los LLMs pueden manejar eficazmente la difícil tarea de reconstruir contextos complejos de frameworks del kernel (que son difíciles de modelar manualmente) para permitir el análisis formal, siempre que el output del LLM sea rigurosamente validado antes de ser utilizado para la toma de decisiones.

Los autores concluyen que, aunque los LLMs se utilizan cada vez más en el análisis de errores, su rol debe limitarse a la construcción de representaciones analizables del contexto del programa, dejando el juicio final sobre el comportamiento del programa a los métodos formales.