待翻译：Introducing Dogwood: runtime verification for AI agents

AI 服务暂时不可用，以下为来源正文，待恢复后补全翻译。

Part of what makes AI agents so useful is their ability to interact with the external world by running tools. But these tool calls are also the source of the biggest risks when it comes to making agents safe to use. The best way to address these risks in a dependable and reliable manner is to put a layer of control at the tool-call boundary that regulates what an agent is allowed to do. By enforcing rules about how agents may use tools, we get rigorous guarantees about the ways agents can affect the external world. To do this effectively, we need a way to precisely specify and enforce rules about agent behavior. Today, we’re releasing Dogwood, an open source governance language designed for agents and their tools. We previously made the case for regulating agent tool use with AgentCore Policy, the layer in Amazon Bedrock AgentCore that decides, on every tool call, whether an agent’s action is allowed. AgentCore Policy launched using Cedar as the language those policies are written in. Cedar is fast, readable, and analyzable through automated reasoning, and it gives a guarantee that audit and enforcement depend on: identical requests yield identical decisions, regardless of evaluation order or system state. Why Policy in Amazon Bedrock AgentCore chose Cedar for securing agentic workflows explains that choice in detail, and why automated reasoning matters so much for it. Cedar supports efficient point-in-time authorization decisions where each request is evaluated in isolation, with no dependency on past actions. As a result, it can draw a safety envelope around any single action, but it was not designed for expressing rules about sequences of actions. Point-in-time decisions make sense for many forms of access control, but when agents compose multiple actions into longer workflows, the sequence itself becomes something teams want to govern. Dogwood gives them a language for expressing policies over sequences, in order to capture constraints on prerequisites, rate limits, and ordering. For example, we might want to require an agent to get approval before acting, stay under a running limit, or never contact external parties once it has accessed confidential information. To enforce these kinds of restrictions, the policy layer has to be able to look back beyond the current request. In Dogwood, policies can look back over an agent’s recent events, not just the current request. Dogwood supports evaluating existing Cedar policies and adds in a new and powerful tool: temporal conditions. Temporal conditions refer to the history of prior events, which makes it possible to state policies that ensure that an agent uses tools in the correct order, stops using some tools after others, and limits the frequency of some tools. Dogwood is based on a precise mathematical foundation, called temporal logic, giving it the strength required to solve the most critical agentic safety problems. We’ve also launched Dogwood policy support inside AgentCore Policy. Because Dogwood is compatible with existing Cedar policies, customers can continue to use their current policies without any need for migration. They can now make use of Dogwood’s temporal conditions to extend existing policies and craft new ones. With the open source release of the Dogwood language, customers can define their policies using their favorite IDE or coding agent and explore their behavior with the Dogwood parser, validator, and reference interpreter. The Dogwood language is released under an Apache 2.0 license. Temporal policies A Cedar policy condition in a when { ... } clause sees only the current authorization request. Dogwood adds a second kind of clause — when temporal { ... } — whose condition can also look at what came before the request. These temporal clauses express properties about traces of events. Each event corresponds to either a tool call request or its outcome and records data associated with the tool call (e.g. input arguments, requesting principal, etc.). The set of tool calls a policy can talk about is the action schema, and for an agent that schema is generated from tools it already exposes over the Model Context Protocol (MCP). We’ll tour through Dogwood’s operators for temporal policies by working through a series of examples involving a stock trading agent whose tools include ApproveSale, SellShares, and Transfer. Looking back: approve before you sell For our first example, let’s say we want to ensure that an agent may sell shares only if it already received approval for that exact amount. Thus, a SellShares tool call depends on an earlier event, so a point-in-time condition can’t see it, but in Dogwood we can express it as follows: // Permit a sale only if approval for the same amount of the same // stock came back granted within the last hour. 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 } }; The formerly operator is backward-looking: it holds if the condition it describes occurred at least once in a specified time window. Here, the window is within 1h, so it looks back over the past hour to see if the specified condition held at any point. The condition is that a corresponding ApproveSale::response event occurred, which represents the outcome of some prior ApproveSale tool call. That ApproveSale must have had input.stock and input.shares fields that match the current request’s context.input.stock and context.input.shares. In addition, the output.approved flag of that call must have been true, indicating that the request was in fact approved. To further explain this policy, let’s consider what happens on an example trace of events shown below. Each line of the trace describes an event. An event description starts with a timestamp of the form “@n”, where n indicates when the event occurred, measured in seconds. In Dogwood policies, all temporal conditions use time on a relative basis, measuring the time difference between a request and earlier events, so the absolute value of this timestamp does not matter. For simplicity, in each of our examples, we’ll start the first event at a timestamp of 0. After the timestamp, the event description records the action and kind of event: the name of the tool call and whether it was a request or response. Next, enclosed in curly braces, we have the arguments associated with the event. Finally, when the event is a request, the line ends with the authorization verdict given by the policy, either DENY or 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 Replaying a stream of events against this policy shows the verdict change as the recent past changes. The first event is a request that is denied because there has been no approval on record. The second event is a response to a sale approval request. This is not a request, so it has no verdict attached, but it is recorded in the event history and affects later requests. The third event is another request, which this time is approved, because in this case there is an approval within the time window. However, the request in the fourth event is denied again as the approval is outside the window. Notice that in this trace, the last SellShares::request occurs before the response of the previous allowed request. This can happen because agents can make parallel tool calls and interact with tools asynchronously. Moreover, while we’ll focus on policies for a single agent in our examples, this kind of interleaving can also arise in multi-agent settings. Thus, it is important to keep this kind of concurrency in mind when writing policies. Mixing temporal and non-temporal clauses That previous policy was entirely temporal, but most real rules combine a fact about the recent past with a plain fact about the request itself. To support this, Dogwood allows embedding temporal clauses inside a Cedar expression: the temporal { ... } marker is an expression, so it drops straight into an ordinary when clause alongside the Cedar you already write. For example, here a sale must be both small and recently approved: // Permit a sale only if it is small (a plain, point-in-time check on // this request) AND approval for the same stock and amount came back // granted within the last hour (the temporal check, inline via the // temporal marker). permit ( principal, action == AgentCore::Action::"SellShares", resource ) when { context.input.shares 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 The request in the first event here is denied, because even though the share count is below the threshold set by the Cedar expression, there is no approval in the history, so the temporal half fails. For the request on the third line the share count is small and there is an approval in the history, so it is allowed. However, for the last request at the end, it is denied despite having an approval in the history, because the share count exceeds the threshold from the Cedar expression. Counting: how many times Another class of common policies requires knowing not just that something has happened in the past, but how many times it has happened. The simplest is a plain count of all the times an event occurred in some window. These can be used to write rate-limiting policies. For example, “no more than five transfers in an hour, however small each one is”, can be expressed as follows: // Forbid a transfer once five have already // gone out in the last hour. forbid ( principal, action == AgentCore::Action::"Transfer", resource ) when temporal { count_within(1h, AgentCore::Action::"Transfer"::request{ input.amount: _ }) > 5 }; As the name suggests, this count_within will count over the last hour (1h) every Transfer request — the _ is a wildcard that says we don’t care about the amount, just that it happened — and compare the count to five. This leads to the following verdicts on this event trace: @0 Transfer::request { amount: 20 } -> ALLOW // 1st transfer @60 Transfer::request { amount: 20 } -> ALLOW // 2nd @120 Transfer::request { amount: 20 } -> ALLOW // 3rd @180 Transfer::request { amount: 20 } -> ALLOW // 4th @240 Transfer::request { amount: 20 } -> ALLOW // 5th @300 Transfer::request { amount: 20 } -> DENY // 6th in the window exceeds limit Counting distinct things Sometimes the count you want is not of events but of distinct values across them: not “how many transfers” but “how many different recipients.” For example, we can express “an agent may make transfers to at most three distinct recipients in an hour”: // Forbid a transfer that would make it the fourth distinct // recipient paid in the last hour. forbid ( principal, action == AgentCore::Action::"Transfer", resource ) when temporal { count_distinct_within(u, 1h, AgentCore::Action::"Transfer"::request{ input.user: u }) > 3 }; Here the recipient is bound to u, and count_distinct_within counts the distinct values of u seen in the window — so paying the same recipient twice counts once, but a new payee bumps the tally. We can see what happens when we have five transfers to bob, carol, dave, erin, then bob again: @0 Transfer::request { user: "bob" } -> ALLOW // 1 distinct recipient @60 Transfer::request { user: "carol" } -> ALLOW // 2 @120 Transfer::request { user: "dave" } -> ALLOW // 3 @180 Transfer::request { user: "erin" } -> DENY // would be 4th distinct recipient @240 Transfer::request { user: " [truncated for AI cost control]