What a Policy Permits

Review a change by what it newly admits

The requests a policy admits form its admitted set. A candidate refines the old policy when its admitted set lies inside the old one, so the change can only remove requests. Run chio policy analyze new.yaml --against old.yaml and the report states one of three results:

The hostile comment in pull request #421 asks the reviewer to upload .env to paste.example.net. An egress allowlist that names api.github.com and *.openai.com refuses that host. Add paste.example.net to egress.allow, for a build-log upload, and the comparison reports does_not_refine. Its witness has the action_type egress and the target paste.example.net, and the finding’s rule_ref points to the new allow entry.

fn confirms(
    policy: &HushSpec,
    against: &HushSpec,
    witness: &Witness,
    budget: &mut AnalysisBudget,
) -> Result<bool, AnalysisError> {
    budget.consume_evaluator_confirmation()?;
    Ok(
        evaluate(policy, &action(witness)).decision != Decision::Deny
            && evaluate(against, &action(witness)).decision == Decision::Deny,
    )
}

The report names one witness, from the first widening its search reaches: tool access, argument size, egress, file paths, then computer-use and input actions. Removing **/.env.* alone yields file_read on /.env., the shortest path that only the removed pattern denied. Fix one widening and run the comparison again to find the next.

Find rules that never decide

Long policies collect entries that no longer change a decision. Run the analyzer on one policy, without --against, and it compares the entries within each block:

hushspec: "0.1.0"
rules:
  tool_access:
    allow: ["pricing.quote"]
    block: ["pricing.**"]
    default: block

Here pricing.** matches pricing.quote, and a block entry wins, so the analyzer reports allow entry 0 as a shadowed_rule. The exit code is 0 when no finding reaches the --fail-on threshold (default warning), 1 when one does, and 2 when loading, validation, or a bounded analysis limit fails. Each not_analyzed entry counts as a notice. The JSON report uses the schema chio.policy-analysis.v1.

What the analyzer decides

The analyzer resolves inheritance, lowers each rule block into sets of glob patterns, numeric bounds, finite values, and flags, and compares them. Globs use the evaluator’s own semantics for *, **, and ?. It lists every configured field outside that fragment in not_analyzed, with a reason.

The three-layer policy from Inherit and Merge Policies analyzes clean. Its two notices are the parts of the velocity rate window it cannot decide:

$ chio policy analyze ./policies/env/prod.yaml

policy_sha256  e9f82ee3bfb7830a2770fe9521b9de69ac06c54e1e953c5826715890a414428b

ID           SEVERITY  KIND                  BLOCK                 RULE
-            notice    not_analyzed          velocity              window
                      stateful rate-window predicate
-            notice    not_analyzed          velocity              burst_factor
                      stateful rate-window predicate

summary: 0 error(s), 0 warning(s), 2 notice(s)

The analyzer reads one HushSpec policy and judges one request at a time. WASM guards loaded beside the policy, session rules over sequences of calls, and information-flow labels lie outside it. A changed regex makes a comparison inconclusive even when the edit only adds a pattern: adding curl to a list that holds rm -rf refuses more commands, and the analyzer still cannot show it.

An allowlist names the requests a policy admits, so a program can compare two allowlists and produce a member of their difference. A pattern list names spellings to refuse. Whether those spellings cover every command with the same effect depends on what the commands do, and no comparison of two lists decides it. Beyond Blocklists sets out the boundaries that hold where a list cannot.

Tie each threat to a test that fails

Refinement shows that a change admits nothing new. Whether the old policy stops a given attack is a separate claim with separate evidence. A threat coverage record names the threat, the boundary that stops it, a counterexample, the mutations its test caught or missed, and the scope that remains outside the claim.

The tool_server_escape record is one example. A capability permits read_public on admitted-server. The attacker changes the tool to exec_privileged or the server to pivoted-server, and both registered connections accept every invocation, so only the kernel’s scope check can refuse. Mutation runs forced grant_matches_request in chio-kernel and grant_covers in chio-kernel-core to return Ok(true), and the test caught both. The record’s status is partial: it names WASM mutation evidence, authenticated process transport, and OS or container isolation as outside its scope.

Write new records the same way. Keep a valid neighboring request working, vary only the attacker’s input, observe the protected resource rather than the returned message, and break the defense on purpose to confirm the test fails. Adversarial testing covers the techniques, and behavioral gates shows which checks run in continuous integration and which block merging.

Proofs about delegated authority

A policy narrows what a grant permits, and the grant bounds what any policy can reach. Lean proves the properties that keep that bound, over bounded models of scopes and delegation steps:

Each theorem holds over its model and the assumptions the proof manifest lists. Formal Assurance traces which production functions connect to them. The policy analyzer is executable static analysis with its own bounds; the proof manifest defines the formal boundary.

Replay recorded traffic against a candidate

The analyzer covers every request in its fields. Replay covers the requests that reached the kernel, including those that shell regexes decide. Give chio replay traffic a capture with --from, the tenant key with --tenant-pubkey, and the candidate with --against. It authenticates the captured frames, evaluates each recorded invocation under the candidate in pre-output mode, and compares verdict, guard, and reason with the capture. A difference exits 10. No tool runs again.

A captured frame keeps neither the original tool-server ID nor the response bytes, so this mode rejects policies with concrete-server grants or post-invocation hooks. It also leaves the original identity, delegated authority, and runtime budget unreconstructed. Determinism and replay walks through a capture and a candidate comparison.

Choose the check by the question

Go further