✓ Human-authored analysis; AI used for formatting and proofreading.
Every cloud security scanner on the market such as Prowler, ScoutSuite, Checkov, AWS Config Rules operates the same way. It evaluates individual resources against individual rules. S3 bucket: is public access blocked? IAM role: is the trust policy scoped? Security group: are ports restricted?
Each finding is correct. Each resource passes or fails its check. And the security team reports: 847 findings, 12 critical, here's your posture score.
The report is formally meaningless as a system-level safety claim.
This is a theoretical impossibility. You cannot derive system-level safety from component-level findings alone. The result has been proven, reproven, and formalized across four decades of computer science. The cloud security industry has collectively ignored it.
This article traces the formal lineage, shows why it matters practically, and describes what a verification framework that addresses system-level safety would require.
The result
The core claim: individual component safety proofs are insufficient for system-level safety. You need explicit specifications of the interfaces between components — what each component assumes about its environment, and what it guarantees to its environment. Without those interface specifications, individual safety proofs tell you nothing about the composed system.
This has been formally established across multiple independent lines of work.
The lineage
Owicki and Gries (1976) got there first. Working on proofs of parallel programs, they showed that a process with a valid individual correctness proof could behave incorrectly in composition because another process modified shared state that the first process's proof assumed was stable. They called this the non-interference problem.
The practical translation: you can prove that process A is correct in isolation, prove that process B is correct in isolation, compose them, and get an incorrect system. The individual proofs are valid. The composition is broken. The proofs failed because they didn't specify what each process assumed about its environment.
Jones (1983) provided the constructive solution: rely-guarantee reasoning. Each component specifies two things:
- A rely condition: what the component assumes its environment will or will not do
- A guarantee condition: what the component promises to its environment
Composition is valid if and only if each component's guarantee satisfies every other component's rely condition. If component A relies on shared state S being stable, and component B's guarantee includes modifying S, the composition is invalid — regardless of whether A and B individually pass their proofs.
Jones didn't just prove that the problem exists. He proved what the solution requires: explicit interface contracts between components. Without them, composition is unverified.
Lamport (1977) formally defined the two categories of correctness properties:
- Safety properties: "nothing bad ever happens" — the system never enters a forbidden state
- Liveness properties: "something good eventually happens" — every request eventually gets a response, every failure eventually triggers recovery
Lamport proved that safety properties are closed under intersection. If two components each satisfy a safety property, the composed system satisfies the intersection of those properties. But here's the critical subtlety: that intersection may be weaker than the global safety property you need. The system-level property may require coordination between components that neither component's individual proof addresses. The intersection is formally valid and semantically vacuous — it proves the system is "safe" only because the assumptions rule out all real executions.
Abadi and Lamport (1993), in "Composing Specifications," formalized this precisely. They showed that composing specifications requires a compatibility condition between the assumptions and guarantees of each component. Without proving compatibility, the composed specification may be satisfiable but only in degenerate cases that don't correspond to any real system behavior.
The degenerate case has a name: vacuous correctness. A composition is vacuously safe when the assumptions of the components are mutually exclusive — component A assumes the environment provides X, component B assumes the environment provides ¬X. Both components are individually correct. The composition is correct only because no real execution satisfies both assumptions simultaneously. In cloud terms: the system is secure because the network configuration prevents anyone from reaching the S3 bucket. But the bucket is also useless, because the network configuration prevents anyone from reaching it. The scanner reports zero findings. The system satisfies no business requirement. The safety proof is real and the safety is meaningless. Vacuous correctness is the result when you verify components without checking that their assumptions are mutually satisfiable.
The result, consolidated: you cannot verify system safety by verifying components individually. You must also verify that the interfaces between components — the rely-guarantee pairs, the assumption-guarantee contracts are mutually compatible. Any verification framework that evaluates only individual components is formally incapable of making system-level safety claims.
The cloud security application
Consider two AWS resources, each individually configured according to security best practices.
Resource A: an S3 bucket. Its bucket policy grants s3:GetObject to IAM role role-X. A scanner evaluates this bucket and passes it: access is restricted to a specific role. No public access or wildcard principals. Clear finding.
Resource B: an IAM role. role-X has a trust policy allowing sts:AssumeRole from any EC2 instance in the account via an instance profile. A scanner evaluates this role and passes it: the trust policy is scoped to a specific service principal (ec2.amazonaws.com) within the account. No cross-account trust or wildcard. Clear finding.
The composition: any EC2 instance in the account, including a compromised developer workstation, an unpatched test instance, or an attacker-controlled instance launched through a separate privilege escalation can assume role-X and read every object in the bucket.
The system is insecure. Both components passed their scans. The vulnerability exists only at the edge — the relationship between the bucket policy and the role's trust boundary.
In Jones's framework, the problem is precise: the S3 bucket's rely condition (implicit, unstated) is that role-X is assumable only by authorized, trusted principals performing authorized operations. The IAM role's guarantee (any EC2 instance can assume it) violates that rely condition. The violation is invisible to any tool that evaluates components individually because the rely condition is not a property of either component. It is a property of the interface between them.
Why node-level scanning is structurally insufficient
Better rules cannot fix this gap. It is a structural limitation of the verification framework itself.
A node-level scanner evaluates a function: f(resource) → {pass, fail}. The input is a single resource configuration. The output is a finding. The scanner's formal power is limited to properties expressible as predicates over individual resource states.
System-level safety properties are not predicates over individual resource states. They are predicates over paths through the resource graph — sequences of edges that, taken together, create an access path, a data flow, or a trust chain that violates a system invariant.
"No unauthorized principal can read objects in bucket B" is not a property of bucket B's configuration. It is a property of every path through the resource graph that terminates at bucket B. It depends on every IAM role that the bucket policy references, every trust policy on those roles, every policy attachment that grants permissions to principals that can assume those roles, and every resource policy on every intermediate resource in the chain.
A scanner that evaluates bucket B's configuration cannot verify this property. It doesn't have the information. The property is not in bucket B — it is in the graph.
This was proved by Owicki and Gries in 1976 for parallel processes, what Jones formalized in 1983 for compositional verification, and what Abadi and Lamport generalized in 1993 for specification composition. The cloud security industry is rediscovering — slowly, expensively, breach by breach — a result that has been formally established for half a century.
What Capital One proved empirically
The 2019 Capital One breach was not a code bug. It was a compound misconfiguration. Four individually-reasonable configurations composed into an exploitable access path:
- A WAF with an SSRF vulnerability (a code bug, but the only code bug in the chain)
- An EC2 instance with access to the AWS metadata service (standard default at the time)
- An IAM role attached to that instance with overly broad S3 permissions (individually assessable, but assessed in isolation)
- S3 buckets containing sensitive data accessible to that role (individually compliant — access was restricted to a specific role)
A node-level scanner evaluating each of these four resources individually would pass three of them. The WAF SSRF might be caught by a code-level scanner (Chris Betz's framework). But the compound misconfiguration — the path from SSRF through metadata service through IAM role to S3 bucket was invisible to any tool evaluating individual resources.
In Jones's terms: the S3 bucket relied on its granting role being assumable only through authorized code paths. The IAM role guaranteed it was assumable by any code running on the EC2 instance. The metadata service guaranteed it would dispense temporary credentials to any process on the instance. Each component's guarantee violated the next component's rely condition. No individual scan could detect this because the violation existed only at the interfaces.
Capital One's breach was an empirical proof of Owicki and Gries (1976). The industry treated it as an operational failure. It was a theoretical inevitability.
What compositional verification requires
If node-level scanning is structurally insufficient, what is sufficient?
Jones's rely-guarantee framework provides the answer, translated to cloud security:
Step 1: Define system-level safety properties. These are the invariants the system must satisfy — not properties of individual resources, but properties of the system as a whole. Examples: "No principal outside the production account can assume any role with access to customer data." "No network path exists from any public-facing resource to any database resource that does not traverse a WAF and an authentication layer." "No IAM policy grants s3:* to any role assumable by a service principal."
Step 2: Model the resource graph. Resources are nodes. Relationships (policy references, trust chains, network routes, data flows) are edges. The graph is the artifact under verification, not the individual resources.
Step 3: Encode rely-guarantee contracts for each resource. For each resource, specify: what does this resource assume about the resources it depends on (rely condition), and what does this resource promise to the resources that depend on it (guarantee condition)? For an S3 bucket that grants access to a role, the rely condition is that the role's trust policy restricts assumption to authorized principals. For the role, the guarantee condition is the actual set of principals that can assume it.
Step 4: Verify compositional compatibility. Check that every resource's guarantee satisfies every dependent resource's rely condition. Any violation is a compound misconfiguration — an edge-level vulnerability that no node-level scanner can detect.
Step 5: Verify system properties against the composed specification. Using the verified composition, check whether the system-level safety properties (Step 1) hold. This is where formal reasoning engines — SAT solvers, SMT solvers (Z3), Datalog engines (Soufflé) become necessary. The state space is too large for exhaustive enumeration but structured enough for formal analysis.
Formally, this step is a refinement check: verifying that the low-level configuration (the implementation — the resource graph as deployed) refines the high-level safety property (the specification — the system-level invariants defined in Step 1). Refinement means every behavior permitted by the implementation is also permitted by the specification. If the implementation allows an access path that the specification forbids, the refinement check fails, and the system is provably insecure with respect to that property. Formal verification goes beyond testing: a test checks whether a specific behavior occurs; a refinement check proves whether any forbidden behavior is possible.
This is compositional verification when applied to cloud security. It requires evaluating edges, not nodes. It requires a specification of what secure means at the system level, not just a catalog of individual resource checks. It requires reasoning engines capable of operating over the graph, not just over individual vertices.
What the industry builds instead
The industry builds node-level scanners and adds more rules.
Every time a new breach reveals a compound misconfiguration, the response is to add a rule to the scanner. After Capital One, tools added checks for IMDSv2, for overly broad IAM policies, for specific known-dangerous policy patterns. Each rule catches the specific compound path that the breach revealed. It does not catch the class of compound misconfiguration.
This is the equivalent of responding to Owicki and Gries by adding more test cases instead of adopting rely-guarantee reasoning. It patches the last breach. It does not verify the system against the next one.
The result is a growing catalog of rules. Prowler has over 300, AWS Config has hundreds more — each of which evaluates an individual resource against an individual predicate. The catalog grows. The false positive rate grows. The coverage of system-level safety properties does not grow, because the verification framework is structurally incapable of evaluating system-level properties.
The specification that is missing
The deepest problem is the absence of a specification.
Every cloud deployment is a system. Every system has safety properties it must satisfy. But almost no organization has written those properties down as formal, mechanically-checkable specifications of the system-level invariants that must hold.
Without a specification, verification is impossible. You can scan. You can discover. You can report findings. But you cannot verify, because verification requires a specification to verify against.
This is the missing specification. A formal description of what secure means for this specific system, expressed as properties over the resource graph, verifiable by formal reasoning engines.
The Owicki-Gries-Jones-Lamport lineage doesn't just prove that compositional verification is necessary. It proves what the inputs to compositional verification must be: component-level rely-guarantee contracts, a compatibility verification between those contracts, and system-level safety properties to verify against the composed specification.
The industry has none of these. It has node-level rules, individual findings, and posture scores. It has taken a formally insufficient verification framework and built an entire market around it.
Where this leads
The formal result is clear: system-level security requires system-level verification. System-level verification requires a specification of system-level properties, a model of the resource graph, and formal reasoning over the composition.
The theoretical foundations are 50 years old. The practical tools exist — SMT solvers, Datalog engines, model checkers. The artifact required for verification (the cloud configuration snapshot) is exportable from every major cloud provider as JSON.
What the industry lacks is the practice of defining system-level security properties and verifying them compositionally. Until that practice exists, every cloud security scanner on the market is formally incapable of answering the question it claims to answer: is this system secure?
Individual findings are not system security. The math proved this in 1976. It's time the industry caught up.
Top comments (0)