*Part 5 of An OS Where the AI Is Never a Principal.*
Four posts of argument. Now the work.
The thesis so far has been a sentence — the model is never a principal — and a pair of duals: bound what the agent can *do* (capabilities) and what it can *know* (label the turn, not the token). This post is where the sentence becomes something you can run. Not a framework, not a diagram — the smallest slice of real code that makes a prompt-injected agent *structurally* fail to escalate and *structurally* fail to exfiltrate, with an audit trail that says exactly why.
It's about four hundred lines of TypeScript. You run it with pnpm demo. Let me walk you through what's actually in there.
The capability is the only way to act
Everything starts with one primitive: an unforgeable reference.
export interface Capability {
readonly id: string;
readonly kind: string;
readonly clearance: Clearance;
invoke(arg: unknown, ctx?: InvokeContext): InvokeResult | Promise<InvokeResult>;
}To hold one of these is to be permitted to use the effect it names. There is no other way to act — no global namespace to reach into, no ambient authority hanging in the air. This is the ocap rule from the companion Endo-and-Agoric series, and it descends straight from Mark Miller's E language: a capability is the unforgeable union of designation and authority.
Here is the load-bearing detail, the one that makes this whole thing work for AI: the model never receives a capability object. It only emits tool *names* — forgeable strings like "admin_delete_all". The trusted vat holds the actual references and resolves names to them. So "possession is authority" is enforced by the trust boundary itself. The model produces data; the trusted code holds the keys. A name is a wish. A capability is a key. The model only ever gets to make wishes.
The vat is the one membrane, and it runs two gates
An agent is a vat — a single-threaded turn loop that holds a cap set and forces every model-driven action through one chokepoint. That chokepoint, vat.act(), is where both halves of the design meet. Every action the model proposes is checked against two gates, and it must pass *both*.
Gate one — authority. Did the model name a tool the vat actually holds?
const cap = this.held.get(toolName);
if (!cap) {
this.record('resolve-fail', `'${toolName}' is not a held capability — naming is not authority`);
return { ok: false, blocked: 'no-authority', tool: toolName };
}This is the (a) axiom in three lines: naming is not authority. If there is no held cap to resolve to, there is nothing to invoke. The action doesn't fail a permission check — there's no permission to check, because the door doesn't exist.
Gate two — flow. Given everything this turn has *seen*, is this sink cleared to receive it?
const verdict = flowCheck(this.turnLabel, cap.clearance, endorsed);
if (!verdict.ok) {
this.record('flow-block', `${cap.kind}: ${verdict.reasons.join(' | ')}`);
return { ok: false, blocked: 'flow', tool: cap.kind, reasons: verdict.reasons };
}Only if both gates pass does the effect fire — and then its result label is *absorbed* back into the turn, so the turn's contamination only ever grows. The whole loop is maybe thirty lines. That's the entire control plane.
The headline demo: two attacks, two structural deaths
pnpm demo runs a scripted oracle (src/oracle.ts) playing a model hijacked by a malicious web page — the canonical prompt injection. It tries two things.
Attack one: escalate. The injected plan calls admin_delete_all. The vat looks it up in its held set, finds nothing, and refuses. There is no admin cap in this agent's possession, so the name resolves to nothing. Blocked by the (a) axiom — not detected, not classified, just *absent*. The audit line reads resolve-fail: 'admin_delete_all' is not a held capability.
Attack two: exfiltrate. This is the subtle one, and it's where the second axis earns its keep. The agent legitimately holds a read_customer_db cap and a send_external cap — both granted, both fine on their own. The injection's move is the classic combination from doc 04: read the database, POST it to evil.com. Neither capability is the bug. The *flow between them* is.
So watch the turn label climb. The agent reads the attacker's page; the web-fetch cap stamps it untrusted-web, which joins into the turn. The agent reads the database; that data carries customer-db secrecy, which also joins in. By the time it reaches send_external, the turn's label carries *both* an untrusted taint and a customer-db secret — and the outbound sink is cleared for neither. The flow gate fails on both axes at once: confidentiality (it carries a secret the sink can't emit) and integrity (it's tainted and the action wasn't endorsed). Blocked.
The gate never looks at the payload — and that's the whole point
Here is the part people get wrong when they first build this, and the reason I want to spell it out.
The flow gate never inspects the arguments for the secret. It does not scan the POST body for database rows. That would be unsound — and not a little unsound, *fatally* so. A language model that has seen a secret is an active adversarial encoder: it can paraphrase the secret, imply it, or steganographically smuggle it into otherwise-clean text. Any literal-redaction check loses to "first letter of each sentence spells the key." You cannot win by reading the payload.
So you don't read the payload. You contaminate the turn. The instant a secret is absorbed, the *whole turn* is high — and every send from that turn is gated regardless of what the model actually put in the arguments. This is label-the-turn, not the token, made executable:
private absorb(l: Label, why: string): void {
this.turnLabel = join(this.turnLabel, l); // join = set-union, labels only rise
this.record('absorb', why);
}You don't try to catch the leak in the bytes. You make it so that a contaminated turn cannot reach an uncleared sink *at all* — encoded or not, clever or not. The soundness comes from refusing the channel, never from inspecting the message.
Structural and auditable — not proven
Every decision the vat makes is appended to an audit log: absorb, resolve-fail, flow-block, invoke-ok. That log is the honest claim. It is not a proof the agent *couldn't* misbehave — it's a precise, causal account of what it could touch, in which tainted turn, granted by whom, and why each action was allowed or blocked. "Structural and auditable" is the exact phrasing in the code, and the *not proven* is deliberate. The verified floor (seL4) comes much later in the ladder; here, the guarantee is structural confinement plus a trail you can read. Honesty cuts both ways.
The trap one level up: who decides the compartments?
There's a deeper problem the first demo doesn't show, and it's the one that almost makes the whole IFC story circular.
The clean way to prevent leaks is compartmentalization: don't put the secret-reading cap and the outbound cap in the *same* vat. A reader vat sees the secret but holds no exit; a sender vat holds the exit but never sees the secret. Task decomposition *is* information compartmentalization — one design move buys you both. Lovely.
Except the decomposition is *proposed by the untrusted model.* Left to it, a prompt injection just proposes a split that conveniently co-locates the secret and the exit in one vat. Compartmentalization can't be a model decision, or it's no decision at all.
So pnpm demo:compartments puts the decision where it belongs: in the trusted base. Before any topology runs, wire() checks a structural separation-of-duties invariant over the *whole flow graph* — no single vat may simultaneously hold a secret-labeled read cap and an uncleared outbound cap. Unsafe wiring is rejected at wiring time, before a single turn executes. And it catches the laundering chain too: a multi-hop route that tries to wash the secret through intermediate vats to reach the exit gets rejected, because the checker reasons over the transitive graph, not one edge at a time. The model proposes the compartments; the trusted base *guarantees* them. Without that check, every IFC claim in this series would be a model decision wearing a trusted-base costume.
What this is, honestly
It's TypeScript, written in SES-compatible patterns so lockdown() drops in cleanly — which is exactly what the next post does: turns these Object.freeze fallbacks into real tamper-proof hardening, adds a transitive revocable membrane, and shrinks the trusted surface to a four-method core. The default model here is a deterministic scripted oracle, so the security property stays testable offline — a real local model arrives two posts on, and the guarantees don't change when it does. That model-independence is the whole bet.
But the slice is real, and it runs, and the two attacks die the same way every time: one because the door was never there, one because the turn was already contaminated before it reached the exit. Not because we asked the model nicely. Because we never handed it the means.
End of Transmission.