Resumen Técnico: FAVA (Autorización Formal para Agentes Verificados con Grafos de Permisos Respaldados por Evidencia)

Planteamiento del Problema

Los agentes de Modelos de Lenguaje de Gran Escala (LLM) operan cada vez más en entornos dinámicos y críticos (por ejemplo, repositorios de código, almacenamiento en la nube, terminales locales), intercalando el razonamiento semántico con operaciones complejas del sistema. El artículo argumenta que los mecanismos de autorización existentes son fundamentalmente insuficientes para estos entornos debido a tres limitaciones principales:

1. Desajuste entre lo Estático y lo Dinámico: Las defensas actuales dependen de listas de permitidos (allowlists) a nivel de herramienta o filtros de palabras clave estáticos, que no logran dar cuenta de la naturaleza altamente dependiente del contexto de la ejecución de un agente. Las políticas de los agentes en el mundo real suelen implicar restricciones temporales dependientes de la secuencia (90% de los proyectos analizados) y lógica condicional anidada (más del 40%), que las listas estáticas no pueden capturar.
2. Ambigüedad Semántica: Las políticas basadas únicamente en prompts (por ejemplo, pedir a los modelos que "sean seguros") carecen de capacidades de ejecución, mientras que los sandboxes a nivel de sistema operativo carecen de la comprensión semántica necesaria para gobernar la lógica condicional de alto nivel y los flujos de datos.
3. Falta de Garantías Formales: Los LLM probabilísticos no pueden garantizar la corrección formal respecto a la exfiltración de datos, las modificaciones de estado destructivas o las violaciones de obligaciones temporales.

Metodología

FAVA propone un marco de autorización en tiempo de ejecución que desacopla la comprensión semántica de la ejecución lógica. El sistema opera a través de un pipeline de cuatro etapas:

1. Adquisición de Evidencia y la IR de Permisos

FAVA utiliza un LLM estrictamente como un extractor semántico, no como un decisor. Analiza tareas en lenguaje natural, contratos de ejecución y trazas de ejecución para convertirlos en una Representación Intermedia (IR) de Permisos estructurada. Esta IR define explícitamente los límites de autorización utilizando cinco campos principales:

• Intención, Activos, Acciones, Obligaciones y Sumideros (Sinks).
• Intervalos de Evidencia (Evidence Spans): Enlaces criptográficos o textuales que conectan cada campo con su origen.
  Este paso preserva las instrucciones semánticas complejas (por ejemplo, "requerir revisión antes de probar") como restricciones estructurales auditables en lugar de juicios opacos del modelo.

2. Reducción de Grafo (Graph Lowering)

Una fase de reducción determinista convierte la IR de Permisos en un grafo de permisos respaldado por evidencia $G = (V, E)$.

• Nodos: Portan etiquetas de seguridad fundamentadas en evidencia (por ejemplo, secreto, PII, destructivo).
• Aristas: Codifican relaciones de dependencia, incluyendo flujos de datos, guardas de control (restricciones temporales) y ascendencia en tiempo de ejecución.
• Sanitización: Requiere especificaciones de transformadores explícitamente confiables (por ejemplo, redactar(secreto) -> texto_seguro); las afirmaciones vagas no se tratan como sanitizadores.
  Este grafo sirve como un sustrato formalmente verificable, transformando los datos semánticos en una estructura apta para la verificación matemática.

3. Autorización SMT

La decisión de seguridad central es computada por un autorizador SMT (Satisfiability Modulo Theories, implementado usando Z3). El solver evalúa el grafo contra una política fija para determinar si una asignación de capacidad es satisfactoria.

• Propagación de Taint (Mancha): Las etiquetas se propagan a lo largo de las aristas de dependencia a menos que sean transformadas por un sanitizador de confianza.
• Resolución de Restricciones: El sistema busca flujos prohibidos (por ejemplo, secreto $\to$ net:*).
• Salida: El solver devuelve un conjunto de capacidades autorizado o un contraejemplo preciso que identifica la ruta de violación.
• Monotonicidad: El sistema soporta la "reparación de grafo monótona", donde los eventos en tiempo de ejecución añaden nuevos hechos al grafo, forzando una re-autorización antes de cualquier acción con efectos.

4. Puerta de Enlace en Tiempo de Ejecución (Runtime Gateway)

Una puerta de enlace Just-In-Time (JIT) hace cumplir el resultado del solver.

• Lógica de Decisión: Si se encuentra un contraejemplo, la acción se bloquea. Si no hay violación, pero la postura de riesgo sigue siendo sensible o ambigua, la puerta de enlace falla de forma cerrada (fails closed) (bloquea la acción) para priorizar la seguridad sobre la utilidad.
• Alcance: La puerta de enlace media todas las ejecuciones de efectos relevantes para la seguridad, asegurando que la ejecución del backend permanezca dentro del conjunto de capacidades otorgado.

Principales Contribuciones

1. Concepto de Marco de Trabajo: Introducción de FAVA, un nuevo marco de autorización en tiempo de ejecución que desplaza la gestión de permisos de las listas de permitidos estáticas a la autorización de grafos verificables.
2. Metodología Formal: Un pipeline que aprovecha los LLM para la extracción de IR estructurada, reduce esto determinísticamente en un grafo respaldado por evidencia y emplea un autorizador SMT para las decisiones de consistencia de la política. Este diseño permite la reparación de grafos monótonos y la re-autorización justo a tiempo.
3. Evaluación Exhaustiva: Pruebas extensas en escenarios de OpenAgentSafety, OctoBench y ActPlane, demostrando una alta conformidad de decisión e interceptando trazas violadoras dinámicas.

Resultados Experimentales

Los autores evaluaron FAVA en un conjunto de datos de 801 tareas a través de cuatro benchmarks.

• Tasa de Conformidad de Decisión (DCR): FAVA logró una DCR del 90.5% sobre el conjunto de datos agregado.
• Escenarios Condicionados por Trazas: FAVA alcanzó una DCR del 100.0% en las divisiones estructuradas y etiquetadas condicionadas por trazas (ActPlane Public y ActPlane Traces), interceptando con éxito todas las acciones no autorizadas sin falsos negativos en estas divisiones específicas.
• Comparación:
  • Vs. Guardas Estáticas/Regex: FAVA superó significativamente a Regex Guard, que sufrió de un bloqueo excesivo (0 Verdaderos Negativos en OpenAgentSafety).
  • Vs. Solo Prompt/Heurística: FAVA superó a GuardAgent y AgentSpec, que exhibieron masivos Falsos Negativos (sub-bloqueo) debido a la falta de un seguimiento explícito de flujos de datos.
• Eficiencia: La puerta de enlace activa en tiempo de ejecución añade un sobrecosto insignificante del 0.3% a la ejecución viva del agente. El tiempo de autorización mediano Just-In-Time es de 0.845 ms, incluso para grafos con hasta 10 nodos.

Significado y Reivindicaciones

El artículo afirma que FAVA establece una base estricta y matemáticamente fundamentada para asegurar agentes autónomos al separar explícitamente la comprensión del LLM de la ejecución de la seguridad.

• Garantía Formal: El sistema proporciona garantías formales respecto al grafo de permisos generado y la traducción de la política. Afirma que cualquier asignación de capacidad satisfactoria satisface estrictamente todas las reglas de política codificadas.
• Cambio de Paradigma: Aborda la "brecha de modalidad" entre las instrucciones en lenguaje natural y la ejecución rigurosa mediante la traducción de tareas ambiguas en un sustrato determinista.
• Seguridad Conservadora: El marco adopta intencionalmente una postura conservadora, priorizando la seguridad sobre la utilidad al fallar de forma cerrada ante acciones ambiguas o sensibles. Este compromiso resulta en una alta tasa de interceptación de ataques (98.9%) a costa de cierta utilidad benigna (69 bloqueos falsos en la evaluación).

Los autores señalan que la solidez del sistema depende de la corrección de la extracción del LLM ascendente y la integridad de la puerta de enlace. Si bien la autorización matemática es robusta, el sistema no pretende resolver la completitud de la extracción de lenguaje natural o el descubrimiento de flujos implícitos. Las mejoras futuras se dirigen hacia la extracción semántica consciente de la procedencia en lugar de alterar la lógica de decisión del SMT.