Dogwood: 基于一阶时序逻辑的策略监控

# 介绍 Dogwood：AI 智能体的运行时验证 | Amazon Web Services 来源：https://aws.amazon.com/blogs/opensource/introducing-dogwood-runtime-verification-for-ai-agents/ AI 智能体之所以如此有用，部分原因在于其能够通过运行工具与外部世界进行交互。但这些工具调用也是确保智能体安全使用的最大风险来源。以可靠、稳健的方式应对此风险的最佳方法，是在工具调用边界处设置一个控制层，用以规范智能体被允许执行的操作。通过强制执行关于智能体如何使用工具的规则，我们能够严格保证智能体影响外部世界的方式。为有效实现这一点，我们需要一种精确指定和强制执行智能体行为规则的方法。今天，我们正式发布 **Dogwood** (https://github.com/dogwood-policy/dogwood)，这是一个专为智能体及其工具设计的开源治理语言。 我们此前已经论证了使用 **AgentCore Policy** 来规范智能体工具调用的必要性，它是 Amazon Bedrock AgentCore 中的一部分，负责在每次工具调用时判定智能体的操作是否被允许。AgentCore Policy 启动时使用了 **Cedar** (https://www.cedarpolicy.com/) 作为编写这些策略的语言。Cedar 迅速、可读性强，并可通过自动推理进行分析，它还提供了一项审计和强制执行所依赖的保证：相同的请求无论评估顺序或系统状态如何，都会得出相同的决策。**《为什么 Amazon Bedrock AgentCore 的 Policy 选择 Cedar 来保障智能体工作流的安全》** (https://aws.amazon.com/blogs/security/why-policy-in-amazon-bedrock-agentcore-chose-cedar-for-securing-agentic-workflows/) 一文详细解释了这一选择及其背后的自动推理的重要性。Cedar 支持高效的*即时*授权决策，每个请求都独立评估，不依赖于过去的操作。因此，它可以围绕任何单个操作划定一个安全边界，但它并非为表达关于操作*序列*的规则而设计。即时决策对于许多形式的访问控制是合理的，但当智能体将多个操作组合成更长的工作流时，操作序列本身就成为了团队希望治理的对象。Dogwood 为他们提供了一种语言，用于表达基于序列的策略，以捕获对前置条件、速率限制和排序的约束。例如，我们可能希望要求智能体在执行操作前获得批准、保持在运行限制之内，或者在访问机密信息后永不联系外部方。为强制执行这类限制，策略层必须能够回溯当前请求之外的内容。 在 **Dogwood** 中，策略可以回溯智能体最近的事件，而不仅仅是当前请求。Dogwood 支持评估现有的 Cedar 策略，并引入了一个强大新工具：**时序条件**。时序条件引用先前事件的历史，这使得表述策略成为可能，该策略确保智能体按正确顺序使用工具、在使用某些工具后停止使用其他工具，并限制某些工具的使用频率。Dogwood 基于精确的数学基础，称为**时序逻辑**，赋予其解决最关键智能体安全问题所需的力量。 我们也在 AgentCore Policy 中推出了 Dogwood 策略支持。由于 Dogwood 与现有的 Cedar 策略兼容，客户可以继续使用他们当前的策略，无需任何迁移。他们现在可以利用 Dogwood 的时序条件来扩展现有策略并制定新策略。随着 Dogwood 语言的开源发布，客户可以使用他们喜爱的 IDE 或编码智能体来定义策略，并通过 Dogwood 解析器、验证器和参考解释器来探索其行为。Dogwood 语言在 Apache 2.0 许可证下发布。 ## **时序策略** Cedar 策略在 `when { ... }` 子句中的条件只能看到当前的授权请求。Dogwood 添加了第二种类型的子句——`when temporal { ... }`——其条件还可以查看请求之前发生的事情。这些时序子句表达了关于**事件**轨迹的属性。每个事件对应于一个工具调用请求或其结果，并记录与该工具调用相关的数据（例如输入参数、请求主体等）。策略可以讨论的工具调用集合是*操作模式*，对于智能体，该模式由其已通过模型上下文协议（MCP）公开的工具生成。我们将通过一系列涉及股票交易智能体（其工具包括 `ApproveSale`、`SellShares` 和 `Transfer`）的示例，来介绍 Dogwood 用于时序策略的操作符。 ### **回溯：先批准后销售** 在第一个示例中，假设我们希望确保智能体只有在已经获得完全相同数量的批准后才能出售股票。因此，`SellShares` 工具调用依赖于*更早的事件*，即时条件无法看到它，但在 Dogwood 中我们可以如下表达： ``` // 仅当同一股票的同一数量在过去一小时内获得批准后才允许销售。 permit ( principal, action == AgentCore::Action::"SellShares", resource ) when temporal { formerly within 1h AgentCore::Action::"ApproveSale"::response{ input.stock: context.input.stock, input.shares: context.input.shares, output.approved: true } }; ``` `formerly` 操作符是向后查看的：如果它描述的条件在指定的时间窗口内至少发生一次，则成立。这里，窗口是 `within 1h`，因此它会回溯过去一小时，查看在任何时间点是否满足指定条件。该条件是相应的 `ApproveSale::response` 事件发生了，它代表了先前某个 `ApproveSale` 工具调用的结果。该 `ApproveSale` 调用的 `input.stock` 和 `input.shares` 字段必须与当前请求的 `context.input.stock` 和 `context.input.shares` 匹配。此外，该调用的 `output.approved` 标志必须为 `true`，表明请求实际上已被批准。 为了进一步解释此策略，让我们考虑在下面所示的示例事件轨迹上发生的情况。轨迹中的每一行描述一个事件。事件描述以“@n”形式的开头，其中 n 表示事件发生的时间，以秒为单位。在 Dogwood 策略中，所有时序条件都使用相对时间，测量请求与较早事件之间的时间差，因此此时间戳的绝对值并不重要。为简单起见，在我们的每个示例中，我们将第一个事件的时间戳设为 0。在时间戳之后，事件描述记录了操作和事件类型：工具调用的名称以及它是请求还是响应。接下来，在花括号中，我们有与事件相关的参数。最后，当事件是请求时，该行以策略给出的授权决定结束，即 `DENY` 或 `ALLOW`。 ``` @0 SellShares::request { stock: "AMZN", shares: 100 } -> DENY @1700 ApproveSale::response { stock: "AMZN", shares: 100, approved: true } @1800 SellShares::request { stock: "AMZN", shares: 100 } -> ALLOW @7200 SellShares::request { stock: "AMZN", shares: 100 } -> DENY ``` 将事件流与此策略重新播放，显示了随着近期情况变化，裁决也发生变化。第一个事件是一个被拒绝的请求，因为没有任何批准记录。第二个事件是对销售批准请求的响应。这不是一个请求，因此没有附加裁决，但它被记录在事件历史中并影响后续请求。第三个事件是另一个请求，这次被批准，因为在这种情况下，时间窗口内存在批准。然而，第四个事件中的请求再次被拒绝，因为批准超出了窗口范围。 请注意，在此轨迹中，最后一个 `SellShares::request` 发生在先前被允许的请求的响应之前。这可能是因为智能体可以并行进行工具调用并与工具异步交互。此外，虽然我们将在示例中关注单个智能体的策略，但这种交错也可能在多智能体环境中出现。因此，在编写策略时，牢记这种并发性非常重要。 ### **混合时序和非时序子句** 之前的策略完全是时序的，但大多数真实规则会结合关于近期的事实和关于请求本身的简单事实。为此，Dogwood 允许将时序子句嵌入 Cedar 表达式中：`temporal { ... }` 标记本身就是一个表达式，因此可以像您编写的普通 Cedar 一样直接放入普通的 `when` 子句中。例如，这里销售必须*同时*金额小*并且*最近获得批准： ``` // 仅当销售金额小（对当前请求的简单、即时检查）且同一股票和数量的批准在过去一小时内获得时才允许销售（通过 `temporal` 标记内联的时序检查）。 permit ( principal, action == AgentCore::Action::"SellShares", resource ) when { context.input.shares <= 100 && temporal { formerly within 1h AgentCore::Action::"ApproveSale"::response{ input.stock: context.input.stock, input.shares: context.input.shares, output.approved: true } } }; ``` `context.input.shares <= 100` 正是您在不使用 Dogwood 时编写的 Cedar 策略——它仅查看当前请求。它旁边的 `temporal { ... }` 则回溯近期事件。两者都必须成立，请求才能被授权，我们可以在以下轨迹中看到： ``` @0 SellShares::request { stock: "AMZN", shares: 50 } -> DENY @60 ApproveSale::response { stock: "AMZN", shares: 50, approved: true } @120 SellShares::request { stock: "AMZN", shares: 50 } -> ALLOW @180 ApproveSale::response { stock: "AMZN", shares: 500, approved: true } @240 SellShares::request { stock: "AMZN", shares: 500 } -> DENY ``` 这里第一个事件中的请求被拒绝，因为尽管股数低于 Cedar 表达式设置的阈值，但历史记录中没有批准，因此时序部分失败。对于第三行的请求，股数小且历史记录中有批准，因此被允许。然而，对于最后的请求，尽管历史记录中有批准，它仍然被拒绝，因为股数超过了 Cedar 表达式设置的阈值。 ### **计数：发生了多少次** 另一类常见策略不仅需要知道过去是否发生了某事，还需要知道发生了多少次。最简单的是对某个窗口内事件发生次数的简单计数。这些可用于编写*速率限制*策略。例如，“一小时内转账不超过五次，无论每次金额多小”可以表达为： ``` // 当一小时内已转出五次后禁止转账。 forbid ( principal, action == AgentCore::Action::"Transfer", resource ) when temporal { count_within(1h, AgentCore::Action::"Transfer"::request{ input.amount: _ }) > 5 }; ``` 顾名思义，此 `count_within` 将统计过去一小时（`1h`）内的每一次 `Transfer` 请求——`_` 是一个通配符，表示我们不关心金额，只关心事件是否发生——并将计数与五进行比较。这将导致以下事件轨迹产生如下裁决： ``` @0 Transfer::request { amount: 20 } -> ALLOW // 第1次转账 @60 Transfer::request { amount: 20 } -> ALLOW // 第2次 @120 Transfer::request { amount: 20 } -> ALLOW // 第3次 @180 Transfer::request { amount: 20 } -> ALLOW // 第4次 @240 Transfer::request { amount: 20 } -> ALLOW // 第5次 @300 Transfer::request { amount: 20 } -> DENY // 窗口内的第6次超过限制 ``` ### **计算不同项** 有时，您需要的不是事件计数，而是事件中*不同值*的计数：不是“多少次转账”，而是“多少个不同的收款人”。例如，我们可以表达“智能体在一小时内最多只能向三个不同的收款人转账”： ``` // 当转账将使其成为过去一小时内支付的第四个不同收款人时禁止转账。 forbid ( principal, action == AgentCore::Action::"Transfer", resource ) when temporal { count_distinct_within(u, 1h, AgentCore::Action::"Transfer"::request{ input.user: u }) > 3 }; ``` 这里收款人绑定到 `u`，`count_distinct_within` 统计窗口内看到的 `u` 的*不同*值——因此向同一收款人支付两次只计一次，但新的收款人会增加计数。我们可以看到当有五笔分别支付给 `bob`、`carol`、`dave`、`erin`，然后再次支付给 `bob` 的转账时会发生什么： ``` @0 Transfer::request { user: "bob" } -> ALLOW // 1个不同收款人 @60 Transfer::request { user: "carol" } -> ALLOW // 2个 @120 Transfer::request { user: "dave" } -> ALLOW // 3个 @180 Transfer::request { user: "erin" } -> DENY // 将是第4个不同收款人 @240 Transfer::request { user: "bob" } -> DENY // 仍然是4个（bob, carol, dave, erin） ``` 尽管这单次转账的所有细节都正常，但第四个*不同*收款人被拒绝；之后重复向 `bob` 转账仍然被拒绝，因为窗口内已经有太多不同的收款人了。 ### **求和：保持运行总计低于限额** 除了计数，Dogwood 还提供了对事件关联数据进行*求和*的方法。例如，对于转账工具，我们可能希望限制在某个窗口内可以转账的总金额，而不仅仅是转账事件的数量。`sum_within` 操作允许我们表达类似“过去一小时内转账总额不超过 5,000 美元，无论需要多少笔交易”的策略： ``` // 当过去一小时内转账总额（跨越任意数量的转账）超过 5,000 美元后禁止转账。 forbid ( principal, action == AgentCore::Action::"Transfer", resource ) when temporal { sum_within(a, 1h, AgentCore::Action::"Transfer"::request{ input.amount: a }) > 5000 }; ``` `sum_within` 与 `count_within` 类似，但它不是统计事件数量，而是将每次转账的 `amount` 绑定到 `a` 并将它们相加。 ### **对请求与响应进行速率限制** 在之前的速率限制策略中，我们基于 `Transfer::request` 事件而非 `Transfer::response` 事件来表达速率限制。这对于在存在并发和异步工具调用的情况下安全实现预期的速率限制非常重要。`Transfer::request` 事件包括任何请求（包括正在考虑授权的那个），而 `Transfer::response` 仅包括已完成的转账。让我们考虑，如果我们使用以下基于 `Transfer::response` 的错误策略代替，智能体将如何规避预期的限制： ``` // 当过去一小时内已结算的转账总额超过 5,000 美元后禁止转账。 forbid ( principal, action == AgentCore::Action::"Transfer", resource ) when temporal { sum_within(a, 1h, AgentCore::Action::"Transfer"::response{ input.amount: a }) > 5000 }; ``` 与前一个策略唯一的区别是一个词：它对 `Transfer::response` 事件而非 `Transfer::request` 事件求和。因为此策略只对响应相关的金额求和，智能体可以在任何一笔转账结算之前发出许多并发转账请求来规避预期限制，正如我们在以下示例轨迹中看到的： ``` response request @0 Transfer::request { amount: 2000 } ALLOW ALLOW @1 Transfer::request { amount: 2000 } ALLOW ALLOW @2 Transfer::request { amount: 2000 } ALLOW ALLOW @3 Transfer::response { amount: 2000 } @4 Transfer::response { amount: 2000 } @5 Transfer::response { amount: 2000 } @6 Transfer::request { amount: 2000 } ALLOW ALLOW @7 Transfer::request { amount: 2000 } ALLOW ALLOW ```