Proving Policy Properties with Cedar's Symbolic Compiler

A test checks the requests you thought of. A proof checks every request the schema allows. I ran both against the agent authorization policies from the first series, and the proofs asked two questions the tests had never raised. Part 2 called Cedar’s symbolic compiler “the next step once tests stop being enough”. This is that step: the series’ eight policies, checked with the cvc5 solver in the build, the verdicts printed as the solver wrote them, and the two changes the proofs caused in the series marked where they happened.

Key terms (3)

property: A statement about a whole policy set, such as “no request of this shape is ever allowed”.
request environment: One combination of principal type, action and resource type. The compiler proves a property for one environment at a time.
counterexample: A concrete request, with its entities, for which the property is false. The solver constructs it; nobody writes it.

What you need

Two binaries and Part 2’s files. The cedar CLI from release 4.14.1, from the experimental archive (cedar-policy-cli-experimental-<target>.tar.xz; the default archive refuses the symcc subcommand). cvc5 1.4.2, the static non-GPL build, named by --cvc5-path or the CVC5 variable; the CLI gives it sixty seconds per query. The schema, policies and entities from Part 2’s downloads, and the property and refactor files at the end of this post.

These checks were written on Cedar 4.13.0 and cvc5 1.3.1. No release since changes them, and every verdict is the same on the pinned releases. Cedar’s own tests still run cvc5 1.3.1; on 1.4.2 one counterexample names other groups, the solver’s choice of model.

One check names one request environment with three flags, principal type, action and resource type, so a property about every action runs three times. The exit code is zero either way; the verdict is the first line of output, and the build fails when it is not the one the manifest declares. A property that stops holding and a counterexample that disappears are both findings, and both stop the deploy. The build runs make policy-prove from prove.json next to the post whenever a policy, the schema, a property or a binary changes.

What a test cannot say

Part 2 left the policy set with test cases, a canary that must fail, and mutation testing: delete each policy and guard in turn, and every broken copy must fail a test. That proves the tests notice when a guard disappears. It does not prove the set is narrow. The cases are points. The schema describes a space, every principal, action, resource, context and entity store that type-checks, and a proof asks about the space.

A box labelled every well-formed request holds three test cases, Alice reads, the injected write and the approved destroy, and one request nobody wrote. The tests point at the three cases one by one. The solver points at the whole box. — Figure 1. Tests check the points someone wrote. The solver checks the box, including the request nobody wrote.

What the symbolic compiler does

Cedar’s symbolic compiler takes a policy set, the schema and one request environment, and compiles the policies into SMT-LIB constraints for a solver like cvc5. Then it asks a question shaped like “does a request exist that both sets allow?”. If the solver proves none exists, the property is verified. If it finds one, the compiler turns the solver’s model back into a request and an entity store: the counterexample.

The policies file, the schema and one request environment, Agent, write, Tool, go into the symbolic compiler, which emits SMT-LIB constraints to cvc5. cvc5 answers unsat, which is a verified property because no such request exists, or sat with a model, which comes back as a counterexample request. — Figure 2. One check: compile, solve, read the model back. A proof is per request environment.

The build asks five kinds of question: disjoint, implies and equivalent, each over two policy sets; always-denies of one set; and never-errors of a single policy.

Going deeper: what the Lean proofs cover, and what they do not

The compilation and the checks are proved sound and complete in Lean, in the cedar-spec repository: a verified property holds for every well-formed input, a failed one has a real counterexample. The CLI runs a Rust port that is fuzzed against that model, and trusts the solver.

The invariant, proved: no cross-tenant allow

Tenant isolation is the invariant the series rests on. To prove it I wrote the bad thing as a policy set of its own: a permit for exactly the requests whose tool belongs to a tenant other than the one bound at authentication.

properties/cross-tenant.cedar

// The bad thing, as a policy set: it allows exactly the requests whose tool belongs
// to another tenant than the one bound at authentication. If the real set and this
// one never allow the same request, no cross-tenant call is ever permitted.
@id("cross-tenant")
permit (principal, action, resource)
when { resource.tenant != context.tenant };

Then I asked whether the real set and this one are disjoint: is there any request both allow?

output, write

✓ Policy sets are disjoint: VERIFIED

Read and destroy say the same; the summary at the end lists all three. Part 2 could say that its cross-tenant cases are denied. This says that no request in the space is allowed, for any user, agent, set of grants or depth.

The twist, proved: delete the policy and the solver writes the attack

Part 2’s twist deleted tenant-isolation and replayed the injected write from a request file someone had written. Run the disjointness check on the set without that policy and the solver writes the request itself:

output, write, with tenant-isolation removed

✗ Policy sets are disjoint: DOES NOT HOLD
  Counterexample found:
principal: Agent::"", action: Action::"write", resource: Tool::""
context: {
  delegated_read_groups: [ToolGroup::"", ToolGroup::"B"],
  delegated_write_groups: [ToolGroup::""],
  depth: -1,
  now: datetime("1970-01-01").offset(duration("-1ms")),
  request_hash: "",
  tenant: Tenant::"",
  user: User::"",
}
entities: [
  Action::"destroy",
  Action::"read",
  Action::"write",
  Agent::"" {
    read_groups: [ToolGroup::"", ToolGroup::"A"],
    write_groups: [ToolGroup::"B"],
  },
  Tenant::"" {
    read_groups: [ToolGroup::"", ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"A"],
  },
  Tenant::"A" {
    read_groups: [ToolGroup::"", ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"A"],
  },
  Tool::"" in [ToolGroup::"", ToolGroup::"A", ToolGroup::"B", ToolGroup::"C"] {
    tenant: Tenant::"A",
  },
  ToolGroup::"",
  ToolGroup::"A",
  ToolGroup::"B",
  ToolGroup::"C",
  User::"" {
    read_groups: [ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"C"],
  },
]

The context binds Tenant::""; the tool belongs to Tenant::"A"; every grant the permits ask for is in place, in a store the solver built. (The build sorts it and prints the context one field per line.) Strip the solver’s names away and it is the call Alice’s assistant sent in Part 2, found by search, not by someone remembering to write it.

The odd values are the point. A gateway would not build depth: -1 or a clock before 1970, but the schema types them, so the proof covers them. A property proved over that space holds for the narrower one a gateway would send; a counterexample needs a second look to see whether a real caller can reach it.

Figure 3. The twist as a search. The build declares that this check must fail, so a counterexample that vanished would stop the deploy too.

Never more than the user

Every permit in the series is an intersection: the user, the agent and the tenant must each hold the grant. Half of that is a property. Write what the user alone may do, and ask whether the real set implies it: every request the real set allows, this set allows too.

properties/user-bound.cedar

@id("user-may-read")
permit (principal, action == Action::"read", resource)
when { resource in context.user.read_groups };

@id("user-may-write")
permit (principal, action in [Action::"write", Action::"destroy"], resource)
when { resource in context.user.write_groups };

output, destroy

✓ Policy set 1 implies policy set 2: VERIFIED

An agent, a tenant grant or a delegation chain can narrow what Alice may do. None of them can widen it. That was a principle in Part 1; now it is a theorem about this set.

A refactor, proved equivalent

request-scope is the one policy that branches on the action: a hand-off may not widen the read scope, and anything that is not a read may not widen the write scope. Some reviewers prefer two plain forbids, one per scope. Whether they are the same policy is a question for the solver: the real set against the real set with the pair swapped in, in all three environments.

refactors/request-scope-split.cedar

// request-scope without the if/then/else: one forbid per scope. Proved
// equivalent to the original under the series 1 schema.
@id("request-scope-read")
forbid (principal, action == Action::"read", resource)
unless { resource in context.delegated_read_groups };

@id("request-scope-write")
forbid (principal, action in [Action::"write", Action::"destroy"], resource)
unless { resource in context.delegated_write_groups };

output, write

✓ Policy sets are equivalent: VERIFIED

The proof is per schema. The if version sends anything that is not a read to the write scope; the split version lists the actions. Add a fourth action and the first starts out strict, the second unconstrained. Run the check again before believing it.

Never errors, and what that does not promise

A Cedar policy that errors at evaluation is skipped and the decision is made without it. The compiler proves a policy never errors for any well-formed input, and the build asks that of each of the eight policies. This is tenant-isolation:

output, write

✓ Policy never errors: VERIFIED

Part 2 printed the other side for the same policy: a tool the loader never registered, and the policy skipped with an error. Both are true. The proof quantifies over well-formed inputs, and a request naming an entity the store does not hold is not one; that stays the job of the suite’s num_errors: 0. Reading that boundary is part of using a proof.

Inside the space, the proof sees what validation cannot. This policy reads like delegation-depth, validates without a warning, and is a different policy:

refactors/delegation-depth-plus-one.cedar

// Reads as delegation-depth (depth > 2), validates, and is not the same policy.
@id("delegation-depth-plus-one")
forbid (principal, action, resource)
when { context.depth + 1 > 3 };

output, read

✗ Policy never errors: DOES NOT HOLD
  Counterexample found:
principal: Agent::"", action: Action::"read", resource: Tool::""
context: {
  delegated_read_groups: [],
  delegated_write_groups: [ToolGroup::""],
  depth: 9223372036854775807,
  now: datetime("1970-01-01").offset(duration("-1ms")),
  request_hash: "",
  tenant: Tenant::"",
  user: User::"",
}
entities: [
  Action::"destroy",
  Action::"read",
  Action::"write",
  Agent::"" {
    read_groups: [],
    write_groups: [],
  },
  Tenant::"" {
    read_groups: [],
    write_groups: [],
  },
  Tool::"" {
    tenant: Tenant::"",
  },
  ToolGroup::"",
  User::"" {
    read_groups: [],
    write_groups: [],
  },
]

The context carries the largest 64-bit integer, depth + 1 overflows, and the forbid errors. The engine alone would skip it and decide without the depth limit: a bypass. A gateway built on the series’ rule, refuse any answer that carries an evaluation error, would deny every request at that depth: an outage. No test case had that number in it, and the validator checks types; depth + 1 is well-typed.

The question the tests never asked

The series’ two-person rule, as first published, said a destroy needs an approver from the same tenant who is not the requester. A stricter reading: the approver holds the write grant for that tool, so could have done the destroy alone.

properties/approver-can-write.cedar

// A destroy is approved by someone who could have done it alone: the approver holds
// the write grant for that tool. The real set should never allow a destroy this
// set denies.
@id("approver-can-write")
permit (principal, action == Action::"destroy", resource)
when {
  context has approved_by &&
  resource in context.approved_by.write_groups
};

Did the set as first published imply it? The build keeps that forbid as a file and composes it into the set in place of the published one:

refactors/destructive-needs-approval-without-grant.cedar, the forbid as first published

@id("destructive-needs-approval-without-grant")
forbid (principal, action == Action::"destroy", resource)
unless {
  context has approved_by &&
  context.approved_by != context.user &&
  context.approved_by in context.tenant
};

output, destroy, with the forbid as first published

✗ Policy set 1 implies policy set 2: DOES NOT HOLD
  Counterexample found:
principal: Agent::"", action: Action::"destroy", resource: Tool::""
context: {
  approval_expires: datetime("1970-01-01").offset(duration("9223372036854775807ms")),
  approval_for: "",
  approved_by: User::"A",
  delegated_read_groups: [ToolGroup::"", ToolGroup::"B"],
  delegated_write_groups: [ToolGroup::""],
  depth: -1,
  now: datetime("1970-01-01").offset(duration("-1ms")),
  request_hash: "",
  tenant: Tenant::"",
  user: User::"",
}
entities: [
  Action::"destroy",
  Action::"read",
  Action::"write",
  Agent::"" {
    read_groups: [ToolGroup::"", ToolGroup::"A"],
    write_groups: [ToolGroup::"B", ToolGroup::"E"],
  },
  Tenant::"" {
    read_groups: [ToolGroup::"", ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"A", ToolGroup::"D"],
  },
  Tool::"" in [ToolGroup::"", ToolGroup::"A", ToolGroup::"B", ToolGroup::"C"] {
    tenant: Tenant::"",
  },
  ToolGroup::"",
  ToolGroup::"A",
  ToolGroup::"B",
  ToolGroup::"C",
  ToolGroup::"D",
  ToolGroup::"E",
  ToolGroup::"F",
  User::"" in [Tenant::""] {
    read_groups: [ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"C", ToolGroup::"F"],
  },
  User::"A" in [Tenant::""] {
    read_groups: [ToolGroup::"", ToolGroup::"C"],
    write_groups: [],
  },
]

It did not. User::"A" is in the tenant, is not the requester, and holds an empty write_groups; the set accepted the approval. The suite even had the case: its one approver was Bob, who holds no write grant, and it asserted an allow, because nobody had asked.

Whether that is a hole depends on what “approver” means. Anyone with authority in the tenant: the set was right. Someone who could have done the thing alone: one more guard, the approver holds the write grant for the tool. The series carries that guard now (Part 2 prints it), and the proof holds on the published set:

output, destroy, the published set

✓ Policy set 1 implies policy set 2: VERIFIED

The fixtures changed with the rule: Dana, who holds the write grant, approves the allow case; Bob approving is a named deny. The counterexample stays on file as a verdict that must keep failing.

The guard has a cost no proof here shows. A destroy now needs two people in the tenant with a write grant for the tool, so a tenant with one cannot destroy at all. A reader on Hashnode pointed that out; Part 2 says so now.

Does the set allow anything

Every proof so far holds for a policy set that allows nothing: disjoint and implies bound what a set permits, and a set of forbids passes both. So ask the solver whether the set always denies a destroy, and declare that the answer must be no.

output, destroy: does the set always deny?

✗ Policy set always denies: DOES NOT HOLD
  Counterexample found:
principal: Agent::"", action: Action::"destroy", resource: Tool::""
context: {
  approval_expires: datetime("1970-01-01").offset(duration("9223372036854775807ms")),
  approval_for: "",
  approved_by: User::"A",
  delegated_read_groups: [ToolGroup::"", ToolGroup::"B"],
  delegated_write_groups: [ToolGroup::""],
  depth: -1,
  now: datetime("1970-01-01").offset(duration("-1ms")),
  request_hash: "",
  tenant: Tenant::"",
  user: User::"",
}
entities: [
  Action::"destroy",
  Action::"read",
  Action::"write",
  Agent::"" {
    read_groups: [ToolGroup::"", ToolGroup::"A"],
    write_groups: [ToolGroup::"B"],
  },
  Tenant::"" {
    read_groups: [ToolGroup::"", ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"A"],
  },
  Tool::"" in [ToolGroup::"", ToolGroup::"A", ToolGroup::"B", ToolGroup::"C", ToolGroup::"D"] {
    tenant: Tenant::"",
  },
  ToolGroup::"",
  ToolGroup::"A",
  ToolGroup::"B",
  ToolGroup::"C",
  ToolGroup::"D",
  User::"" in [Tenant::""] {
    read_groups: [ToolGroup::"A", ToolGroup::"B"],
    write_groups: [ToolGroup::"C"],
  },
  User::"A" in [Tenant::""] {
    read_groups: [ToolGroup::"", ToolGroup::"C"],
    write_groups: [ToolGroup::"D"],
  },
]

That is an approved destroy. User::"" asks and User::"A" approves; both are in the tenant, and each holds a write group that contains the tool. Not the same group: the requester holds ToolGroup::"C", the approver ToolGroup::"D", and the tool sits in both.

Nobody had written that case either. Part 3’s check on the grant data counted the users holding each write group, reasoning that a destroy needs two holders of the same grant. The policy says resource in context.approved_by.write_groups, which any group of the tool satisfies. With a tool in two groups and one holder in each, the count read one and one while this destroy was reachable. The count is per tool now, and Part 3 prints the store the old count passed.

What it costs

expected/prove.summary.txt

no-cross-tenant-allow  disjoint  read  VERIFIED
no-cross-tenant-allow  disjoint  write  VERIFIED
no-cross-tenant-allow  disjoint  destroy  VERIFIED
no-cross-tenant-allow.without-tenant-isolation  disjoint  write  DOES NOT HOLD
never-more-than-the-user  implies  read  VERIFIED
never-more-than-the-user  implies  write  VERIFIED
never-more-than-the-user  implies  destroy  VERIFIED
request-scope-split  equivalent  read  VERIFIED
request-scope-split  equivalent  write  VERIFIED
request-scope-split  equivalent  destroy  VERIFIED
tenant-isolation-never-errors  never-errors  read  VERIFIED
tenant-isolation-never-errors  never-errors  write  VERIFIED
tenant-isolation-never-errors  never-errors  destroy  VERIFIED
read-tools-never-errors  never-errors  read  VERIFIED
read-tools-never-errors  never-errors  write  VERIFIED
read-tools-never-errors  never-errors  destroy  VERIFIED
write-tools-never-errors  never-errors  read  VERIFIED
write-tools-never-errors  never-errors  write  VERIFIED
write-tools-never-errors  never-errors  destroy  VERIFIED
destructive-needs-approval-never-errors  never-errors  read  VERIFIED
destructive-needs-approval-never-errors  never-errors  write  VERIFIED
destructive-needs-approval-never-errors  never-errors  destroy  VERIFIED
approval-matches-call-never-errors  never-errors  read  VERIFIED
approval-matches-call-never-errors  never-errors  write  VERIFIED
approval-matches-call-never-errors  never-errors  destroy  VERIFIED
approval-is-fresh-never-errors  never-errors  read  VERIFIED
approval-is-fresh-never-errors  never-errors  write  VERIFIED
approval-is-fresh-never-errors  never-errors  destroy  VERIFIED
request-scope-never-errors  never-errors  read  VERIFIED
request-scope-never-errors  never-errors  write  VERIFIED
request-scope-never-errors  never-errors  destroy  VERIFIED
delegation-depth-never-errors  never-errors  read  VERIFIED
delegation-depth-never-errors  never-errors  write  VERIFIED
delegation-depth-never-errors  never-errors  destroy  VERIFIED
depth-plus-one-never-errors  never-errors  read  DOES NOT HOLD
approver-can-write  implies  destroy  VERIFIED
approver-can-write.without-guard  implies  destroy  DOES NOT HOLD
destroy-is-reachable  always-denies  destroy  DOES NOT HOLD
results: 38 runs, 34 hold, 4 do not hold, every verdict as declared

One line per solver run, seconds for the whole file on this schema. Part 2’s mutation step does not run the proofs: the one mutant they care about, tenant-isolation removed, is already a declared property with its counterexample on file.

Try it yourself

Try it

With the two binaries and Part 2’s files in place (see What you need), download the files below next to the schema and policies and run:

terminal

cedar symcc --schema schema.cedarschema \
  --principal-type Agent --action 'Action::"destroy"' --resource-type Tool \
  implies --policies1 policies.cedar --policies2 approver-can-write.cedar

That prints VERIFIED. Then swap the published forbid for the one in destructive-needs-approval-without-grant.cedar in your copy and run it again: the solver prints a counterexample of the same shape, in the CLI’s own order.

These property files are the ones the build proves, not copies.

Checklist

Questions to ask of your own policy set. Each links to the section that shows the check, and the series’ own checklist is in Part 3.

Is the core invariant a policy set of its own, proved disjoint from the real set? (the invariant, proved)
Does every property run in every request environment it speaks about? (what you need)
When a forbid is removed, does the build expect the counterexample, so a check that silently passes fails the build? (the twist, proved)
Is there a bound set, what one party alone may do, that the real set is proved to imply? (never more than the user)
Is every refactor proved equivalent before it merges, and again when the schema gains an action? (a refactor, proved equivalent)
Does never-errors hold for every policy, and do you know which errors sit outside the proof and what your gateway does with one? (never errors)
Is the stricter reading of each rule written as a property and checked? (the question the tests never asked)
Does a witness show the set allows what it should, so no proof passes on a set that denies everything? (does the set allow anything)
Does the review print the solver’s output rather than restate it? (what it costs)

What you need#

What a test cannot say#

What the symbolic compiler does#

The invariant, proved: no cross-tenant allow#

The twist, proved: delete the policy and the solver writes the attack#

Never more than the user#

A refactor, proved equivalent#

Never errors, and what that does not promise#

The question the tests never asked#

Does the set allow anything#

What it costs#

Try it yourself#

Checklist#

Subscribe

What you need

What a test cannot say

What the symbolic compiler does

The invariant, proved: no cross-tenant allow

The twist, proved: delete the policy and the solver writes the attack

Never more than the user

A refactor, proved equivalent

Never errors, and what that does not promise

The question the tests never asked

Does the set allow anything

What it costs

Try it yourself

Checklist