LATIDIA · Ciberseguridad

Verificación formal del tiempo de ejecución para agentes de LLM que utilizan herramientas: un estudio fuera de línea del mismo punto de referencia sobre AgentDojo y STAC

arXiv: 2610.09793v1Tipo de anuncio: nuevo Resumen: Las barandillas para los agentes LLM que utilizan herramientas suelen ser reglas específicas de la aplicación, lo que hace que las políticas de seguridad dependientes de datos de varios pasos sean difíciles de especificar, auditar y reutilizar. Como d

La noticia

arXiv:2610.09793v1 Announce Type: new Abstract: Guardrails for tool-using LLM agents are usually application-specific rules, which makes multi-step, data-dependent safety policies hard to specify, audit and reuse. As a declarative alternative, we evaluate metric first-order temporal logic (MFOTL), replaying the recorded trajectories that AgentDojo, STAC and R-Judge already ship through the unmodified MonPoly monitor, offline and without running an agent. On these corpora, five generic obligations flag 71.8% of STAC attack chains and 70.1% of successful AgentDojo attacks, but also fire on 29.3% of benign runs. This imprecision stems from the corpora rather than the logic: they rarely record approvals and never record timestamps, so history-dependent obligations reduce to detecting risky