Your cloud configuration is a satisfiability problem

✓ Human-authored analysis; AI used for formatting and proofreading.

A team writes requirements for a healthcare app on AWS.

1. PHI data must never be anonymously readable.
2. The website must serve static assets to the public.
3. Both live in the same S3 bucket.
4. Encryption at rest is mandatory.
5. CloudTrail data events are required for the PHI bucket.

A scanner can check each of these against the live configuration. That's table stakes. The harder question is: can all five hold simultaneously on the same bucket? Once you ask it out loud, you can hear the contradiction. Requirements 1 + 2 + 3 cannot coexist. There is no S3 configuration where the same bucket is both anonymously readable and not-anonymously-readable. The compatibility check tells you the requirements themselves are inconsistent before you spend an engineering time trying to deploy them.

This is the difference between misconfiguration detection (a crowded space with every CSPM vendor) and configuration compatibility reasoning (a quiet space, Microsoft Research SecGuru did it for routing tables in 2015; almost nobody is doing it for cloud config). Stave is the second one, and this post walks through how.

Misconfiguration vs incompatibility

Misconfiguration: this setting is wrong right now. A linter for cloud. Useful but shallow.

Incompatibility: the union of these requirements cannot be satisfied by any configuration of this resource graph. A theorem for cloud. Different question.

The first answers "fix this one thing." The second answers "stop trying, your requirements contradict each other." A scanner cannot produce the second answer because it has no constraint set to reason over. It only has a pass/fail list.

Industry today has five layers consisting of IaC diff, policy-as-code, graph-based attack-path analysis, runtime CSPM blast-radius tools, and staging-plus-human-review. Each catches a slice. None reasons about whether the whole set of requirements is jointly satisfiable. That's a SAT problem, and SAT solvers have been verifying chip designs, flight control software, and TLS protocols for two decades. The technique is sound. The cloud security tooling category just hasn't applied it yet.

The SAT framing

Restate every requirement as a logical constraint over facts about the configuration:

phi(b)            sensitive data classification on bucket b
anonymously_reachable(b, p)  some principal p with public_principal(p) can s3:GetObject from b
website_hosted(b) static-website endpoint enabled on b
phi_invariant: forall b. phi(b) -> not (exists p. public_principal(p) and anonymously_reachable(b, p))

Plus the snapshot facts:

bucket(ping_api_production)
phi(ping_api_production)
website_hosted(ping_api_production)
allows_get_object(public_principal, ping_api_production)
public_access_block_disabled(ping_api_production)

Hand that to an SMT solver. Two outcomes:

• SAT There exists an assignment where every constraint holds. Your safety envelope is feasible against this configuration.
• UNSAT No such assignment exists. The constraints contradict, and the solver can hand back an unsat core: the minimal subset of constraints that produces the contradiction.

That unsat core is the killer feature. "You said PHI must not be public, the website must be public, and they share a bucket. Three of your six requirements directly contradict, here are the three." A scanner can list ten findings; the unsat core hands you the exact subset that proves the system as stated cannot work.

Why this is tractable: the Pareto narrowing

Modeling all of AWS in logic is intractable. The team did the math: there are ~280 services, each with hundreds of properties, and the combinatorial state space explodes. SMT solvers are powerful.

The trick is that you don't need all of AWS. Two Pareto observations narrow the space:

First Pareto: 20% of unsafe states cause 80% of severe cloud incidents. Public storage, excessive IAM trust, exposed secrets, weak network boundaries. The disclosed-breach corpus repeats. You don't model every possible cloud state. You model the unsafe ones that have caused $300M incidents.

Second Pareto: 20% of relationships drive most attack paths. IAM role assumption, internet reachability, public/private boundary crossing, production access chains. Most edges in the cloud graph are uninteresting (an EC2 tag does not affect data exposure). Your solver needs to see the few that are interesting.

Combined: a few hundred high-value unsafe states + a few dozen critical relationship types = a tractable model. Stave ships 700+ controls and 80+ chains framed this way. Each control is a constraint over a small predicate vocabulary. Each chain is a compound assertion across services. The state space is large enough to find real incidents and small enough for any SMT solver to handle in milliseconds.

How Stave maps to this design

The architecture mirrors a compiler:

snapshot.json  →  facts  →  SMT constraints  →  solver verdict  →  cloud-facing explanation

Each arrow is a separate process, separately testable and versioned. Layer-by-layer:

Snapshot → facts. Stave reads obs.v0.1 snapshot JSON and projects it into a normalized fact stream. The projector lives in internal/core/sir/ and produces facts like phi(bucket-xyz), allows_anonymous_read(bucket-xyz), public_access_block_disabled(bucket-xyz) — clear domain vocabulary rather than raw AWS field names. Every fact carries provenance (which snapshot, which property path, which evidence) so the solver verdict traces back to source.

Facts → constraints. Stave's controls are constraints. A control's unsafe_predicate: block is the assertion that this combination of facts is forbidden:

id: CTL.S3.ACCESS.PHI.001
unsafe_predicate:
  all:
    - field: properties.storage.data_classification
      op: eq
      value: phi
    - field: properties.storage.access.public_read
      op: eq
      value: true

That's a per-resource constraint. Chains are compound constraints across resources:

id: cognito_unauth_escalation
controls:
  - CTL.COGNITO.IDENTITY.GUEST.001
  - CTL.COGNITO.IDPOOL.UNAUTH.IAM.001
  - CTL.COGNITO.IDPOOL.UNAUTH.LAMBDA.001
escalation_threshold: 2
compound_severity: critical

Three constraints; the chain fires when any two co-occur. That is configuration incompatibility detected via composition. The chain represents a stated invariant ("guest access on AND a path to elevated capability is forbidden") that cannot hold simultaneously with the snapshot facts.

Facts + constraints → solver input. stave export-sir --format smt2 emits the entire fact stream and the active control predicates as a closed-world SMT-LIB v2 document. Pipe it to Z3:

stave export-sir --format smt2 --observations ./snapshots/ > facts.smt2
echo "(check-sat)" >> facts.smt2
z3 facts.smt2

SAT means the unsafe state is realizable in this snapshot. There is a path from unauthenticated user to PHI. UNSAT means there is no path and your safety envelope holds.

Solver verdict → explanation. A raw (error ...) from a solver is useless to a CISO. Stave maps every constraint back to its source control, its compliance citation, its remediation, and its provenance. Findings ship with description, remediation.{description,action,example}, and fix_plan. The human-facing translation of the formal verdict.

The same fact stream can drive other engines. --format jsonl produces triple-form facts that Soufflé (Datalog), Clingo (ASP), Prolog, or PySAT can consume. There is no SMT lock-in. The fact stream is the contract. The repo's examples/engines/ directory has runners for five.

The unsat-core feature in production

The end-to-end is one query you can run today. The "Tagged 'Internal', Readable by Everyone" case from Shopify (HackerOne #1021906) is exactly the contradiction pattern. The bucket carried data-classification: internal and a policy with Principal: *. Two requirements stated explicitly on the same resource. UNSAT.

A scanner reports "public S3 bucket." Useful. Insufficient.

Stave's framing reports the per-control conflict in plain English: which property of the configuration violates which named invariant, with the offending field path and the property value as evidence. The team that owns the bucket reads control_description and remediation.action and knows which decision needs to flip. That's the unsat-core idea, delivered without forcing the operator to read solver output.

The Shopify case is in the e2e suite: testdata/e2e/e2e-h1-shopify-1021906/. The fixture is a reconstructed snapshot from the public disclosure. CTL.S3.PUBLIC.001 fires. The golden output is committed. The "compatibility check failed" is reproducible at any time by running make test-e2e.

Why the layers matter: debugging UNSAT

The four-stage pipeline (snapshot → facts → SMT → explanation) gives you fault isolation that monolithic scanners cannot offer. When a finding looks wrong:

Each layer has its own test corpus. The fact stream is committed JSONL. The SMT-LIB output is committed .smt2. The solver verdict is committed JSON. The cloud-facing report is committed Markdown. A failing test surfaces the exact layer where reality diverges from expectation. That is the difference between a scanner you fork and a verification system you can audit.

Mutation testing for cloud security

This is the test discipline the SAT framing unlocks. Take a known-safe snapshot. Perturb one fact by flipping BlockPublicPolicy from true to false. Re-run the verdict. The system must transition from SAT (safe envelope holds) to UNSAT (PHI reachable). If it doesn't, the model is missing a constraint and the test caught it.

Stave's examples/ directory is structured this way. Each example has a writeup-config/ (the breach state) and a remediated-config/ (the fix), both as observation directories. stave apply on the first produces findings; on the second, it produces none. That's a one-fact mutation test, and there are 70+ of them in the repo today, each tied to a publicly disclosed incident.

What this isn't

It is not "use Z3 to check your cloud." Z3 alone gives you cryptic solver output. The product value is in the four layers around it consisting of the fact projection, the named constraints, the provenance, and the cloud-facing explanation. The solver is the easy part; the encoding is the hard part.

It is not "model every AWS service." The Pareto narrowing is doing real work. You model the high-value unsafe states and the relationships that drive attack paths. Everything else stays out of the formal model.

It is not a replacement for runtime CSPM. CSPM watches the live cloud; Stave reasons over snapshots. They compose: CSPM tells you what changed, Stave tells you whether the change broke your safety envelope.

Try it

git clone https://github.com/sufield/stave
cd stave && make build

# A reproduction of HackerOne #1021906 — the Shopify Tag/Policy contradiction
./stave apply \
  --controls testdata/e2e/e2e-h1-shopify-1021906/controls \
  --observations testdata/e2e/e2e-h1-shopify-1021906/observations \
  --max-unsafe 168h \
  --eval-time 2026-01-15T00:00:00Z \
  --format json | jq '.findings[].control_id'

# Export the same case as SMT-LIB; feed to z3 / cvc5 / Yices for an independent verdict
./stave export-sir --format smt2 \
  --controls testdata/e2e/e2e-h1-shopify-1021906/controls \
  --observations testdata/e2e/e2e-h1-shopify-1021906/observations \
  --eval-time 2026-01-15T00:00:00Z > /tmp/shopify.smt2

echo "(check-sat)" >> /tmp/shopify.smt2
z3 /tmp/shopify.smt2

The first command lists the controls that fire. Stave's verdict on the configuration. The second hands the same fact base to Z3 and asks the solver for an independent satisfiability verdict. Two engines agreeing is the strongest signal this technique can produce.

The design choice underneath

The reason this works is one architectural decision: files are the boundary between cloud evidence and reasoning. The snapshot is a file. The facts are a file. The SMT-LIB encoding is a file. The verdict is a file. The explanation is a file. Each file is a versioned contract.

Once that's true, you can swap reasoning engines without touching Stave. Soufflé for blast-radius enumeration, Z3 for SAT/UNSAT verdicts, Clingo for constraint satisfaction, Prolog for proof trees, PySAT for boolean compound checks. The contract is the JSON, not the API.

That turns "we use a solver" into "we reason about your configuration." The product value is not in any one engine. It is in the encoding boundary that lets any engine consume it. Configuration compatibility reasoning becomes a property of the data, not a property of one tool's runtime.