# mcp-authority-boundary

**Correct mediation is not sufficient: separating enforcement, authorization-execution binding, and policy adequacy at the MCP tool boundary.**

Every test passed. The replay verifier said VERIFIED. The mediation invariant held. And a 100,000-byte write went through a policy that capped writes at 4,096 bytes.

That is not a story about a bug. It is the artifact's result. Authorization assurance has layers that fail independently, and the usual green signals cannot tell them apart.

---

## The controlled witness

One `write_document` call whose `content` argument is a one-element array holding 100,000 characters, against a policy that caps writes at 4,096 bytes. Two frozen versions receive the same call. An observer that imports nothing from this repository reads the file that was actually written and each version's ledger as plain text. This table is generated by `experiments/independent-observer/compare.mjs`:

| Version | Cedar | Ledger / replay | Independent world observer |
|---|---|---|---|
| v1 (`631196d`) | ALLOW (byteLen=0) | VERIFIED | 100,000 bytes written vs 0 authorized → DIVERGENCE |
| repaired (`7b7e973`) | REFUSE (unresolvable-resource; never reached Cedar as an allow) | INCOMPLETE (nothing executed) | no write |

- **Cedar's decision.** Cedar was asked about a 0-byte write and allowed it. That was the correct answer to the request it received. The request did not describe the operation, because the resolver and the executor read the raw argument separately and disagreed about it. Nothing here shows Cedar evaluating a policy incorrectly.
- **Why the internal signals stayed green.** Replay re-decides the *recorded request* with the same engine. The recorded request is the resolver's output, so the divergence sits upstream of everything replay can check. The v1 ledger has an intact hash chain and replays as VERIFIED.
- **What detected it.** `experiments/independent-observer/observe.mjs` (sha256 `889cf7a2…0bd0`, pinned in `experiments/hardening/RESULTS.json`) imports only `node:fs`, `node:path` and `node:crypto`. It sees a 100,000-byte file (sha256 `d69e6898…42e5d4`) where the ledger records an authorized length of 0.
- **The repair** (`c3f7ade`; `7b7e973` is the repaired base used above). Every argument is validated once into one immutable `ResolvedOperation`. The Cedar request is derived from that operation, the grant is bound to `sha256(operation)`, and execution receives the operation, never the raw arguments. The malformed call is refused before Cedar is consulted. See [Why A1 matters](#why-a1-matters) and [docs/REPAIR.md](docs/REPAIR.md).
- **Reproduce.** See [VERIFY.md](VERIFY.md). Building the two frozen versions needs network access for `npm ci`; the comparison itself runs offline in seconds.
- **Where it has been reproduced.** On the author's MacBook (2026-09-10, and on 2026-09-23 from a fresh clone of the public repository at `3ccac8a`), and in [GitHub Actions run 34483375841](https://github.com/repowazdogz-droid/mcp-authority-boundary/actions/runs/34483375841) on a GitHub-hosted Ubuntu runner at `3ccac8a`. All three runs produced the same effect sha256 and the same observer sha256. In each run, all three roles (input source, system under test, observer) ran on a single host. The three-host procedure is documented but no run of it is recorded here.
- **Formal status.** `formal/Boundary.lean` proves, for an abstract transition system, that every reachable execution has a grant whose request is derived from the operation and allowed, and that a grant executes at most once. Removing the single-use premise yields a double-spend trace. A further theorem checks only the arithmetic behind the v1 witness: the size budget admits a 0-byte request and rejects a 100,000-byte one. The file prints axiom reports for these five theorems, and they list only `propext` and `Quot.sound`, with no `sorryAx`. `formal/Conformance.lean` checks recorded TypeScript traces against that model (39 traces). **This is a trace check, not a refinement proof.** Nothing establishes that every execution of the TypeScript implementation is a model transition.

### Limits to read before citing the witness

- **Observer independence is in imports, not in custody.** The harness exports v1's in-memory effect to disk, and the observer reads that export. `test/observer-export.test.ts` checks that the two are byte-identical, but a process that controls the harness controls the export.
- **The observer reads final state.** A write that happens and is then reverted before observation is missed. The hardening campaign keeps this as a labelled negative control (`transient-extra-write`, `knownMiss`).
- **The scope is one MCP tool-call boundary in one server with one authored policy set.** Nothing here tests GUI or computer-use agents, other policy engines, or how often this occurs in other codebases.
- **The failure class is not new.** Two components interpreting the same input differently is a long-known class (for example MITRE CWE-436, *Interpretation Conflict*). What this repository offers is a small executable instance at an agent tool boundary, with the evidence that separates the internal signals from the observed effect. It does not claim a new vulnerability class.
- The full list is [docs/LIMITATIONS.md](docs/LIMITATIONS.md) (L1–L11).

---

## Abstract

Authorization at an AI agent's tool boundary is usually treated as one property: either the policy engine is in the path or it is not. This artifact separates it into properties that fail independently. A Cedar-enforced Model Context Protocol server mediates six tools across 25 adversarial scenarios, recording every decision in a hash-chained ledger with an independent replay verifier.

The first version passed 66 tests, replayed as VERIFIED, and satisfied a checked complete-mediation invariant, while a 100,000-byte write executed under a 4,096-byte policy limit. The resolver measured the payload as a string and substituted zero bytes for a non-string; the executor coerced the same argument and wrote it. Both read the raw input independently, so the engine authorized a request that did not describe the operation.

The repair binds execution to one validated immutable operation. Later hardening closes the A2 delegation and A6 SQL defects, adds write-ahead logging and trace proofs, and tests real file effects with a separate observer. Permitted-but-harmful scenarios still show that enforcement correctness does not establish policy adequacy.

## Current hardening experiment

Run `npm test`, `npm run test:formal`, and `npm run experiment:hardening`.
`npm run test:conformance` runs the suite and the hardening campaign with `MAB_TRACE=1`
and has Lean check every emitted grant transition against the transition system in
`formal/Boundary.lean` (`formal/Conformance.lean`). That is a trace check over the runs
taken, not a refinement proof; its header says exactly what it does and does not cover.
The [experiment guide](experiments/hardening/README.md) explains the controls and trust boundaries.
[RESULTS.json](experiments/hardening/RESULTS.json) records the latest measured outcomes and source hashes.
Historical tables below refer to their named commits; they are not measurements of the edited tree.

---

## Four properties, which fail separately

The point of this repository is that these are four claims, not one.

| | Property | Status here |
|---|---|---|
| **A** | **Mediation.** No mediated tool executes without an `allow`. | **Established** |
| **B** | **Binding.** Execution consumes the same canonical operation Cedar authorized. | **Established.** Did not hold in v1. |
| **C** | **Policy adequacy.** The policy expresses the authority its author intended. | **Not established.** A2/A6 are fixed; authored tests do not establish intent. |
| **D** | **Effect verification.** The recorded effect matches the authorized operation. | **Not established by the default scenario evidence.** Its eight effect checks remain record-consistency. The separate [hardening campaign](experiments/hardening/README.md) supplies real-file write/delete controls and injected failures, with a separate observer and explicit scope. |

### Correction to v1.0.0

Released v1.0.0 stated claim D as *"Effect verification. The observed effect matches the authorized operation — Established for the fixture tools only"*, and its replay output reported that *"the effect observed in the world after execution matches the authorized operation"*. Both overstated the evidence.

Independent fixture read-back is implemented only for `write_document` and `delete_file`, and the v1.0.0 ledger executed neither: its seven stage-4 checks were `read_document` ×5, `execute_shell` ×1 and `send_email` ×1. Every stage-4 check shipped in v1.0.0 was therefore record-consistency, not independent effect observation.

Claims A, B and C are unaffected and stand as released. Corrected 2026-08-14. Current claim D status is in the table above; the detail is in [docs/LIMITATIONS.md L7](docs/LIMITATIONS.md), and `test/evidence-composition.test.ts` now fails the build if this combination recurs.

### Correction to v1.0.0: session establishment

Released v1.0.0 read the principal as `process.env['MCP_SESSION_ID'] ?? 'sess-alice-root'`. A launcher that omitted the variable therefore did not fail; it ran as `sess-alice-root`, the highest-authority session in the entity store. An unknown session id already failed closed, so absence was the one input routed to maximum privilege rather than to refusal.

`MCP_SESSION_ID` is now required and has no default: an absent or blank value refuses startup with exit code 2, and an unrecognised one still fails closed at the first decision. **This does not add authentication, and it does not contain a hostile local actor who can spawn the process.** Whoever launches the server still chooses the session identity, and possession of the launch path remains equivalent to possession of any session named in it. Assumption A2 stands as written; the trust boundary is in [docs/ASSUMPTIONS.md](docs/ASSUMPTIONS.md).

Claims A, B, C and D are unaffected. Corrected 2026-08-17. 155/155 tests pass, including startup refusal for missing and blank identities, and unchanged enforcement under explicitly supplied admin and delegated sessions; `test/session-establishment.test.ts` fails the build if the default returns.

---

A held in v1 and B did not, which is the whole finding: **the gate can be perfectly enforced and still authorize the wrong thing.** A and B holding says nothing about C, and says nothing about what an authorized command does outside this boundary — scenario S24, and the section below.

---

## Why A1 matters

This is the intellectual centre of the artifact, so it comes before the architecture.

Version 1 had complete mediation in the strong sense. Tools were unreachable without a single-use grant that only the policy decision point could mint. The invariant "no tool result without an `allow`" was checked at runtime, again over the ledger, and again by the replay verifier. Sixty-six tests passed. Replay reported VERIFIED.

The following call, using nothing but tool arguments, wrote 100,000 bytes under a grant capped at 4,096:

```json
{"tool": "write_document",
 "args": {"path": "corp/public/notes.md", "content": ["xxxx… 100000 chars …"]}}
```

`content` is an array. Two code paths read it, and they disagreed:

- `resolve.ts` measured the payload with `typeof clean['content'] === 'string' ? clean['content'] : ''`, so a non-string became the empty string and `byteLen` became 0.
- `tools.ts` executed `String(a['content'] ?? '')`, which coerced the array into a 100,000-character string and wrote it.

Cedar answered correctly. It was asked about a zero-byte write, and `forbid-oversized-write` does not fire on zero bytes. The engine, the policy, the grant and the ledger were all working. The request simply did not describe the operation.

Nothing in the verification apparatus could see this. The replay verifier re-decides the **recorded request**, and the recorded request is the resolver's output, so the resolver sits upstream of everything replay can check. A ledger containing this bypass replays as VERIFIED with an intact hash chain. That probe is preserved as a test.

**The repair is structural, not a filter.** Rejecting arrays would have closed one input and left the class open. Instead there is now exactly one place where an argument becomes a validated value, one immutable `ResolvedOperation` carrying every security-relevant value, and an execution layer with no access to the raw arguments at all. `executeTool(op, grant)` takes no `args`, and a test asserts over the source text that `src/tools.ts` contains no reference to raw arguments and performs no coercion. The grant is bound to `sha256(operation)` and re-checked at execution time.

The test that separates a structural repair from a patch is `F1`: ten non-string types across ten string-valued fields across six tools, 100 combinations, every one required to fail closed before Cedar is consulted. A filter on arrays passes one of those and fails 99.

---

## Architecture

```mermaid
flowchart TD
    subgraph UNTRUSTED["UNTRUSTED - attacker-controlled"]
        A["Raw MCP call<br/>tool name + arguments"]
    end

    subgraph SERVER["MCP SERVER PROCESS - trust boundary"]
        B["Validation and canonicalisation<br/>reject wrong types, never coerce<br/>NFC, traversal, control chars"]
        C["ResolvedOperation<br/>immutable, deep-frozen<br/>carries every execution value"]
        D["Cedar request<br/>DERIVED from the operation"]
        E["Cedar decision<br/>allow / deny + determining policy ids<br/>anything else maps to DENY"]
        F["Grant bound to sha256 of the operation<br/>single use, minted only by the PDP"]
        G["Execution<br/>consumes the operation, no raw args"]
        H["Effect record<br/>read back (2 tools) or<br/>derived from the operation (4)"]
    end

    subgraph EVIDENCE["EVIDENCE - after the fact, prevents nothing"]
        I["Hash-chained ledger"]
        J["Replay verifier<br/>4 separately reported stages"]
    end

    A -->|"session, clock, policy and entity store<br/>come from the host, never the model"| B
    B --> C
    C --> D
    D --> E
    E -->|allow| F
    E -->|deny| I
    F --> G
    G --> H
    H -->|"mismatch throws"| G
    H --> I
    I --> J

    style UNTRUSTED fill:#3a1f1f,stroke:#c0554d,color:#f0e6e6
    style SERVER fill:#1f2d3a,stroke:#4d8ac0,color:#e6ecf0
    style EVIDENCE fill:#2a2a2a,stroke:#888888,color:#e8e8e8
```

The gate sits inside the server, in front of tool dispatch, rather than between the client and the server. A check the calling process performs on itself is a check the calling process can decline to perform, and the agent chooses which client code runs. Scenario S14 is the negative control: a client that speaks raw JSON-RPC and imports none of this repository's client code gets the identical denial.

---

## Results

| | v1 `631196d` | Adversarial audit `5d55d20` | Repaired `c3f7ade` |
|---|---|---|---|
| Scenarios | 24 | 24 | 24 |
| Ledger entries | 26 | 26 | 26 |
| Determining-policy coverage | 15/15 | 15/15 | 15/15 |
| Policies (base + overlay) | 14 + 1 | 14 + 1 | 14 + 1 |
| Tests | 66 pass | 80 pass (66 + 14 probes) | 100 pass |
| Mediation invariant | HOLDS | HOLDS | HOLDS |
| Replay | VERIFIED, one verdict | VERIFIED, with A1 live | 4 stages, all PASS |
| 4,096-byte write limit | **bypassed, 100,000 bytes written** | witness exhibited | blocked before Cedar |
| Live-session expiry | never fired | witness exhibited | fires, no restart |
| Revocation flipped on disk | ignored by a running process | witness exhibited | next decision denies |

The three columns are tagged historical states. Subsequent additions and the current hardening experiment change no earlier column. Current counts belong to the generated reports and test output, not this historical table.

Counts are over an authored scenario set written by the same person who wrote the policies. They describe this artifact and estimate nothing about attack prevalence, real-model behaviour, or any other policy set. The measurement frame is in [docs/EVIDENCE.md](docs/EVIDENCE.md).

---

## What this establishes

> For every mediated tool execution, the operation executed is the same immutable, type-validated, canonicalised `ResolvedOperation` from which the Cedar request was derived, verified at execution time by digest comparison. No mediated tool executes without an `allow` under the policy version and entity-store state recorded alongside it, both read at decision time.

**Assumptions.** The server process, policy files, entity store, session binding and clock source are outside the adversary's control. Cedar is correct. Every addressable resource is enumerated in advance. Effects are simulated against an in-process fixture. The adversary does control the model completely, the content of every resource, the MCP client, and every tool argument.

## What this does not establish

- **Cedar correctness.** Every decision is as sound as `@cedar-policy/cedar-wasm` 4.12.0. Replay re-runs the same engine, so it cannot detect an engine fault.
- **Policy adequacy.** The historical A2 and A6 witnesses now have regression fixes: both edges of an admitted depth-two delegation chain are checked, and database queries must parse as the supported read-only SELECT language. These fixes do not establish that policies express their author's intent. S18 and S24 remain permitted-but-harmful controls.
- **Arbitrary real-world side effects.** No shell command runs, no mail is sent, no database is queried. Claim D is scoped to a fixture world with no symlinks, races, partial writes or permissions; for four of the six tools the recorded effect is derived from the operation rather than read back at all, and the two tools that do read back are never executed in the shipped ledger.
- **The consequence of an authorized command.** Scenario S24 and the section below.
- **Exhaustive adversarial coverage.** 25 authored scenarios and 32 audit and falsification probes bound the search, not the world. No counterexample found is not no counterexample.
- **Production security.** There is no authentication. Session identity is bound from the environment at spawn.
- **Faithful logging.** Replay now reconciles write-ahead authorizations and completions, checks the end seal, and can use a verifier-held anchor. A co-located editable seal does not authenticate itself. A compromised host can fabricate records. The real-file campaign demonstrates both detected truncation and an extra write that only the independent observer catches.

---

## The boundary of the boundary

Scenario **S24** is the second permitted scenario, and it is in the demo output for the same
reason S18 is: it marks where the claims stop.

`execute_shell` is authorized on a non-production host by `permit-admin-tier`. The command
string denotes a consequence outside this boundary. `cedarRequestFromOperation` maps
`execute_shell` to `(action, Mcp::Host, byteLen 0, recipientDomain "")` — the command is not a
field Cedar receives, so the Cedar request for that call is *identical* to the request for a
benign command on the same host, and no policy in this set, present or future, can be written
against the difference. `test/external-effect.test.ts` asserts that identity, asserts that both
calls draw the same verdict from the real PDP, and asserts that claims A and B hold throughout:
nothing ran without an `allow`, and execution consumed the operation the grant was minted for.
The operation digests differ, so binding does separate the two calls — it binds execution to
the authorized operation, and the authorized operation is the one whose consequence is
unrepresented.

Nothing in the scenario performs network access. `execute_shell` appends to an in-process array
and returns `[simulated output]`; the domain is a reserved `.example` name and is never
resolved. What S24 exhibits is the representation gap, not an effect.

**The underlying limitation is prior work, and none of it is claimed here.** An enforcement
mechanism cannot constrain what it can neither observe nor control:

- **Schneider**, *Enforceable Security Policies*, TISSEC 3(1), 2000 — execution monitors
  enforce only safety properties. The biconditional is not his: he states that "the converse —
  that all safety properties have EM enforcement mechanisms — does not hold".
- **Basin, Jugé, Klaedtke & Zălinescu**, *Enforceable Security Policies Revisited*, POST 2012 /
  TISSEC 16(1), 2013 — partitions actions into controllable and only-observable, and
  characterises enforceability as `(U,O)`-safety: informally, "P is safety in U and bad things
  are not caused by an only-observable action". The command's consequence is such an action for
  this boundary.
- **Khoury & Hallé**, *Runtime Enforcement With Partial Control*, FPS 2015
  ([arXiv:1508.06525](https://arxiv.org/abs/1508.06525)) — generalises that partition to a
  lattice of control levels, with file and network operations as the worked examples, and shows
  the enforceable set grows monotonically as an action is moved to a level the monitor
  controls. Adding a lower-layer enforcement point is that move.
- **Ray**, *What Can Be Enforced? A Theory of Certified Runtime Safety for Tool-Using Agents*,
  2026 ([arXiv:2607.22868](https://arxiv.org/abs/2607.22868)) — the same characterisation for a
  pre-execution gate on agent tool calls, relative to a fixed vector of oracle predicates: what
  the gate cannot see, it cannot enforce.

**What this repository adds is an executable demonstration.** S24 and its tests are a running
instance in which complete mediation and authorization-execution binding both hold, every test
passes, the four replay stages all report PASS, and the containment inference still does not
follow. The proposition is not this artifact's; the witness is.

## Reproduce

```bash
git clone <this repo>
cd mcp-authority-boundary
npm install
./run.sh
```

Node 20.11 or newer. No API key and no network after `npm install`. The clone must have full history (not shallow), because two tests rebuild `631196d` from git. The run takes well under a minute on an M-series laptop. The hardening campaign additionally needs Python 3 with `sqlite3`, and the formal checks need Lean 4.33.1; both are listed in [VERIFY.md](VERIFY.md).

You should see 25 scenarios, each printing the tool call, the decision, the determining Cedar policy ids and a ledger position; an unmediated baseline showing what those same calls would do without the authorization layer; then four replay stages reporting separately:

```
chain-integrity      PASS   checked 27  n/a  0  failures 0
policy-replay        PASS   checked 27  n/a  0  failures 0
auth-exec-binding    PASS   checked 25  n/a  2  failures 0
effect-consistency   PASS   checked  8  n/a 19  failures 0
```

then the passing regression suite. Stages are reported separately. Intent reconciliation and seal checks can now detect changes alongside the operation/effect stages. [docs/QUICKSTART.md](docs/QUICKSTART.md) has the commands.

The ledger and intent journal are deterministic for a fixed source, policy and fixture version.
Changing those inputs changes the evidence hashes; historical hashes must not be presented as current.

---

## Layout

```
policies/          Cedar schema, 14 base policies plus a 1-policy revocation
                   overlay. Read this first; the TypeScript exists to put
                   requests to it.
entities/          sessions, scopes, documents, mailboxes, tables, hosts
src/               ~2500 lines of code. resolve.ts is the correspondence layer
                   and the place A1 lived; mediation.ts holds the grant machinery.
test/              the regression suite (182 tests at 3ccac8a; run `npm test`), including 17 audit probes (the original 14
                   witnesses, several now split into before/after pairs), a
                   15-probe post-repair falsification sweep,
                   external-effect.test.ts, which pins the S24 boundary, and
                   evidence-composition.test.ts, which guards claim D against
                   the ledger's actual per-tool composition
docs/              architecture, threat model, assumptions, limitations,
                   evidence, audit, repair
evidence/          committed, and regenerated byte-identically by ./run.sh
```

| Document | What it is for |
|---|---|
| [ARCHITECTURE.md](docs/ARCHITECTURE.md) | why the gate sits behind the transport, and the binding pipeline |
| [THREAT_MODEL.md](docs/THREAT_MODEL.md) | what the adversary controls, and what is out of scope |
| [ASSUMPTIONS.md](docs/ASSUMPTIONS.md) | the trusted base, stated as premises |
| [LIMITATIONS.md](docs/LIMITATIONS.md) | eleven limitations (L1–L11); read before citing |
| [EVIDENCE.md](docs/EVIDENCE.md) | the numbers and their measurement frame |
| [AUDIT.md](docs/AUDIT.md) | the adversarial review that falsified the v1 claim |
| [REPAIR.md](docs/REPAIR.md) | what changed, and why it is structural rather than a filter |
| [ATTACK_MATRIX.md](docs/ATTACK_MATRIX.md) | scenario to policy mapping, and what is out of reach |

## Prior and adjacent work

Cedar is Amazon's open-source policy language. MCP is Anthropic's Model Context Protocol. Neither is claimed here. The MCPSecBench class references in the attack matrix are this author's reading of that benchmark's taxonomy; the benchmark is not run and no score against it is claimed. `mcp-assurance-lab` is a separate earlier artifact by the same author, in Python with hand-written policy predicates; this repository is not a port of it.

No novelty claim is made about the layering. Complete mediation is Saltzer and Schroeder, 1975. What is offered is a small executable artifact where the layers come apart in a way you can run.

## License

Apache-2.0.