Resumen Técnico: Verificación Estática Basada en LLM del Código Frente a Requisitos en Lenguaje Natural

Enunciado del Problema

Las herramientas convencionales de análisis estático (por ejemplo, Coverity, SonarQube) son efectivas para detectar defectos de codificación, problemas de seguridad de la memoria y patrones de vulnerabilidad conocidos. Sin embargo, carecen de la capacidad para verificar si el código implementado satisface requisitos funcionales escritos en lenguaje natural. Existe una brecha crítica en la detección de defectos de lógica de negocio, como un programa que implementa una suma en lugar de una multiplicación, o una política de contraseñas que contradice estructuralmente su especificación en lenguaje natural. Estos defectos a menudo no contienen firmas de vulnerabilidad reconocibles y son difíciles de exponer mediante pruebas dinámicas debido a la cobertura limitada de casos de prueba, la dificultad de definir oráculos de prueba y la complejidad de grandes espacios de entrada. El desafío consiste en realizar un análisis estático consciente de los requisitos y consciente de la semántica que verifique el código frente a especificaciones en lenguaje natural sin requerir compilación, ejecución o entornos de tiempo de ejecución.

Metodología

El artículo propone un flujo de trabajo basado en LLM de dos etapas diseñado para abordar el problema de verificación dependiente de especificaciones en un contexto de ciberseguridad de vehículos inteligentes. Este enfoque evita pedir a un único LLM que verifique directamente el código frente a especificaciones extensas en lenguaje natural, lo cual conlleva riesgos de alucinación, variabilidad de salida y pérdida de contexto. En su lugar, introduce una representación intermedia estructurada.

Etapa 1: Minería de Reglas Basada en IA (ruleMiner)

El primer agente, ruleMiner, procesa los requisitos en lenguaje natural frase por frase para extraer un conjunto de reglas verificables.

• Lógica de Extracción: Retiene únicamente la lógica normativa y falsable (por ejemplo, declaraciones explícitas de "deberá" y declaraciones de "debería" contextualmente obligatorias).
• Manejo de Ambigüedad: Se excluye el material explicativo, permisivo o subjetivo. Términos como "aleatorio" o "fuerte" no se convierten en reglas a menos que se fundamenten en condiciones medibles.
• Registro de Defectos: Las ambigüedades, las autocontradicciones y las declaraciones no verificables no se traducen en reglas. En su lugar, se registran explícitamente en una estructura de datos requirements_specs_issues para evitar que los requisitos defectuosos contaminen las verificaciones posteriores.
• Mejora de la Completitud: Para abordar la variabilidad de salida, el sistema emplea una relación metamórfica (MR1): incluso con la temperatura del LLM establecida en 0, las ejecuciones repetidas pueden producir salidas diferentes. Se utiliza una estrategia de agrupación para conciliar y fusionar las salidas de múltiples ejecuciones (1–3 ejecuciones) y generar un conjunto de reglas más completo.

Etapa 2: Auditoría de Código Basada en IA (codeAuditor)

El segundo agente, codeAuditor, evalúa el código fuente frente al conjunto de reglas extraído.

• Razonamiento Semántico: A diferencia de los escáneres basados en patrones, codeAuditor razona sobre el contenido semántico, derivando puntos de verificación concretos como valores permitidos/prohibidos, umbrales, condiciones de unicidad y desencadenantes operativos.
• Verificación Basada en Evidencia: Verifica estos puntos frente al código fuente, configuraciones, constantes, lógica de validación y relaciones de llamadas entre archivos.
• Criterios Estrictos: Una regla no se considera satisfecha meramente por la presencia de identificadores o comentarios sugerentes. Por el contrario, una prohibición no se marca como violada a menos que exista evidencia de una ruta de habilitación real o un comportamiento alcanzable.

Estudio de Caso Industrial y Resultados

La metodología se aplicó a un estudio de caso industrial de seguridad pública que involucraba un subsistema de seguridad WiFi en vehículos.

Observaciones Clave

1. Detección de Defectos en Requisitos: La pipeline identificó con éxito requisitos contradictorios. Por ejemplo, una política de contraseñas requería tipos de caracteres específicos pero proporcionaba un patrón de ejemplo que no cumplía esas condiciones. ruleMiner marcó correctamente esto como contenido contradictorio en requirements_specs_issues en lugar de generar una regla falsa. Este defecto había permanecido sin detectar durante más de un año.
2. Detección de Desajustes de Lógica: El sistema identificó un desajuste entre un requisito (punto de acceso WiFi deshabilitado cuando "no está en uso") y la implementación. La implementación se basaba en condiciones de inactividad local en lugar del estado del sistema más amplio implicado por el requisito. Esto reveló un defecto de requisito (estado desencadenante no definido) en lugar de un simple error de codificación.
3. Hallazgos Cuantitativos:
   • Requisitos: De 222 elementos analizados, se reportaron 75 problemas de requisitos. La inspección manual del subconjunto de seguridad WiFi no encontró reglas extraídas incorrectas.
   • Código: El análisis de la base de código WiFi madura produjo 8 hallazgos "Fallo/Desconocido". La inspección manual confirmó ningún falso positivo. Se detectó un problema de codificación de alta prioridad que posteriormente fue corregido por el equipo de desarrollo.
   • Cobertura: El flujo de trabajo verificó más del 50% de los requisitos que anteriormente solo podían evaluarse mediante pruebas de software.

Contribuciones Clave

1. Pipeline de Verificación de Dos Etapas: Un flujo de trabajo novedoso que desacopla la aclaración de requisitos de la auditoría de código, utilizando un conjunto de reglas intermedio para reducir los modos de fallo del LLM (alucinación, variabilidad) y mejorar la explicabilidad.
2. Manejo Explícito de Defectos: La introducción de la estructura requirements_specs_issues asegura que los requisitos ambiguos o contradictorios se pongan de manifiesto en lugar de normalizarse silenciosamente en reglas verificables por máquina pero semánticamente poco fiables.
3. Integración de Pruebas Metamórficas: La aplicación de relaciones metamórficas (específicamente la agrupación de múltiples ejecuciones de LLM) para mejorar la completitud y consistencia de la minería de reglas.
4. Análisis Estático Orientado a la Lógica de Negocio: Un cambio de la detección basada en patrones al razonamiento consciente de la semántica, capaz de identificar desajustes en desencadenantes, rutas de ejecución y lógica de aplicación que las herramientas convencionales pasan por alto.

Significado y Afirmaciones

El artículo posiciona este enfoque como una estrategia complementaria y no de reemplazo para las pruebas dinámicas y el análisis estático convencional. Su significado principal radica en:

• Verificación "Shift-Left": Permitir la detección de defectos de lógica de negocio en etapas más tempranas del ciclo de vida del desarrollo sin necesidad de compilación, ejecución o entornos de tiempo de ejecución.
• Abordar el Problema del Oráculo de Prueba: Al razonar sobre la semántica del código fuente y la lógica de implementación en lugar de depender exclusivamente de las salidas programadas esperadas, la cadena de herramientas basada en LLM ayuda a mitigar la dificultad de definir oráculos de prueba para lógica de negocio compleja.
• Trazabilidad Industrial: Destacar la dependencia crítica de una alta calidad en la trazabilidad (por ejemplo, historial de solicitudes de fusión) entre requisitos y código, señalando que las brechas en la trazabilidad organizacional pueden limitar la interpretación definitiva de los hallazgos.

Los autores mantienen un tono modesto, señalando que los resultados cuantitativos son preliminares y no afirmaciones de referencia. Reconocen que la recuperación y la completitud de la minería de reglas no se evaluaron exhaustivamente debido al esfuerzo manual requerido. Sin embargo, la experiencia sugiere que integrar la aclaración de requisitos, la conciencia de la trazabilidad y el análisis estático basado en LLM representa una dirección prometedora para la garantía industrial.