让大模型代理在运行时自动验证权限，防止越权操作。
FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs
- 用自然语言生成结构化权限约束，再转为带证据的权限图。
- 90.5%决策合规率，能识别并拦截动态违规执行路径。
- 适合关注AI安全、自主代理授权的开发者和研究者。
大型语言模型代理在复杂系统中自主进行语义推理与操作。静态工具权限无法满足需求，安全授权必须依赖实时状态与数据流。我们提出FAVA（形式化授权框架），通过LLM引导的权限中间表示，将模糊的自然语言任务转化为结构化约束；再经确定性降阶，生成显式追踪数据流、依赖关系与上下文标签的证据支撑权限图。通过SMT求解器对当前图进行数学验证，确保符合安全策略后才允许执行。运行时网关根据求解结果强制放行或拦截，并提供精确反例。我们在OpenAgentSafety、OctoBench和ActPlane场景下评估，总数据集上实现90.5%的决策合规率（DCR），成功拦截了条件触发的违规执行轨迹。
原文摘要 · Abstract (English)
Large language model (LLM) agents autonomously interleave semantic reasoning with complex system operations. In these dynamic environments, static tool-level permissions are fundamentally insufficient; safe authorization is highly context-dependent and heavily reliant on evolving runtime states and data flows. We present FAVA (Formal Authorization for Verified Agents), a permission-carrying authorization framework for agent execution. FAVA utilizes an LLM-guided Permission Intermediate Representation (IR) to translate ambiguous natural-language tasks into structured constraints. A deterministic lowering pass then converts this IR into an evidence-backed permission graph that explicitly tracks data flows, dependencies, and contextual labels. To provide strict security guarantees, a Satisfiability Modulo Theories (SMT) authorizer mathematically verifies the current graph against security policies before any effectful action executes. A runtime gateway then enforces the solver's result, either authorizing the execution or intercepting it with a precise counterexample. We evaluate FAVA across OpenAgentSafety, OctoBench, and ActPlane scenarios. Our evaluation demonstrates that FAVA achieves a 90.5% Decision Compliance Rate (DCR) over the aggregate dataset, successfully intercepting dynamic violating traces in the evaluated trace-conditioned scenarios.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。