Four Security Problems That Don't Need a Scanner

There's a class of cloud security problem where writing a scanner is the wrong move.

They're the right tool for behavioral detection — anomalous API calls, unusual traffic patterns, credential stuffing attempts. But a meaningful fraction of cloud security problems aren't behavioral. They're structural. The configuration is wrong, and it's wrong right now, and you can determine that from the configuration alone without watching anything happen at runtime.

For structural problems, the scanner approach — write procedural code that traverses infrastructure, checks properties, accumulates findings — is both more effort and less coverage than the alternative: write a declarative constraint that says what must be true, and let a reasoning engine determine whether it holds.

Here are four classes where this applies. Each one maps to a real-world incident, a real constraint, and a real evaluation strategy.

Class 1: Exposure boundaries

The Toyota leak in 2022. A data server containing customer records was accessible from the public internet for many years. The configuration was a single property on a single resource — but nobody checked it continuously.

This is the simplest class: a binary violation of an organizational boundary. An asset designated as internal has a direct path to the unauthenticated internet.

The constraint:

// CEL predicate — Stave atomic control
asset.network.ingress_source == "0.0.0.0/0" &&
asset.tags.exists(t, t.key == "DataClassification" && t.value == "Internal")

That's it. No traversal code. No API pagination. No retry logic. No state management. The predicate evaluates against a snapshot of the configuration, returns true or false, and the finding includes the specific resource and the specific property.

The procedural alternative — a Python script that paginates through every security group, checks each rule, cross-references tagging, handles API throttling, manages credentials — is 200-400 lines for the same check. It needs to be rewritten when the cloud provider changes their API response format.

The constraint doesn't change. The snapshot format absorbs the API changes. The predicate stays the same.

Other examples in this class: public S3 buckets, databases with 0.0.0.0/0 on port 3306, unauthenticated API Gateway endpoints, EBS volumes without encryption in regulated environments.

Class 2: Toxic combinations

Capital One, 2019. No single resource was misconfigured. A public-facing proxy had an IAM role. The role had a policy permitting S3 read. The bucket contained sensitive data. Four resources, each individually within normal parameters, whose composition created an exploitable path.

This is the class where scanners structurally can't help. A scanner's inner loop is for resource × rule → match?. A composition check's inner loop is for resource_tuple × constraint → match?. The scanner checks properties of individuals. The constraint checks properties of combinations.

The constraint:

// CEL predicate — Stave compound control
// Does a principal-policy-resource chain exist?
asset.type == "aws_iam_role" &&
asset.trust.allows_service("ec2.amazonaws.com") &&
asset.permissions.actions.exists(a, a.startsWith("s3:Get")) &&
asset.permissions.resources.exists(r, 
    r.tags.exists(t, t.key == "DataClassification" && t.value == "PII"))

This is still a predicate — a boolean function over a state. But the state it ranges over is the composition of multiple assets, not a single resource. The reasoning engine evaluates it against the snapshot's resource graph, not against each resource individually.

For more complex reachability — "does any path exist from any public principal to any sensitive resource through the permission graph?" — the predicate language runs out. That's an existential query over a graph with transitive closure. Datalog handles it:

// Soufflé rule — transitive role assumption
can_assume(P, R) :- trust_policy(R, P, _).
can_assume(P, R2) :- can_assume(P, R1), trust_policy(R2, R1, _).

// Effective access via role chain
effective_access(P, Res, Act) :-
    can_assume(P, R),
    has_action(R, Act),
    has_resource(R, Res).

Six lines of Datalog replace what would be a recursive graph-traversal algorithm in procedural code — and the Datalog engine computes the fixed point correctly, handles cycles, and terminates provably.

Other examples: an IAM role that can both modify code and approve its own deployment pipeline, a user with iam:PassRole to a higher-privilege role, a Lambda execution role with broader permissions than the function's exposure warrants.

Class 3: Trust boundary violations

The SolarWinds supply chain attack exploited trust relationships between organizations. In cloud infrastructure, the simpler version happens constantly: a cross-account IAM role trust policy with a typo in the account ID, or a missing sts:ExternalId condition, silently opens access to an unintended party.

Trust paths form a directed graph. The question "does my environment trust anyone it shouldn't?" is graph reachability — the same mathematical structure as Class 2, but with the edge type being sts:AssumeRole trust rather than policy attachment.

The constraint:

// CEL predicate — trust policy weakness
asset.type == "aws_iam_role" &&
asset.trust.cross_account_assumes.exists(a,
    !organization.approved_accounts.contains(a.account_id)) &&
!asset.trust.has_condition("sts:ExternalId")

The procedural alternative needs to: list all roles, parse each trust policy document (which is a JSON string inside a JSON response), extract the Principal field, handle the multiple formats AWS uses for principals (ARN, account ID, service principal, wildcard), cross-reference against an approved account list, and check for condition blocks. That's 300-500 lines of code with a high density of edge cases.

The constraint expresses the invariant. The snapshot parser handles the edge cases once, for all constraints.

Other examples: OIDC providers for GitHub Actions with broad subject matching, SAML federation without group attribute filtering, service principal trust without aws:SourceAccount restriction (the confused deputy problem).

Class 4: Network isolation

AWS itself uses formal reasoning for this. AWS Tiros and Zelkova translate VPC routing tables, security groups, and NACLs into mathematical constraints and use an SMT solver to prove network isolation properties. They don't simulate traffic — they prove reachability algebraically.

The constraint:

// Pseudo-constraint — network isolation invariant
assert: can_reach(subnet_public_web, subnet_secure_db) == false

In practice, this is the most complex class because network reachability involves multiple overlapping rule sets (security groups, NACLs, route tables, VPC peering, transit gateways, endpoint policies) that compose in non-obvious ways. A security group allows traffic that a NACL denies. A route table permits a path that a VPC endpoint policy restricts.

The SMT approach converts each rule set into a set of linear constraints and checks satisfiability: "is there any packet (source IP, destination IP, port, protocol) that satisfies all the allow rules and none of the deny rules?" If the answer is unsatisfiable, isolation is proved. Not tested — proved.

No procedural code can match this. A scanner can check "is port 3306 open in this security group?" — a single-layer, single-resource check. It cannot check "is there any path from subnet A to subnet B across all layers of the network stack simultaneously."

Other examples: VPC peering with overlapping CIDRs creating unintended routes, transit gateway route table propagation bypassing firewall appliances, private subnets with accidental internet gateway routes.

What this gets you — and what it doesn't

The honest comparison:

Notice what the last row says. It does not say "mathematically covers all possible scenarios." It says the coverage boundary is defined by the constraints you write. If you haven't written a constraint for a pattern, the engine won't find it — just like a scanner won't find what it hasn't been coded to check. The difference is that the constraint is 3 lines instead of 300, so you write more of them, and the reasoning engine handles composition for free.

The real advantage is in Class 2-4 — the compositional and graph-reachability problems. For Class 1 (simple property checks), the declarative approach is more concise but not structurally more powerful. For Class 2-4, it's structurally more powerful because the reasoning engine can explore the combination space and compute transitive closure — capabilities that procedural code must reimplement from scratch for every check.

The separation that makes it work

The architectural insight is the separation of policy logic from execution engine:

Your constraints (CEL predicates)     →  What must be true
                                          ↓
Snapshot (JSON Schema-validated)      →  What is actually true
                                          ↓
Reasoning engine (Z3, Soufflé, CEL)   →  Does reality satisfy the constraint?
                                          ↓
Finding (typed, severitied, cited)    →  What to fix

The constraints are yours — domain-specific, authored by the team that understands the infrastructure, reviewable in pull requests, auditable for compliance. The reasoning engine is generic. It handles the combinatorial search, the graph traversal, the satisfiability checking. You don't write the search. You write the question.

This is the same separation that made SQL powerful: you describe the data you want (declarative), and the query optimizer figures out how to retrieve it (procedural). You describe the invariant that must hold (declarative), and the reasoning engine figures out whether it holds (procedural).

From CEL to Z3: how the constraints reach the solver

Most articles about declarative security skip the translation. You write a CEL predicate. An SMT solver speaks SMT-LIB. How does one become the other, and why does it matter?

Stave's reasoning-engine export pipeline works in two steps. First, the snapshot is decomposed into standardized facts — JSONL predicates like has_action(role_arn, "s3:GetObject"), trusts_service(role_arn, "ec2.amazonaws.com"), has_tag(resource_arn, "DataClassification", "PII"). These are the base facts about the actual configuration. Second, those facts are translated into the target engine's native format: SMT-LIB assertions for Z3, Datalog relations for Soufflé, ASP facts for Clingo.

The security invariant — the CEL predicate — becomes an assertion in the target language. The solver's job is to determine whether the assertion holds against the facts, or whether there exists a variable assignment (a principal, a path, a resource) that violates it.

Each problem class maps to a different solver strength:

Class 1 (exposure boundaries) is propositional. The CEL predicate translates to a direct SMT-LIB assertion:

;; SMT-LIB — does an internal asset have public ingress?
(declare-const ingress_source String)
(declare-const data_class String)
(assert (= ingress_source "0.0.0.0/0"))
(assert (= data_class "Internal"))
(check-sat)
;; SAT = violation exists. UNSAT = safe.

Z3 answers this in microseconds. The value of SMT for Class 1 is marginal — CEL evaluates these directly. The export matters for auditability: a compliance officer can see the mathematical proof that the invariant holds, not just a tool's verdict.

Class 2 (toxic combinations) is existential quantification over tuples. This is where the solver earns its keep:

;; SMT-LIB — does any principal-resource pair violate confidentiality?
(declare-const principal String)
(declare-const resource String)
(declare-const action String)
(assert (has_action principal action))
(assert (has_resource principal resource))
(assert (is_sensitive resource))
(assert (not (is_authorized principal resource)))
(assert (is_read_equivalent action))
(check-sat)
;; SAT = unauthorized access path exists. The model gives you which one.

When Z3 returns SAT, the model — the specific variable assignment that satisfies the formula — tells you which principal can reach which resource via which action. You don't enumerate paths; the solver finds them. This is the same technique AWS uses internally with Zelkova for IAM policy analysis.

But for transitive composition — role A can assume role B can assume role C — SMT's bounded quantification gets expensive. Datalog is the better engine here because fixed-point evaluation naturally computes transitive closure:

%% Soufflé — six lines, handles arbitrary role chain depth
can_assume(P, R) :- trust_policy(R, P, _).
can_assume(P, R2) :- can_assume(P, R1), trust_policy(R2, R1, _).

effective_access(P, Res, Act) :-
    can_assume(P, R), has_action(R, Act), has_resource(R, Res).

Class 3 (trust boundaries) is graph reachability with constraints. Both Z3 and Soufflé handle it, but with different tradeoffs. Z3 can prove that no unauthorized trust path exists (UNSAT = proved safe). Soufflé can enumerate all unauthorized trust paths (every fact in the effective_access relation that violates the authorization model). Proof vs. enumeration — pick the one your workflow needs.

Class 4 (network isolation) is where SMT is structurally dominant. Network rules are linear constraints: "allow TCP from 10.0.0.0/24 to 10.1.0.0/24 on port 443" is a conjunction of range checks. Security groups, NACLs, and route tables compose as layers of constraints. The satisfiability question — "does any packet exist that passes all allow rules and no deny rules across all layers?" — is a natural SMT problem. This is how AWS Tiros works internally.

;; Simplified — network isolation check
(declare-const src_ip (_ BitVec 32))
(declare-const dst_ip (_ BitVec 32))
(declare-const dst_port (_ BitVec 16))
;; Security group allows
(assert (bvuge src_ip #x0A000000))  ;; src in 10.0.0.0/24
(assert (bvule src_ip #x0A0000FF))
;; NACL denies
(assert (not (and (bvuge dst_ip #x0A010000) ;; dst in 10.1.0.0/24
                  (bvule dst_ip #x0A0100FF))))
(check-sat)
;; UNSAT = isolation proved. SAT = reachable packet exists.

Datalog can't do this — it's relational, not arithmetic. Clingo (ASP) can approximate it but SMT is the native fit.

The right engine for each class:

The CEL predicate is the human-readable invariant. The SMT-LIB or Datalog translation is the machine-checkable form of the same invariant. The snapshot provides the facts. The solver provides the verdict. You author the invariant once in CEL, and the export pipeline translates it to whichever engine handles that class best.

This is why Stave exports to five engines (Z3, Soufflé, Clingo, Prolog, PRISM) rather than picking one. No single engine is optimal across all four classes. The invariant is the stable artifact; the engine is a deployment choice.

Not every security problem is structural. Behavioral detection — anomalous login patterns, unusual API call sequences, data exfiltration by volume — requires runtime observation, not snapshot analysis. Scanners, SIEM rules, and ML models are the right tools for those problems.

But for the four classes above — exposure boundaries, toxic combinations, trust violations, network isolation — a few lines of declarative constraints outperform thousands of lines of procedural scanner code. Not because declarative is always better. Because these problems are structural, and structural problems have structural solutions.

Stave is an open-source cloud security reasoning engine that evaluates CEL predicates against JSON Schema-validated configuration snapshots. It exports standardized facts to Z3 (SMT-LIB), Soufflé (Datalog), Clingo (ASP), Prolog, and PRISM for external reasoning — covering all four classes described above.