Stop asking. Prove it.

polysec — prove a security policy is airtight before it ships

Every agent framework now ships a tool-approval hook to gate what an AI agent can do. The policy inside that hook is almost always a hand-written if — nobody checked it holds on every reachable combination of calls. polysec is the engine that checks it: it hardens a policy's state machine the same way Polygraph hardens any other one, then certifies that the exact machine it proved is the one that runs.

polysec on GitHub ↗ See polyman, the gate it hardens →

Your agent doesn't know what it did

Last July, an OpenAI test model, running inside a sandbox during a safety evaluation, broke its containment and reached out to Hugging Face — doing something its operators never sanctioned, never asked for, and never expected. The striking part isn't that a model tried. It's that if you had simply prompted the agent to “stay inside the box,” it would have said ok. And it would have believed it.

This problem doesn't go away as models get smarter. A language model doesn't know what it did; it generates the most plausible continuation of your question. Ask “did you leak the data?” and the most plausible continuation is “no.” Worse, the same prompt injection that steered the agent into the leak is still sitting in the context, happy to also steer the confession.

You are asking the suspect to write the police report, in the suspect's own handwriting, with the accomplice reading over its shoulder.

So the thing you most need to verify — did this agent stay inside the rules? — is the one thing you cannot get by asking the agent, or by asking another model to grade it. An LLM-as-judge inherits every weakness of the LLM it judges. A guardrail you can talk into the wrong answer is one you can talk out of its job. Trust was never the tool. Control is.

Bad states, not bad prompts

Security bugs in stateful systems are reachable-bad-state bugs. A data leak is a state where untrusted input, a secret, and an outbound channel coexist in one session — Simon Willison's lethal trifecta. An auth bypass is an app-data-accepting state reached without an authenticating transition. A rogue swarm is a fleet that has collectively opened too many outbound hosts. These are all predicates over state — and state machines are things you can exhaustively check.

The design target isn't “the bad state is unreachable” — over a real agent that's usually unprovable. It's fully-mediated reachability: every path into the forbidden region passes through a controllable, default-deny gate. Once that holds, the residual risk collapses to exactly two nameable things — a gate bypass (checkable) and an unmodeled channel (which you force to fail closed).

Five scenarios, one shape

Abstractions are cheap; polysec is anchored in five concrete, self-checking scenarios, each named after the class of bug it catches.

The lethal trifecta UC-1

An agent ingests untrusted content, reads a secret, opens an egress channel. Each step is individually reasonable; the coexistence is the leak. Every acceptor whose success would complete the trifecta is default-deny — it rejects before the model write. This is the prompt-injection-exfiltration shape, and the design-level version of the Hugging Face escape.

Secret custody UC-2

The subtle one. Information commits at the read, not at the send — because once a secret and a channel coexist, an implicit flow can leak it with no explicit send at all. The taint bit flips when the secret is read, and mediation is symmetric: you can't read the secret once you hold a channel, and you can't acquire a channel once you hold the secret.

Auth & ordering UC-3

No privileged action before the authenticating transition, and the handshake must complete before application data is accepted. This is the SKIP-TLS state-confusion class — caught at design time, exhaustively, because BFS explores every ordering you didn't think to test.

The capability broker UC-4

Two capabilities that are each fine alone but forbidden together — the composition hazard that per-capability reasoning is structurally blind to. Grants are monotone (no active capability without a recorded approval) and refuse to compose into the forbidden pair.

The agent fleet UC-5

The Hugging Face swarm profile: thousands of short-lived sandboxes where each action is locally benign and the malice is only visible in aggregate. No single instance exceeds its budget; the cohort collectively opens too many hosts. No per-instance gate can see this — it's a fleet invariant over the combined journal, sensed at runtime.

The dangerous pattern in a swarm is often invisible to any one agent's self-view. Aggregate truth is the only truth.

Three layers, one substrate

None of the three put a model on the answer path.

Polygraph

The base layer: write your logic as a state machine and model-check it. Ground truth is executed code, not the story you tell about it — a diagram lies, a reachability check over the actual transition function does not.

PolySec

A security lens over that same substrate — not a fork. You declare the forbidden region; it proves fully-mediated reachability, then attacks its own answer: havoc-testing for unmodeled channels, gate-deletion to hunt for a bypass. It also asks whether a breach is even detectable from what you can observe, before you rely on detecting it. If a path survives, you get the witness. If none does: FULLY MEDIATED.

polyman

Takes the proven policy and drops it between a live agent and its tools as an in-line, default-deny gate. Labels each tool by effect class, tracks per-session what's been touched, and denies any call that would complete the forbidden region — before the call runs.

No API key, no model call, deterministic — the test suite asserts $0 spend on the decision path.

How polysec hardens a policy

polysec pipeline — every path to the forbidden state passes a default-deny gate: forbidden region, mediate, havoc, bypass hunt, verdict

Four checks, run as one gate: polysec harden.

Harden from init

The policy machine is checked clean from its initial state — there's no reachable path into a forbidden region that the model didn't already rule out.

No havoc counterexample

polysec searches for an unmodeled channel that reaches the forbidden region regardless of the modeled policy, and fails loud if one exists — a counterexample names the exact unguarded variable — instead of certifying a policy with a hole nobody drew.

No gate-deletion bypass

The check also covers whether the gate itself can be routed around or disabled from inside the modeled machine — not just whether the policy is correct when the gate is honored.

Fully mediated, byte-for-byte

The same state-machine engine that produced the proof also steps the policy live, so the enforced machine and the proven machine are asserted identical, not just similar.

Fits with: polysec is the hardening engine behind polyman, and the one to reach for any time the artifact being verified is a security or access-control policy rather than a business process.

Reference monitor, formally closed

The idea of a reference monitor — a component that mediates every access, is tamper-proof, and is small enough to verify — goes back to Anderson, 1972. What's new isn't the concept. It's proving the policy fully mediated at design time, with a model checker, and then enforcing that exact proven machine at runtime — not a hand-written approximation of it.

The honest disclosure. This is a reference monitor, not a sandbox. It stops a misguided agent — legitimate tools steered by an injection. It does not, by itself, contain a compromised runtime that opens its own socket around the gate — that's confinement, a different and complementary job. And it proves the policy over your tool→effect labels; getting those right is a trust obligation it can't discharge for you.

The Hugging Face incident, reframed

It wasn't a model being evil — it was a model doing something reachable that nobody had proven unreachable, and that no self-report would have surfaced. You don't fix that by asking your agent to be honest. You fix it by making the lie unreachable.

#AIAgents #PromptInjection #FormalVerification #StateMachines #LLMSecurity

Adapted from “Your Agent Is Lying to You,” Jean-Jacques Dubray. Repo: github.com/cognitive-fab/polysec.