✓ Human-authored analysis; AI used for formatting and proofreading.
If you had read the article on Google Has 1,000 Platform Engineers Making Security Invisible. You Have Zero. Here's How Agents Close the Gap., you might be thinking: "Is what you're describing just Security as Code?"
It starts there. But it doesn't end there. Compound breaches, the Capital One pattern, the multi-hop privilege escalation, the toxic combination live undetected in the gap between where Security as Code ends and where the next step begins.
What Security as Code does well
Security as Code brought a discipline to cloud security that didn't exist before: security policies defined as machine-readable code, version-controlled alongside infrastructure, automatically enforced in CI/CD, testable, reviewable, auditable.
Before Security as Code, security checks were manual audits, spreadsheet checklists, and annual penetration tests. After Security as Code, every pull request runs against a policy engine. Every deployment is gated by automated checks. Every rule is in version control with a review history.
This was a genuine paradigm shift. Tools like OPA/Rego, Checkov, Sentinel, Semgrep, tfsec, and Cedar moved security from a periodic human activity to a continuous automated process. The impact is real and substantial.
What Security as Code checks
Every Security as Code tool does the same thing at the structural level: it evaluates whether a specific configuration matches a specific rule.
Input: One configuration (a Terraform plan, an IAM policy, a K8s manifest)
Rule: One pattern (is this bucket public? is this port open? is this role admin?)
Output: Yes or no. This configuration matches (or doesn't match) this rule.
The evaluation is per-resource, per-rule. Checkov checks whether THIS S3 bucket has public access enabled. OPA checks whether THIS Kubernetes pod runs as root. Semgrep checks whether THIS code path has unsanitized input. Each check is a pattern match: does the configuration text match the rule pattern?
This catches a large class of misconfigurations. The class it catches: individual resources with individual misconfigurations that are visible in the text of the configuration.
What Security as Code doesn't check
The class it DOESN'T catch: properties that emerge from the interaction between multiple resources.
The Capital One breach (2019) had five components. Each was individually configured. Each would pass a per-resource security check. The breach existed in the COMPOSITION:
Component 1: Public-facing WAF → correct for its purpose
Component 2: EC2 instance behind the WAF → correct for its purpose
Component 3: IAM role on the EC2 instance → correct for its purpose
Component 4: S3 bucket with customer data → correct for its purpose
Component 5: Role trust allowing EC2 → S3 access → correct for its purpose
Each component: PASS (individually configured correctly)
The composition: FAIL (WAF → EC2 → IAM → S3 = public to customer data)
No per-resource Security as Code rule catches it. Checkov checks each resource individually. OPA evaluates each policy individually. Each returns PASS. The breach exists in the relationships BETWEEN resources and no single rule sees all five simultaneously.
It's a limitation of the PATTERN: one resource, rule and evaluation. The pattern can't express "does there exist ANY path from a public endpoint to a sensitive resource through ANY chain of role assumptions, policy attachments, and trust relationships?"
That question requires something different.
Two different operations
The distinction is between CHECKING and PROVING:
CHECKING (what Security as Code does):
"Does this configuration match this rule?"
Input scope: one resource
Rule scope: one pattern
Method: pattern matching on configuration text
Output: pass/fail for this resource against this rule
What it means: "this resource has (or doesn't have) this specific problem"
PROVING (what reasoning engines do):
"Does this property hold across all resources and all their relationships?"
Input scope: the entire configuration graph
Rule scope: a property expressed over relationships
Method: logical inference, satisfiability checking, transitive closure
Output: verified/violated with evidence trace
What it means: "this property holds everywhere" or "here is the specific
path/composition that violates it"
Checking asks: "does this resource match this pattern?" Proving asks: "does this property hold across all resources and their interactions?" The first is a pattern match. The second is a logical derivation.
How the two work together
They're complementary layers, like types and tests:
Layer 1 — Per-resource rule checking (Security as Code):
CEL predicates evaluate each asset against each control.
2,662 controls. Per-resource. Per-rule. Fast. Deterministic.
Catches: individual misconfigurations
Example: "This bucket has public access enabled"
Example: "This role has admin-level permissions"
Example: "This security group allows SSH from 0.0.0.0/0"
Tools: OPA, Checkov, Semgrep, tfsec, Cedar, Stave's CEL controls
Layer 2 — Cross-resource property proving (Reasoning engines):
SMT solvers, Datalog, Prolog evaluate properties over relationships.
Transitive closure. Satisfiability. Reachability.
Catches: compound risks that emerge from composition
Example: "A privilege escalation path exists through 3 role assumptions"
Example: "This policy is mathematically equivalent to Principal: *"
Example: "A public endpoint can reach a sensitive resource through
a chain of individually-safe configurations"
Tools: Z3, Soufflé, Prolog, Clingo, AWS Zelkova, Stave's SIR exports
Layer 1 checks settings. Layer 2 proves properties about compositions. You need both.
A team with only Layer 1 catches every misconfigured bucket but misses the Capital One pattern. Because each component passes individually. A team with only Layer 2 proves compound properties but misses the simple misconfiguration. Because the reasoning engine doesn't check every setting against every rule.
The practical workflow
The two layers run in sequence on the same snapshot:
Step 1: Capture configuration snapshot (all resources, all relationships)
Step 2: Layer 1 — Per-resource checks (Security as Code)
stave apply → evaluates 2,662 CEL controls against each asset
Catches: individual misconfigurations, per-resource violations
Output: per-asset findings (the equivalent of Checkov/OPA results)
Step 3: Layer 2 — Cross-resource proving (Reasoning engines)
stave export-sir → emits observation properties as triples
Soufflé/Prolog → computes transitive closure over role chains
Z3 → proves satisfiability of composed policy logic
Catches: compound chains, mathematical equivalences, reachability
Output: property-level verdicts with evidence traces
Step 4: Combined report
Per-resource findings (Layer 1) + property verdicts (Layer 2)
The CISO gets: "12 individual misconfigurations AND 2 compound
attack paths that wouldn't be detected by per-resource checks"
Layer 1 is fast and covers the full catalog. Layer 2 is deeper and covers the compound cases. Both evaluate the same snapshot. Both are deterministic. Both produce evidence.
Where Security as Code tools sit
Tool Layer 1 (rules) Layer 2 (properties) Notes
──────────── ─────────────── ──────────────────── ──────────────
Checkov Yes No Terraform/K8s rules
OPA/Rego Yes Limited Can express some cross-resource
Semgrep Yes No Code patterns
tfsec Yes No Terraform rules
Cedar Yes No AWS policy language
Sentinel Yes No Terraform Enterprise
AWS Config Rules Yes No AWS-managed rules
Prowler Yes No AWS CIS/HIPAA checks
ScoutSuite Yes No Multi-cloud audit
AWS Zelkova No (internal) Yes IAM policy satisfiability
AWS Tiros No (internal) Yes VPC network reachability
Stave Yes (CEL) Yes (SIR → Z3/Datalog) Both layers, open source
Most tools are Layer 1 only. AWS has Layer 2 internally (Zelkova, Tiros) but it's not available as a general-purpose tool. It's embedded in specific AWS services (IAM Access Analyzer, VPC Reachability Analyzer). The gap in the market is an open-source tool that does both layers against any configuration snapshot.
Why this distinction matters for practitioners
If you're evaluating cloud security tooling, the question to ask is:
"Can this tool detect a vulnerability that exists only in the composition of multiple correctly-configured resources?"
If the tool evaluates one resource at a time (Layer 1 only), the answer is no. It can catch every individual misconfiguration. It cannot catch the Capital One pattern.
If the tool exports to a reasoning engine that computes transitive closure, satisfiability, or reachability (Layer 2), the answer is yes — for the properties the engine is configured to check.
Both layers are necessary. The individual misconfiguration (open SSH port, public bucket, admin-level role) is the common case. The compound composition (WAF → EC2 → IAM → S3) is the breach case. The tool that catches only the first gives you a false sense of completeness. The tool that catches both gives you the coverage your auditor is asking about.
The terminology, clarified
Term What it means Layer
────────────── ───────────────────────── ─────
Infrastructure as Code Define infrastructure as code Input (what's deployed)
Policy as Code Define policies as code Layer 1 rules
Security as Code Define security checks as code Layer 1 checks
Formal Verification Prove properties mathematically Layer 2 proofs
"Security as Code with formal verification" = both layers
Security as Code is Layer 1. Formal verification is Layer 2. You need both. The term for both layers together doesn't have an established name yet. Because almost no tool does both. As the compound detection gap becomes more visible (more Capital One pattern breaches, more multi-hop escalations), the vocabulary will emerge. For now: "Security as Code extended with formal verification" is precise. "Reasoning engine" describes the Layer 2 mechanism without requiring the audience to know formal methods terminology.
The per-resource checks described in this article are implemented as 3,000+ CEL controls in Stave. The cross-resource property proving is implemented through Stave's SIR (Stave Intermediate Representation) export, which emits observation properties as triples consumable by Z3, Soufflé, and Prolog. Both layers evaluate the same configuration snapshot. Both are deterministic. Both are open source. Apache 2.0.
Top comments (0)