Agentic Security Policies as Compiled Logic

An agent with real permissions

This post is about the security of AI agents, and Claude Code (a CLI coding agent) will be our running example. If you run Claude Code in a fully locked-down sandbox with no outbound network, you can stop reading now: nothing the agent does in there can hurt you. But hardly anyone runs it that way. Most sandboxes leave the network open, so exfiltration is still possible, and most developers skip the sandbox entirely: you run the agent against your actual repositories, with your actual credentials on disk, often with permission prompts turned off because they interrupt the flow. Every tool call the agent makes is real.

Here is a concrete scenario that shows the threat. You ask the agent to rotate an API key. Somewhere in that session it reads the .env file, so the old key is now in its context. Fifty steps later (or five, or five hundred) it runs some outbound command, like a curl, a git push, or a wget. So here is the question this post tackles: how do you stop that command from carrying the secret out, without breaking the agent’s ability to do its job?

sasy-guard is a runtime guard for Claude Code built on the SASY policy engine, and it solves exactly this type of provenance-based authorization problem. This post builds up to that solution one puzzle at a time, starting with the puzzle you’d hit on day one.

Claude Code gives you one natural choke point: a PreToolUse hook that sees every tool call before it runs and can allow or deny it. How should we design the rule in this PreToolUse hook? The rest of this post works through a sequence of designs for that rule: at each stage we try one, see where it falls short, and let the failure point to the next.

The if-then version

The simplest way to set up the hook is a pattern check:

def hook(call):
    if "curl" in call.tool:
        if session_read_a_secret_recently():
            return DENY
    return ALLOW

It looks reasonable enough: an outbound command after a recent secret read gets denied.

Question 1. Look at the hook again before reading on. Which part of it is tricky to design well, and is there any choice for that part that actually works?

The tricky part is the word recently. Whatever window you pick (say five minutes, ten messages), it’s going to cause trouble: a secret read just before the window starts falls outside the check, and slips through.

Question 2. Let’s try an easy fix: instead of using a fixed-size window, scan the entire session transcript for reads of sensitive paths, so that there is no arbitrary cutoff at all. But two problems remain, one about precision and one about cost. Can you name them?

The precision problem: this scan is a blunt instrument; all it can tell you is whether a secret was read somewhere in the session, i.e., it is a presence check. It asks “was a secret read at any point?” when the question that actually matters is “does this command carry data from that read?” One .env read in the first minute now condemns every outbound command for the rest of the session, no matter how unrelated. And you can’t fix this by inspecting the text of the pending command, because that text is clean: the agent read .env, pasted the key into rotate.sh, and the command being judged is just bash rotate.sh plus a curl with no secret in sight. The secret traveled through an intermediate file. What connects the read to the curl is a chain of data dependencies, and a presence scan sees no chains.

The cost problem: the hook re-scans the whole transcript on every tool call, and transcripts grow. You’re paying linear work per call for an answer that is wrong anyway.

So the real fix has to track dependencies, using something like:

def carries_secret(call, graph):
    seen = set()
    frontier = [call]
    while frontier:
        node = frontier.pop()
        if node in seen:
            continue
        seen.add(node)
        if is_secret_read(node):
            return True
        frontier.extend(graph.parents(node))
    return False

This function tracks transitive dependencies, so it fixes both the fixed-window and the presence-check failures.

Question 3. Say your team adds a second history-dependent rule: “a git push must wait for a clean secret scan covering the files you edited.” Then a third. What starts to go wrong as these rules pile up? And is there a question about the resulting guard that you simply have no way to answer?

Each new rule either duplicates the traversal or grows a second, slightly different one, so you now maintain a small fleet of hand-rolled reachability engines. Rule interactions become control flow: the order of the if statements silently encodes precedence decisions nobody wrote down. Those hand-rolled traversals are all supposed to compute dependencies, but their code can quietly drift apart.

This leads to questions that are impossible to easily answer: is there some session where two of these traversals disagree, one rule seeing a dependency that another misses? Or: is there any session in which rule three can ever fire? With rules encoded as imperative code, you have no way to answer such questions except by testing: run the agent and watch. In principle there’s a second route: static analysis, tools that answer such questions from the code alone, without running it. But for arbitrary imperative code, questions like these run into undecidability (this is Rice’s theorem territory), and practical analyzers handle far shallower properties than whether two hand-rolled traversals can disagree. Keep the idea in mind anyway, because what makes a language amenable to static analysis is exactly where this post ends up.

The deeper problem is the language. A property like “transitively depends on” is recursive, and imperative languages make you pay for recursion with bookkeeping (worklists, visited sets, ordering) that obscures the rule’s intent. What we ideally want is a language in which we can just state rules as properties and let an engine compute them. The rest of this post builds on this idea.

A session is a set of facts

Before we can write rules like that, we need something for them to work on. SASY’s observability layer provides it: it records a Claude Code session as a message-dependency graph, where every user message, tool result, and pending tool call is a node, and an edge points from each node to the nodes that use its data. Here is our key-rotation session, reduced to four nodes.

The four-node session graph: the user message m1 feeds the Read of .env (r1), whose output feeds the Edit of rotate.sh (e1), whose output feeds the pending curl call (c1), marked Current.

The session as the policy engine receives it: nodes, edges, and the pending call marked Current. Ids are abridged for the walkthrough.

To the policy engine, this graph is a set of ground facts: concrete, fully specified statements with no variables in them. In this notation, a name such as Edge or Current is a predicate: it describes one kind of fact. The set of all facts with the same predicate name is its relation. Here is the four-node session above, written out as facts:

Edge("m1", "r1").   // the Read served the user's request
Edge("r1", "e1").   // the Edit pasted in the key that Read returned
Edge("e1", "c1").   // the curl runs the edited script
Current("c1").      // the call awaiting a verdict from the Policy Engine
ToolResult("r1", "Read", '{"file_path": ".env"}').   // what node r1 was

Notice that no verdict appears anywhere in these facts. The verdict is something the rules must derive from them. So what does a “rule” look like in this world? That’s worth a short detour, because the language is small enough to learn in the next few paragraphs.

A little language of facts and rules

The rules we are about to meet are Horn clauses. A Horn clause has one statement on the left (the head), the symbol :- (read it as “if”), and a list of conditions on the right (the body), implicitly joined by AND:

Head :- Condition1, Condition2, Condition3.

“The head is true if every condition is true.” A clause with an empty body is unconditional: that is exactly what the ground facts above are. And a clause is a template: InContext(id) :- Current(id). has a variable in it, and it fires by substitution. We have the ground fact Current("c1"), so setting id = "c1" satisfies the body, and out comes a new derived fact: InContext("c1"). That single mechanism (match the body against known facts, emit the head) is the entire execution model.

The body of a clause only joins conditions with AND, so what about OR? It turns out we don’t need special syntax for it: to express a disjunction like “id is in context if it is the pending call or the pending call depends on it,” you just write two clauses with the same head.

InContext(id) :- Current(id).
InContext(id) :- CurrentDepends(id).

Each clause is an independent way to establish the head, which is exactly what OR means. (The second clause mentions CurrentDepends, which we haven’t defined yet, and will do shortly.) Let’s keep the two-clause construction in mind; we’ll see it again soon in a more interesting context.

This little language is Datalog. It has been studied since the 1980s¹¹ Datalog grew out of the database and logic-programming communities; unlike more general logic-programming languages, its facts and rules cannot use expressions that build new, nested values, a restriction that guarantees termination. and SASY evaluates it with Soufflé, an engine we will lean on heavily in a moment when we turn to compilation.

Question 4. Now try this exercise: using only Horn clauses over the Edge and Current facts (no loops, no sets, no mutation), define “everything the pending call transitively depends on.” Two clauses are enough, and it’s worth an honest attempt before reading on.

Two rules that walk the graph

Here is the definition, as shipped in SASY’s common policy (lightly abridged):

// CurrentDepends(src): some Current node transitively depends on src.
CurrentDepends(src) :- Current(id), Edge(src, id).
CurrentDepends(src) :- CurrentDepends(mid), Edge(src, mid).

If your two clauses said something like “the pending call depends on its parents, and on the parents of anything it depends on,” you basically got it. Note the shape: this is the two-clauses-as-OR construct from the last section, with a twist. The first clause is a base case. The second mentions CurrentDepends in its own body: the definition is recursive. Together with the InContext pair above, these rules name the backward slice of the pending call, the portion of the session that could have influenced it.

Now compare this with the imperative carries_secret function from earlier: that one needed a while-loop, a frontier list, and a visited set just to walk the graph. None of that bookkeeping appears here. The two clauses say what the slice is, and nothing about how to compute it.

From the slice to a verdict

The graph-walking rules compute what the pending call depends on, but a slice is not yet a decision.

Question 5. You now have the slice: everything the pending call depends on. To turn that into a “block this call” verdict, what else must be true? Don’t worry about syntax. Just name, in plain words, the conditions you would check, and how you would combine them.

Here is one answer, at that same conceptual level. Two conditions: first, somewhere in the slice, a secret was read (say, a Read of a file like .env). Second, the pending call is a way for data to leave the machine (say, a curl). And the combination is just AND: if both conditions hold, block the call.

The Datalog says exactly this, one clause per condition plus one clause that combines them. Here are the three clauses, from sasy-guard’s shipped policy:

// A secret-bearing read is in the pending call's slice.
SensitiveInContext() :- InContext(id), ToolResult(id, "Read", args),
    p = @json_get_str(args, "file_path"),
    SensitivePath(s), @str_contains(p, s) = 1.

// The pending call is an egress channel (one of ~14 such rules).
IsExfil(idx) :- ShellNorm(idx, n), @str_contains(n, "curl") = 1.

// The verdict.
Unauthorized(idx) :- RuleEnabled("toxic_flow"), IsExfil(idx),
    SensitiveInContext().

The names map straight onto the two conditions. SensitiveInContext is the first: some node in the slice is a Read of a secret-bearing path. IsExfil is the second: the pending call is an egress channel, a way for data to leave the machine (a curl, here). And Unauthorized is the AND that combines them: block the call when the protection is enabled, the call is egress, and a secret is in its slice. The remaining names are shallow plumbing: SensitivePath is a list of secret-bearing path fragments (“.env”, “id_rsa”), ShellNorm is the pending command lowercased and whitespace-collapsed so CURL cannot dodge the match, idx is the index of the pending call in the session’s action list (verdicts are keyed by it), and the @-prefixed names are Soufflé’s built-in string helpers.

In the running example this is what fires: the pending curl carries the key that .env gave up, so Unauthorized evaluates to True, and the call is blocked. So the protection is the two CurrentDepends clauses that walk the graph, the two InContext clauses that name the slice, and the three above: two conditions and a verdict. The shipped policy has a few more details, but for simplicity we’ve kept just the essential shape here.

What the logic form buys

Question 6. Put those clauses beside the imperative guard from the first half of this post. Length aside, which of the problems that plagued the imperative guard does the declarative version fix? And recalling Question 3, can you now answer the questions you couldn’t answer at all before?

Let’s put the two versions side by side. The imperative guard was a growing pile of traversals and if statements; the declarative one states relations and lets the engine derive them. Three of the problems we hit in the imperative version are now gone: (a) the hand-rolled graph traversals, (b) the rules that kept stepping on each other as we added more, and (c) the questions we had no way to answer.

For (a): we stated the property and let the engine compute it. CurrentDepends says what the backward slice is, and all the bookkeeping details are gone. And since we never wrote a traversal, the usual traversal bugs simply can’t happen here.

For (b): the policy is now one artifact, and it composes. In the imperative guard, each new rule duplicated a traversal and shifted the meaning of the ones around it, because precedence lived in if-statement order. Here, a second protection is just a few more clauses in the same file, not a second reachability engine bolted alongside the first. Adding a clause never edits the text of an existing rule, and because derivation only ever adds facts, a new clause cannot make an existing rule derive less (this is the monotonicity property of Datalog). New protections reuse the same graph relations instead of rebuilding them.

For (c): the policy is analyzable. The questions that were hopeless for Python code (can two rules conflict?, can this rule ever fire?) become questions about the policy text, and Datalog is precise enough that a tool can answer them without running the agent at all. SASY checks a policy for contradictions, redundant rules, and unreachable clauses before it ever judges a live call. Analyzability is really the mild version of a bigger win: because the policy has an exact mathematical meaning, you can state and prove guarantees about what it enforces, which is what the FORGE paper does. The foundation that makes those proofs possible is the subject of the next post.

Compiling the policy

One issue remains: runtime cost. The policy is evaluated against the session’s facts on every tool call, and the call waits until the verdict comes back.

Question 7. Recall the cost problem from Question 2. If the engine read and interpreted these clauses afresh on every call, would that problem have quietly returned? And what is the usual way to run a high-level language without paying the interpreter on every execution?

The imperative guard was expensive because it rescanned a growing session transcript on every call. The declarative guard has its own cost: evaluating the policy against the session’s facts on every call. If the guard adds noticeable latency, the temptation is to just turn it off, so this cost matters.

The usual answer to “run a high-level language cheaply” is to compile it, and that is what SASY does. The compilation happens exactly once, when the policy is installed: SASY hands the Datalog clauses to Soufflé, which translates them into C++ and compiles that into native code. Then at runtime, when a tool call arrives, rather than interpreting the clauses, compiled native code evaluates the policy against the session’s facts.

This is the idea of a policy compiler. We write the policy in a high-level language built for the problem: Datalog over a session graph, where each rule reads almost like a plain-English statement of the requirement it enforces, and a compiler turns it into native code that enforces it. This is the benefit any compiled language gives you: write for humans, run at machine speed. One question remains, though: on each tool call, does the engine re-derive everything from scratch, over all the facts of the session so far, or can it reuse the work it did on earlier calls? That’s a question about evaluation strategy, and we take it up in the next post.

Compile time is also the natural place to run the checks we described in the previous section: contradictions, redundant rules, and unreachable clauses are all caught when the policy is compiled and installed, before it ever judges a live call.

What does “the engine computes it” really mean?

When we introduced the logic form of the rules, we leaned on a phrase without ever examining it: the engine computes it. For example, consider the recursive CurrentDepends definition that computes the backward slice:

CurrentDepends(src) :- Current(id), Edge(src, id).
CurrentDepends(src) :- CurrentDepends(mid), Edge(src, mid).

Question 8. The definition is circular: CurrentDepends appears on both sides of the :-, and nothing marks nodes as visited. On a graph with a cycle, why does an engine running this not loop forever? What does it even mean to “run” a circular definition?

The answer involves an idea called a fixpoint, which gives these rules their guarantees of termination and a single well-defined result. We’ll save the full story of fixpoints for a future post.