💻 computer science

FAVA: Formal Authorization for Verified Agents with Evidence-Backed Permission Graphs

FAVA 是一个正式的授权框架，通过将自然语言任务转化为结构化权限图，并利用 SMT 求解器将其针对安全策略进行数学验证，从而在未经授权的操作发生前对其进行拦截，确保了 LLM 智能体执行过程中的安全性。

原作者： Yifan Zhang, Xinkui Zhao, Sai Liu, Hengxuan Lou, Guanjie Cheng, Chang Liu

发布于 2026-07-31

📖 1 分钟阅读☕ 轻松阅读

原作者： Yifan Zhang, Xinkui Zhao, Sai Liu, Hengxuan Lou, Guanjie Cheng, Chang Liu

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象这样一个世界：你的电脑不再仅仅是听从指令，而是真正地在对指令进行“思考”，像数字侦探或编程巫师一样规划复杂的任务。这就是 AI 智能体（AI agents） 的领域——这些由大语言模型（LLM）驱动的智能程序可以阅读文件、编写代码，甚至与其他计算机交谈。但问题在于：这些智能体具有极强的创造力，这意味着它们有时会做得太过火，从而在无意中做出危险的行为，比如删除重要文件或将秘密密码发送给错误的人。

为了约束这些数字助手，我们通常使用“准许条（permission slips）”。你可以把它们想象成一份简单的规则清单：“你可以读取这个文件，但不能碰那个。”然而，现实生活是复杂的。有时候，某个动作只有在“完成作业之后”才是安全的，或者只有在“没有拿着秘密钥匙”时才是安全的。这些被称为**上下文相关（context-dependent）**的规则。问题在于，传统的权限列表过于僵化；它们无法理解忙碌的一天中那种“如果……那么……”的逻辑。如果我们不能教会这些智能体理解其行为背后的“故事”，它们可能会在甚至没有意识到违规的情况下破坏规则。这就是为什么科学家们正在竞相构建更好的安全系统，以追踪整个过程的故事，而不仅仅是单个步骤。

于是有了 FAVA（用于验证智能体的形式化授权，Formal Authorization for Verified Agents），这是一个旨在成为这些 AI 智能体终极“保安”的新型安全系统。FAVA 不仅仅是听信 AI 说“我保证我会很安全”，它更像是一个超级严格、热爱数学的裁判，会在每一步行动发生之前进行检查。

以下是 FAVA 的工作原理，我们用一个有趣的类比来解释：想象 AI 智能体是一位在厨房里想要烹饪复杂餐点的厨师。

翻译官（权限中间表示，Permission IR）： 首先，厨师用凌乱的手写笔记记录下他们的食谱（自然语言任务）。FAVA 有一位翻译官，负责阅读这些凌乱的笔记，并将其转化为一份严格、结构化的蓝图，即权限中间表示（Permission IR）。这份蓝图不仅说“烹饪鸡肉”，还会说“使用鸡肉（资产）来做汤（动作），但前提是炉灶必须是开启状态（上下文），并且绝不允许生鸡肉接触沙拉（安全规则）”。
地图绘制者（权限图，Permission Graph）： 接下来，FAVA 会根据那份蓝图绘制一张详细的地图，称为权限图（Permission Graph）。在这张地图上，每种食材和工具都是一个点，而规则则是连接它们的线。如果厨师试图使用“秘密香料”（敏感数据），地图就会亮起红灯。如果厨师试图把食物扔出窗外（向互联网发送数据），地图会检查他们是否拥有“垃圾处理许可”。
数学法官（SMT 授权器，SMT Authorizer）： 这是最酷的部分。FAVA 不仅仅是靠猜测；它使用一个强大的数学引擎（SMT 求解器）来检查地图。它会询问：“这位厨师现在在数学上是否有可能违反规则？”如果答案是“是的，存在泄露秘密的可能性”，系统会立即踩下刹车并说：“停！这里就是你出错的地方。”如果答案是“不，规则是安全的”，厨师就能获得绿灯通行。

研究人员在许多棘手的场景中测试了 FAVA，包括真实的编程任务和安全挑战。他们发现 FAVA 在工作中表现得极其出色。在测试中，它成功拦截了其他安全系统漏掉的 90.5% 的危险行为。它在识别那些取决于事件顺序或隐藏条件的复杂情况方面表现尤为出色。

然而，FAVA 并非万能。论文明确指出，该系统依赖于初始翻译官能否正确阅读厨师凌乱的笔记。如果翻译官遗漏了一个关键细节（比如忘记提到炉灶坏了），数学法官可能无法捕捉到错误。此外，由于 FAVA 非常谨慎，它有时会为了确保万无一失而拦截一些原本安全的动作（即“误报”），但作者表示，为了保护秘密，这是一个公平的权衡。他们展示了，相比于其他要么放行太多坏事、要么盲目拦截一切的系统，FAV 通过将模糊的指令转化为经过数学验证的地图，找到了那个完美的平衡点。

简而言之，FAVA 证明了我们可以通过让 AI 智能体走过一个经过数学检查的迷宫——在每一步被执行前都经过验证——来让它们变得更安全，而不是仅仅寄希望于它们的自觉。这就像是给你的数字助手配了一个安全带和一个 GPS，一旦你试图驶向悬崖，它就会大声尖叫“停！”，确保即使是最有创造力的 AI 也能在既定的轨道内行驶。

技术摘要：FAVA（基于证据支撑权限图的正式化验证智能体授权）

问题陈述

大型语言模型（LLM）智能体越来越多地在动态且关键的环境中运行（例如，代码仓库、云存储、本地 Shell），这些环境将语义推理与复杂的系统操作交织在一起。本文认为，现有的授权机制在这些场景下存在根本性的不足，主要由于以下三个局限性：

静态与动态的不匹配： 现有的防御手段依赖于静态的工具级白名单或关键词过滤，无法考虑到智能体执行过程中高度依赖上下文的特性。现实世界的智能体策略通常涉及序列依赖的时间约束（在分析的项目中占 90%）和嵌套条件逻辑（超过 40%），而静态列表无法捕捉这些特性。
语义歧义性： 仅基于提示词（Prompt-only）的策略（例如，要求模型“保持安全”）缺乏强制执行能力，而操作系统级的沙箱又缺乏治理高层条件逻辑和数据流所需的语义理解能力。
缺乏形式化保证： 概率性的 LLM 无法在数据外泄、破坏性状态修改或时间义务违反方面提供形式化正确性的保证。

方法论

FAVA 提出了一种将语义理解与逻辑执行解耦的运行时授权框架。该系统通过一个四阶段流水线运行：

1. 证据获取与权限中间表示（IR）

FAVA 将 LLM 严格用作语义提取器，而非决策者。它将自然语言任务、执行合约和运行时追踪解析为结构化的权限中间表示（Permission Intermediate Representation, IR）。该 IR 通过五个核心字段显式定义授权边界：

意图（Intent）、资产（Assets）、动作（Actions）、义务（Obligations）以及汇聚点（Sinks）。
证据跨度（Evidence Spans）： 连接每个字段与其来源的加密或文本链接。
这一步骤将复杂的语义指令（例如，“在测试前需要审核”）保留为可审计的结构化约束，而非模糊的模型判断。

2. 图降级（Graph Lowering）

一个确定性的降级过程将权限 IR 转换为一个由证据支撑的权限图 $G = (V, E)$ 。

节点： 携带基于证据的安全性标签（例如，secret、pii、destructive）。
边：编码依赖关系，包括数据流、控制守卫（时间约束）和运行时祖先关系。
净化（Sanitization）： 要求显式的受信任转换器规范（例如，redact(secret) -> safe_text）；模糊的断言不被视为净化器。
该图作为一个可形式化验证的基质，将语义数据转化为适用于数学验证的结构。

3. SMT 授权

核心的安全决策由一个可满足性模理论（SMT）授权器（使用 Z3 实现）计算完成。求解器根据固定的策略评估图，以确定能力分配是否是可满足的。

污点传播： 标签沿依赖边传播，除非经过受信任的净化器进行转换。
约束求解： 系统检查是否存在禁止的流（例如，secret $\to$ net:*）。
输出： 求解器返回已授权的能力集或一个识别违规路径的精确反例。
单调性： 系统支持“单调图修复”，即运行时事件向图中追加新事实，从而在任何影响性动作发生前强制进行重新授权。

4. 运行时网关

一个即时（JIT）网关负责执行求解器的结果。

决策逻辑： 如果发现反例，则拦截该动作。如果没有发现违规，但风险态势仍处于敏感或模糊状态，网关将失效闭锁（Fail Closed）（即拦截动作），以安全性优先于可用性。
范围： 网关调节所有与安全相关的运行时效应，确保后端执行始终处于授予的能力集之内。

核心贡献

框架概念： 引入了 FAVA，一种新型的运行时授权框架，它将权限管理从静态白名单转向可验证的图授权。
形式化方法： 该流水线利用 LLM 进行结构化 IR 提取，确定性地将其降级为证据支撑的图，并采用 SMT 授权器进行策略一致性决策。这种设计实现了单调图修复和即时重新授权。
全面评估： 在 OpenAgentSafety、OctoBench 和 ActPlane 场景下进行了广泛测试，证明了其具有高决策合规性，并能拦截动态违规追踪。

实验结果

作者在四个基准测试的 801 个任务上对 FAVA 进行了评估。

决策合规率（DCR）： FAVA 在整个数据集上的 DCR 达到了 90.5%。
追踪条件场景： FAVA 在结构化且带标签的追踪条件拆分集（ActPlane Public 和 ActPlane Traces）上实现了 100.0% 的 DCR，成功拦截了所有未经授权的动作，且在这些特定拆分集中没有出现漏报（False Negatives）。
对比：
- 对比静态/正则防护： FAVA 显著优于 Regex Guard，后者存在严重的过度拦截问题（在 OpenAgentSafety 上为 0 个真阴性）。
- 对比仅提示/启发式方法： FAVA 优于 GuardAgent 和 AgentSpec，后者由于缺乏显式的数据流追踪，表现出大量的漏报（False Negatives）。
效率： 主动运行时网关增加的开销极小，仅为 0.3%。即使对于包含多达 10 个节点的图，其中值即时授权时间也仅为 0.845 ms。

重要性与主张

论文声称 FAVA 通过显式地将 LLM 理解与安全执行解耦，为保护自主智能体建立了严格的、具有数学基础的基石。

形式化保证： 系统针对生成的权限图和策略翻译提供了形式化保证。它断言任何可满足的能力分配都严格符合所有编码的策略规则。
范式转移： 它解决了自然语言指令与严谨执行之间的“模态间隙”，将模糊的任务转化为确定性的基质。
保守安全： 该框架有意采取保守立场，通过在模糊或敏感动作上采取失效闭锁策略，将安全性置于可用性之上。这种权衡导致了较高的攻击拦截率（98.9%），但也造成了一些良性可用性的损失（评估中出现 69 次误拦截）。

作者指出，系统的健全性取决于上游 LLM 提取的正确性和网关的完整性。虽然数学授权是鲁棒的，但系统并不声称解决了自然语言提取的完备性或隐式流发现的问题。未来的改进方向在于提升面向溯源的语义提取能力，而非改变 SMT 决策逻辑。