geohashim

authz-proof

A permission engine for SpiceDB-style schemas, Google Zanzibar's model, built to answer the question a schema review can't answer by reading: if this change merges, who gains access and who loses it?

Authorization schemas are short, and they read as if they were obviously right. authz-proof evaluates every relation and permission of every object for every subject, once before a change and once after, and lists each difference with the chain of relationships that causes it. In CI it fails the pull request when access changes in a way an allowlist doesn't expect.

View on GitHub What it found in SpiceDB

Plays the seven stages below in order, about 65 seconds. Scroll or press Esc to stop.

Language
Go 1.22 or newer, standard library only
Tests
27 passing, 2 of them against a live SpiceDB
Schema
SpiceDB's language: + & - ->, wildcards, subject sets
Commands
diff, check, lookup-resources, lookup-subjects, expand, validate
Checked against
A naive second evaluator, seven planted bugs, and SpiceDB v1.56.2
License
MIT
authz-proof diff schema.zed schema-refactor.zed relationships.txt --fail-on-gain compared 966 checks per side: every relation and permission of 23 objects, for 14 subjects 6 grants gained, 0 lost GAINED document:budget#view user:bob, user:carol GAINED document:offer-letters#view user:bob, user:carol GAINED document:payroll#view user:bob, user:carol

Real runs of authz-proof at commit 1e6e95e, output verbatim, in examples/drive: a shared drive with five definitions, 30 relationships and four versions of the schema. The refactor moves one exclusion and is described as changing nothing.

1Parse the schema the way SpiceDB does

SpiceDB binds + before & before -, all left-associative, so a - b + c means a - (b + c). authz-proof parses with the same precedence, and validate warns whenever a permission depends on it.

  • SpiceDB's schema errors are refused too: permissions or wildcards on the left of an arrow, permissions that alias each other in a loop, wildcards reached through a subject set on another definition.
  • A permission that subtracts something depending on itself, such as view = viewer - view, has no single meaning. SpiceDB accepts it; authz-proof refuses it.
  • Caveats, nil and the .any() and .all() arrows aren't supported, and say so.
  • Every relationship is checked against the schema: the relation must exist and allow that subject type.

One pair of parentheses dropped

schema.zed, document#view

schema-no-parens.zed reads like

and means

What it refuses Illustrative input

The two schemas are the repository's. The seven refused files were written for this page, one mistake each; the errors and exit codes are real.

2Check, and show the chain

A check is a depth-first search over the relationships. Every yes comes with the shortest chain that grants it, and every no with the exclusion that removed it, if one did.

  • Recursion is read as the least fixed point: teams that contain each other have exactly the members someone actually added. A goal already on the current path counts as false, which is exact because a shortest derivation never passes through itself.
  • A "no" that leaned on such a cut is only remembered once the goal it leaned on has finished.
  • Every user in no relationship has the same access, so one stand-in per type answers for all of them. That makes "everyone" a finite question: user:* grants show up for the stand-in.

Three questions about the shared drive

    The chains are drawn from check's own output, shown verbatim below them. user:zoe appears in no relationship: the answer comes from document:status-page#viewer@user:*.

    3Diff every check, both sides

    diff runs every check twice, under the old schema and relationships and under the new: every object, times every relation and permission of its type, times every subject, stand-ins included. Each change gets the shortest chain on the side that grants it, and the exclusion that removed it on the other side.

    • A schema change and a data change are both access changes: two schemas, or one schema with --new-relationships.
    • The example has 23 objects with 69 relations and permissions among them, and 14 subjects: 966 checks per side.
    • --json prints every change with its chain, for a bot to post on the pull request.

    The refactor's description: "Only explicit viewers need the contractor check; folder access is already scoped to staff." It isn't. The company folder is shared with the whole organization, and contractors are members of it.

    966 checks before, 966 after

    Yes on both sidesGainedLostNo
    Columns are the 69 relations and permissions, grouped by object; rows are the 14 subjects, with "any other" for the stand-ins. Every cell is the engine's real answer, computed with authz-proof's own engine package in the order diff uses; the yes counts, 121 before and 127, 121 or 91 after, match what SpiceDB answered for the same schemas.

    4Check the engine against a naive twin

    A tool that says "no access changes" is only useful if it would have noticed one. ref is a deliberately naive second evaluator: it computes every fact for every subject by repeating rounds until nothing changes, and shares no evaluation code with the engine.

    • The property tests generate random schemas and relationships: cycles, wildcards, nested subject sets, arrows, intersections, exclusions, and operators mixed without parentheses.
    • The engine must agree with the reference on every check, lookup, expansion and diff.
    • It also carries seven known mistakes behind a switch, and the same tests must catch every one. A clean run means nothing unless a broken engine fails.

    Seven planted bugs, 500 seeds each

      Both runs are real and verbatim. The bars are the share of the 500 seeds on which each broken engine failed a property. hunt took 23.6 s in the README's run; here it took 83.3 s on a machine busy with other work, with the same models and the same result.

      5Ask a real SpiceDB the same questions

      crosscheck writes the same schema and relationships to SpiceDB v1.56.2 through its HTTP API and asks it every question the engine answers. CI does this on every push, for the four example schemas and 600 random models.

      • Every schema authz-proof refuses is written too, to see if SpiceDB refuses it. It never refused one authz-proof accepted.
      • The random models never lead from an object back to itself, because on cyclic data SpiceDB answers max depth exceeded where authz-proof answers no.
      • SpiceDB runs with its dispatch cache off. With the cache on, its answers depend on the order of the questions.

      Agreement, and the order-dependent answer

      Alice views documents one and two, and edits neither. view_and_edit = viewer & editor

      Run here against authzed/spicedb:v1.56.2 in Docker, in-memory datastore. The counts are crosscheck's output, identical to the README's. The answers are examples/spicedb-cache/repro.sh on two fresh servers, one with default settings and one with --dispatch-cache-enabled=false.

      Expected by nameAbove this line authz-proof works out every change in access and checks its own engine. Below it, a person lists the changes a pull request is meant to make, and anything else fails it.

      6A person names the expected change

      The allowlist says which changes a pull request is meant to make, one pattern and reason per line. Each part of a pattern can use globs and one {a,b} group. A gain the allowlist covers is still printed, marked allowed, with the line and reason that allowed it.

      • --fail-on-gain and --fail-on-loss fail on any change the allowlist doesn't cover.
      • The diff covers the relationships you give it: a fixture like the example, or a snapshot from staging or production. Objects in no relationship aren't covered.

      PR #213, and the same PR with one word wrong

      
              
      
              
      
              
        
              
        userAllowed by a line of the allowlistuserNo line expects it
        
              
        exit0
        
            
        
            
        All repository files: allow-pr213.txt, and the two relationship files that add one line each to the 30. Both diffs are real; the grants are their GAINED lines, verbatim. The slip also exposes something the schema always allowed: only view excludes contractors, so a contractor who can edit the company folder can edit payroll without being able to read it.
        
          
        
        
        
      
        
    
        

    
        
      
        
        
        
          
        7Fail the pull request
        
          
        In a workflow, take the base branch's schema with git show, diff it against the pull request's, and let the exit code decide. diff exits 1 when a gate trips, check exits 0 for yes and 1 for no, and every command exits 2 on bad input.
        
          
          
            
        • The relationships are a file in SpiceDB's text form, such as document:readme#viewer@user:alice.
          • 
            
        • The repository's own CI runs the tests, the 20,000-seed hunt, the mutant table, the SpiceDB crosscheck, and the cache reproducer against two servers, on every push.
          • 
          
        
        
        
        
        
          
        
            
        
              
        The workflow step, and CI on the repository
        
              
            
        
            
        # a step in .github/workflows/*.yml
- run: git show origin/main:authz/schema.zed > /tmp/schema-main.zed
- run: >
    authz-proof diff /tmp/schema-main.zed authz/schema.zed authz/relationships.txt
    --allow authz/allow.txt --fail-on-gain --fail-on-loss
        
            
        
            
        
              
        CI run 38658145655 on 1e6e95e5 jobs, all passed
        
              
          
            
          
            
          The workflow step is the README's. The terminal is the end of the refactor's real diff with --fail-on-gain. Job names, results and durations come from GitHub's API for that run, rounded to whole seconds.
          
          
          
        
          
      
          
    
          

    
          
      
          
        
          
          
          Measured, not assumed
          
          
          The SpiceDB comparison re-run here, with the cache on and off, and what a diff costs. One Linux machine, shared with other work while these ran.
          
        
          
        
          
          
          
            
          SpiceDB agrees, cache off
          
            
          600 random models, every question asked of both, after the four examples' 3,864:
          
            
          59,110 checks0 disagreements18.9 s in all
          
            
          83 random schemas refused by both, none by SpiceDB alone. 111 refused by authz-proof alone: 110 that depend on themselves through an exclusion, and 1 wildcard reached through a subject set.
          
          
          
          
          
            
          Cache on, answers drift
          
            
          The same crosscheck against a fresh SpiceDB with default settings, twice:
          
            
          Run 1: 26 disagreementsRun 2: 26
          
            
          Out of 59,110 checks, in 11 of the 600 models each time, on partly different seeds. The README's run found 14 in 7. The four examples agreed every time.
          
          
          
          
          
            
          A diff in milliseconds
          
            
          Wall time for the whole process, 966 checks per side, median of 50 runs:
          
            
          Refactor: 5.8 msSlip: 5.7 ms
          
            
          Each answer is cached per subject. Cost grows as objects times names times subjects; the README says plainly it hasn't been measured on a production snapshot, and neither has this page.
          
          
          
        
          
      
          
    
          

    
          
      
          
        
          
          
          27 tests, two of them against SpiceDB
          
          
          Counted with go test -count=1 -json ./...: 25 pass and 2 skip without a server. With SpiceDB v1.56.2 running and SPICEDB_ENDPOINT set, as CI's spicedb job runs them, the other 2 pass too. Go 1.27.2; vet and gofmt clean; go test -race -short ./... passes.
          
        
          
        
          
          
          
            
            
            
          
            
          
            
            
            Few tests, wide ones
            
            
              
              
            • Engine against the reference: one test runs the property checks on 2,000 seeds (200 with -short), and another requires every mutant to be caught within 300.
              • 
              
            • Schema: SpiceDB's precedence, the mixed-operator warning, what SpiceDB accepts, the refusals, and the evaluation order that puts dependencies first.
              • 
              
            • Engine and diff on the example: the drive's checks, cycles, lookups, expand agreeing with check, the shortest chain, the exclusion behind a no, the refactor, the reordering and the dropped parentheses.
              • 
              
            • Allowlist, relationships, generator, CLI: patterns and parsing, refusals, rendering, a deterministic generator whose acyclic mode has no cycles, bad input, and the CLI end to end.
              • 
              
            • SpiceDB: the examples and random models agree with a live server.
              • 
            
            
            
            CI runs vet, gofmt and the tests with -race -short and without, on Go 1.22 and stable, and the hunt, mutants and SpiceDB jobs alongside.
            
          
            
        
            
      
            
    
            

    
            
      
            
        
            
          
            
            
            Deliberately missing
            
            
            
              
            A server
            It loads a schema and a relationship file into memory and answers questions. No API, no storage, no consistency tokens, no watch.
            
              
            Data that doesn't exist yet
            "No access changes" means none for the objects and subjects in the file. Subjects in no relationship are covered by the stand-in; objects in no relationship aren't.
            
              
            Caveats
            Caveats and with, nil, and the .any() and .all() arrows are refused with a message.
            
              
            Every SpiceDB
            One version, one in-memory datastore, small acyclic random models. The findings are observations on that version, not claims about others.
            
            
            
          
            
          
            
            
            Run it
            
            
            git clone https://github.com/ahmed-hashim-pro/authz-proof
cd authz-proof
go build -o authz-proof ./cmd/authz-proof
go test ./...           # seconds

cd examples/drive
../../authz-proof diff schema.zed schema-refactor.zed \
  relationships.txt --fail-on-gain
../../authz-proof check schema.zed relationships.txt \
  document:payroll#view@user:bob
cd ../..
make check              # also the hunt and the mutants
make spicedb            # the crosscheck, SpiceDB in Docker
            
            
            Go 1.22 or newer, no dependencies. Without Go, the README builds it in golang:1.25 with Docker.