Notes · Dissecting Real Systems

growing

Don't Write the Policy. Derive It.

A security policy is a claim about every case you did not think of. State the invariant instead, enumerate what the system can actually do, and let a model checker hand you the counterexample.

Yesudeep Jose Mangalapilly

Published 3 weeks ago · Updated 11 days ago · 15 min read

security, formal-methods, tla-plus, alloy, web, verification, dissecting-systems

Program testing can be used to show the presence of bugs, but never to show their absence!

— Edsger W. Dijkstra, Notes on Structured Programming (EWD249, 1970), stated there as a corollary

Cite this

APA

Mangalapilly, Y. J. (2026, July). Don't Write the Policy. Derive It.. Saṃhitā Notes. https://yesudeep.com/blog/dont-write-the-policy-derive-it/

BibTeX

@online{mangalapilly2026don,
  author  = {Yesudeep Jose Mangalapilly},
  title   = {Don't Write the Policy. Derive It.},
  journal = {Sa\d{m}hit\=a Notes},
  year    = {2026},
  month   = {July},
  url     = {https://yesudeep.com/blog/dont-write-the-policy-derive-it/},
  urldate = {2026-08-12},
}

Plain

Yesudeep Jose Mangalapilly. “Don't Write the Policy. Derive It..” Saṃhitā Notes, 2026. https://yesudeep.com/blog/dont-write-the-policy-derive-it/.

RIS

TY  - ELEC
AU  - Mangalapilly, Yesudeep Jose
TI  - Don't Write the Policy. Derive It.
T2  - Saṃhitā Notes
PY  - 2026
UR  - https://yesudeep.com/blog/dont-write-the-policy-derive-it/
Y2  - 2026-08-12
ER  -

A method, worked end to end on a real boundary. By the end you'll know why a hand-written policy is structurally unable to tell you what it missed, how to state a security property as an invariant, the one modeling decision that separates a model finding real attacks from one finding artifacts, when to reach for TLA+ versus Alloy, and how to keep a model honest once it exists — including the failure mode where the whole apparatus reports success and checks nothing.

Every security policy is written the same way. Someone thinks hard about what should be allowed, enumerates the cases they can imagine, writes a rule, and ships it. The rule is then correct about exactly those cases, and silent about the rest.

The silence is the problem, and it is not a failure of diligence. A policy is not a description of the cases its author considered; it is a claim about all of them. The author knows a handful; the claim covers the whole space. When a case nobody pictured arrives, it does not announce itself as a gap in someone's imagination — it arrives as an incident, and the post-mortem concludes that someone should have thought of it.

Two ways to arrive at a policy. Both produce a rule; only one produces the list of what the rule missed, and produces it before a user does.

A hand-written policy is a claim about every case its author did not consider. Nothing in the writing process can tell you what those were.

The alternative inverts the order of work. Rather than writing a rule and hoping it covers the space, you:

State the invariant — what must never happen, as a property of the system's state rather than of the policy's shape.
Enumerate the actions — everything the system genuinely permits, not everything you expect it to do.
Ask a checker for a counterexample — a reachable sequence of legal actions ending in a state the invariant forbids.

If it finds one, that is your missing clause, and it arrives as a concrete trace rather than a hunch. If it finds none, you have something no hand-written rule can offer: a claim about every case in the model, checked instead of assumed.

Imagine writing the rules for who may enter a building. The usual way is to picture the people you expect — staff, deliveries, visitors with appointments — and write a rule for each. The rule works beautifully for everyone you pictured.

The other way is to write down the one thing that must never happen ("nobody reaches the vault without an escort"), then list every door, lift, stairwell, and service hatch the building actually has, and hand both to someone whose only job is to find a path you missed. They will come back with "the loading bay lift reaches the vault floor and nobody escorts you there," which is not a rule you forgot to write. It is a rule you had no reason to know you needed.

The worked example

The method needs a real boundary or it stays a slogan. The worked example uses fetch metadata — the Sec-Fetch-Site, -Mode, -Dest, and -User request headers, which let a server see who initiated a request before deciding whether to answer it. If you want the boundary explained on its own terms, that's a separate piece; here it is the specimen, and you need only three facts about it.

First, the browser sets those four headers and page script cannot forge them, because Sec- prefixed names are forbidden request headers. Second, they describe the provenance of a request: who initiated it, in what mode, for what kind of element, and whether a human action caused it. Third, a server can therefore reject a request before authenticating anyone — which is the whole point, and also, as the model will show, a detail with teeth.

The question the model answers is the one any adopter has: which requests should I refuse, and what breaks if I refuse them? That is a policy question, and the usual answer is a hand-written rule.

Step one: state what must never happen

The temptation is to state the invariant as a property of the policy — "the policy rejects cross-site POSTs." Resist it. A property of the policy can only ever confirm that the policy says what you wrote, which you already know.

State it as a property of the outcome instead:

A cross-site actor never ends up holding a response to a
non-navigational request.

Now a policy that looks strict but leaks by some route you did not model still fails the check, because the property is about what the attacker ends up with rather than about the rule's shape. The outcome-based check distinguishes a test that can surprise you and one that cannot.

Important

An invariant that mentions your policy's mechanism is a tautology dressed as a check. Write it over the attacker's final state, never over the rule.

Step two: enumerate what the system can actually do

Here is the decision that determines whether the model is worth building, and it is the one most likely to be got wrong.

An attacker does not choose Sec-Fetch-Site: cross-site. They cannot: the header is unforgeable. What they choose is an action — embed an image, auto-submit a form, frame a page, open a window — and the browser derives the header tuple from that action.

So the model has two relations, and only one of them is under test:

Derive : Action      → HeaderTuple    the browser; trusted, per spec
Admit  : HeaderTuple → serve | 403    the policy; the thing being checked

The modeling decision the method rests on. Because the browser's derivation is modeled explicitly, the checker cannot invent a header combination no browser would emit — so every counterexample is an attack that can actually be run.

Model only the second relation and the checker will cheerfully explore header tuples no browser will ever send, and report attacks that cannot happen. Model both and every counterexample is reachable in a real browser, because the only way into the state space is through an action a page can genuinely take.

Model what the attacker chooses, not what the server sees. The gap between those two is where false counterexamples come from.

Prediction checkpoint. Commit before reading on.

Step three: ask for the counterexample

With the invariant and the action alphabet in hand, the checker does the part that a human cannot do reliably: it tries everything.

For a hand-written policy — same-site traffic allowed, top-level GET document navigations allowed, everything else refused — the checker confirms the invariant holds. That is a real result and it took seconds.

The interesting output is what happens when you relax the policy by one clause. Allow cross-site framing, on the entirely reasonable grounds that your page is meant to be embeddable, and the checker returns a trace: a cross-site <iframe> is a safe-method top-level navigation, which is exactly the case SameSite=Lax still sends cookies for — so any site can frame your page and load it as the logged-in user.

That is not an exotic finding. It is the clickjacking and cross-site-leak shape, and it is what "embeddable" costs when the cookie policy is Lax rather than Strict. What matters for the method is how it arrived: nobody had to think of it. It fell out of asking for a counterexample.

Note

Two things that look like implementation detail turn out to be safety properties, and both are invisible to a model that only looks at headers: a shared cache that does not Vary on the fetch-metadata headers replays a first-party response to a cross-site requester — the policy still exists, the attacker simply never reaches it — and a policy evaluated after authentication emits an observable that varies with the victim's session, handing back the signal the rejection was supposed to withhold. Both need the model to include a cache and an ordering. Which is the argument for modeling more than the obvious surface.

The profiles fall out

Because the policy is a variable in the model rather than fixed text, you can ask which policies satisfy the invariant instead of asserting that yours does. The rungs stop being a matter of taste:

Strict — same-site traffic plus genuine top-level GET document navigations. Holds under the strong invariant. A site with no cross-origin API can deploy it as-is.
Standard — strict, plus cross-site CORS calls. Cannot satisfy the strong invariant, and this is not a defect: a public API is a cross-site read. It satisfies the honest weaker claim instead — an attacker may call the API, but never as the victim.
Embeddable — standard, plus framing and hotlinking. Sound only with SameSite=Strict; under Lax it admits the credentialed read described in the worked example.

Each profile admits a superset of the stricter profile, so moving up a rung never invalidates an exemption already reviewed. That ladder property is worth stating explicitly because it is what makes the profiles adoptable: a site can start at the top and descend as it discovers real cross-site traffic, and never re-audit.

Make the policy a variable and the checker stops grading your answer and starts producing it.

Choosing the tool

Two checkers, two questions, and the split is not redundancy.

TLA+ models a system evolving over time, so it is the right tool the moment your property involves sequences — a cache populated by one request and read by another, an ordering between authentication and rejection, anything where "what happened before" matters. The cache-ordering and authentication-ordering hazards both need it.

Alloy models relations and finds instances, so it is the right tool for "over all combinations, does anything satisfy this?" It answers the which-tuples-does-this-policy-admit question faster and shows counterexamples better.

Running both is worth it when the same claim can be stated in each, because agreement between two independently-written models is real evidence, and disagreement is a bug in one of them — which is itself a useful signal, and one you cannot get from a single spec.

Warning

A model is only as honest as its action alphabet. An attack that uses a mechanism you did not encode is invisible, and the model will report success with total confidence. "No counterexample found" means no counterexample in the modeled world — never "no attack exists." Every model needs its limits written down next to its results, or the results will be read as stronger than they are.

Keeping it honest

A model that nobody runs is a comment, and a model that runs but cannot fail is worse than no model at all, because it manufactures confidence. Two practices matter more than the modeling itself.

Make the checker a build gate. Pin the model checker by digest and run it in CI alongside the tests. A spec that stops holding should break the build exactly like a failing unit test.

Make the attack demonstrations fail loudly if they stop demonstrating. The configurations that encode attack paths should assert that a violation is found. Otherwise a change that quietly makes one hold looks like a pass, and you have lost a demonstration without noticing.

There is a specific failure mode worth naming, because it is the one that turns the whole apparatus into theatre. Model checkers report violations in their output and use coarse exit codes; a naive wrapper that treats "the tool ran" as "the check passed" will report success for a spec with a parse error. The wrapper must treat no recognizable verdict — parse error, bad config, crash — as a failure. Then verify that it does, by deliberately breaking the spec and confirming the gate goes red.

A green gate that checks nothing is worse than no gate, because it is evidence of the wrong thing.

What this is not

Formal methods have a reputation for demanding more than a project can pay, and the honest version of this argument has to name what it does not claim.

A passing model is not proof that your system is secure. The model is a small abstraction, and its results hold over that abstraction. The implementation may not match it.

It is not a substitute for the reasoning. Choosing the invariant and the action alphabet is the real work, and it is unautomated. The checker only searches the space you describe.

It is not expensive here, and that is the actual argument. The model in this piece is a few hundred lines and runs in seconds. The claim is not that you should verify everything — it is that when you are about to hand-write a policy that other people will deploy, a few hundred lines that can tell you what you missed is a good trade against finding out from an incident.

The same move, at industrial scale

The worked model is small, and it is worth seeing that the underlying move is not. Google published an account of preventing DOM-based XSS across its JavaScript codebase, and the shape of what they did is the shape of this article — with a compiler where this piece uses a model checker.

The paper's title states the thesis better than a summary could: If It's Not Secure, It Should Not Compile. Rather than writing rules about which uses of innerHTML are acceptable, they made the dangerous sinks unusable and provided typed replacements, then let the type checker discharge the argument:

a collection of specially designed types and APIs that reduce the task of demonstrating the absence of XSS vulnerabilities to a type checking problem.

Note what that sentence does. The property is not asserted by a reviewer and it is not enumerated case by case; it is reduced to something a machine decides. That is the same trade this piece argues for — replace a human claim about all cases with a mechanical verdict over a stated space — and the difference is only which machine and which space.

The measured result is one product, over three years:

period	DOM-based XSS reports
year before adoption	10
year during adoption	2
year after adoption	1

Note

Read that table narrowly. It is one product with a few tens of frontend engineers who spent roughly a year refactoring, and the metric is externally-reported bug bounty submissions rather than ground truth. The paper is careful about this: its company-wide figures are proportions, and the authors concede those "may be contributed to by other security measures deployed during the sampled period." A 10 → 1 trend on one team is evidence, not a guarantee.

Two honest limits from the paper transfer directly to model checking, and both were named earlier in this piece in different words. Their analysis is unsound — TypeScript's type system permits casts, and the paper prints the two-line bypass — so the mechanism stops accidents rather than adversaries. And they cannot enumerate every sink, because "it is unrealistic to cover all browser-specific XSS sinks because many browsers have undocumented behaviors." That is the action-alphabet ceiling again: a checker is bounded by the world you described to it.

Whether the machine is a type checker or a model checker, the move is the same: stop asserting the property and start deriving it over a space you wrote down.

Lessons

A hand-written policy is a claim about every case its author did not consider, and nothing in the writing process surfaces those cases.
State the invariant over the attacker's final state, never over the policy's mechanism. An invariant that names your rule is a tautology.
Model what the attacker chooses, not what the server sees. Encoding the browser's derivation from action to header tuple is what makes every counterexample reachable in reality.
Make the policy a variable and the checker derives profiles instead of grading yours.
TLA+ for sequences, Alloy for combinations. Cache replay and evaluation ordering are temporal properties; which-tuples-are-admitted is relational. Two agreeing models are evidence; disagreement is a bug worth finding.
"No counterexample" means none in the modeled world. The action alphabet is the ceiling, and the limits belong next to the results.
Gate the model in CI, and verify the gate can fail. A wrapper that reads "the tool ran" as "the check passed" will pass a spec with a parse error.
The move generalizes past model checkers. Google reduced "this code has no DOM XSS" to a type-checking problem and measured 10 → 1 reports on one product. Same trade, different machine — and the same two limits: an unsound analysis, and a sink list nobody can complete.

Practice

Retrieval. Recover the rule that keeps counterexamples real.

Discrimination. Match the property to the checker that suits it.

Transfer. Diagnose a verification setup that reports success and checks nothing.

References

Leslie Lamport. “The TLA+ Home Page.” — the specification language and the TLC model checker
Daniel Jackson. “Alloy: A Language and Tool for Exploring Software Designs.” MIT. — the relational modeling language and analyzer
Edsger W. Dijkstra. “Notes on Structured Programming.” EWD249, 1970. — the epigraph, and the argument for reasoning over testing
Newcombe et al.. “How Amazon Web Services Uses Formal Methods.” Communications of the ACM, 2015. — formal methods on production systems, and what they found
Wang, Bangert, Kern. “If It's Not Secure, It Should Not Compile: Preventing DOM-Based XSS in Large-Scale Web Development with API Hardening.” ICSE, 2021. — the same move discharged by a type checker rather than a model checker, its measured result, and its two honest limits
W3C. “Fetch Metadata Request Headers.” W3C Working Draft, 2025. — the boundary used as the worked example
WHATWG. “Fetch Standard.” WHATWG. — forbidden request headers: why the browser's derivation is trusted
Google. “Protect your resources from web attacks with Fetch Metadata.” web.dev. — the hand-written policy the model checks against

How to cite

APA

Mangalapilly, Y. J. (2026, July). Don't Write the Policy. Derive It.. Saṃhitā Notes. https://yesudeep.com/blog/dont-write-the-policy-derive-it/