✓ Human-authored analysis; AI used for formatting and proofreading.
Each scanner checks one resource. Each check passes. The system is breached.
This is a composition gap. Three individually-correct configurations composed into an attack path that no individual check could see. The IAM role was valid. The Lambda was valid. The S3 bucket was valid. The PATH from anonymous user through Cognito through IAM through Lambda to PHI in S3 was the problem and no single-resource scanner can see a path.
The industry's response: build more scanners, check more resources, add more rules. More local checks. But the theorem says: local correctness does not compose to global correctness. More local checks produce more local verdicts. The composition is still not sound.
There's a different category of property namely safety properties where local checks DO compose to global guarantees. The theorem has been proven for 40 years. Distributed databases adopted it in the 2000s. Cloud security ignored it.
The theorem
Alpern and Schneider proved it in 1985, building on Lamport's 1977 work:
Safety properties are closed under conjunction.
If property A is a safety property and property B is a safety property, then A AND B is also a safety property. Enforcing both locally enforces both globally without any global reasoning step.
And the dual:
Correctness properties are NOT closed under composition.
Two components that are each locally correct can compose into a globally incorrect system. Local correctness does not guarantee global correctness.
Four words that separate two architectural categories:
Correctness emerges. Safety composes.
Safety vs Correctness
A safety property says: "the system must never be in this state." A forbidden state. A bucket must never be public. A role must never have unrestricted admin. An anonymous user must never reach PHI data.
A correctness property says: "the system must behave this way." A required behavior. The workflow must execute steps in order. The deployment must roll out blue-green. The audit must complete within 90 days.
The two LOOK similar. They're structurally opposite:
| Safety property | Correctness property | |
|---|---|---|
| About | States (configurations that must not exist) | Behaviors (sequences that must execute correctly) |
| Composition | Composes by conjunction — enforce A and B locally, get A∧B globally for free | Does NOT compose — components A and B each correct, composition can be incorrect |
| Scaling | 2,658 properties → 2,658 local checks. Linear. | 2,658 properties → ~7 million pairwise interactions. Quadratic. |
| Local enforcement | Sufficient — the theorem guarantees global safety | Insufficient — global reasoning required for every interaction |
| Once violated | Violated forever (you can't un-expose data) | Potentially recoverable (retry the workflow) |
The scaling row is the practical consequence. A safety-based system with 2,658 invariants runs 2,658 local checks and gets the conjunction for free — by mathematical theorem. A correctness-based system with 2,658 behaviors needs to reason about millions of pairwise interactions, and that's just pairs. Triplets, quadruplets, and higher-order interactions explode further.
Why every scanner has the same blindspot
Every cloud security scanner checks correctness: "is this resource configured correctly?" Each check is local. It evaluates one resource against one rule. Each check can pass.
The problem: local correctness doesn't compose. Three locally-correct resources can compose into a globally-unsafe system:
Scanner verdict (local correctness):
✅ Cognito identity pool: valid configuration
✅ IAM role: MFA required, valid trust policy
✅ S3 bucket: encryption enabled, versioning on
Actual state (global safety):
❌ Cognito pool grants anonymous access to IAM role
IAM role has Lambda invoke permission
Lambda writes to S3 bucket containing PHI
→ Anonymous user reaches PHI data
Every local check passed. The system is breached.
The scanner checked correctness (is each resource configured correctly?). The answer was yes for each resource. The COMPOSITION was unsafe. But the scanner's property (correctness) doesn't compose. Local correctness of A, B, and C does not guarantee global correctness of A+B+C. The theorem says so. The breach proves it.
Now consider the same resources checked for SAFETY (forbidden states):
Safety check:
"The state 'anonymous user reaches PHI' must not be reachable"
Compound chain evaluation:
CTL.COGNITO.UNAUTH.001 → unsafe (anonymous access to IAM role)
CTL.IAM.ROLE.SCOPE.001 → unsafe (role has Lambda invoke)
CTL.S3.PHI.MARKER.001 → unsafe (bucket contains PHI)
Conjunction: A ∧ B ∧ C → UNSAFE
The forbidden state IS reachable.
Gate blocks. The configuration never deploys.
The safety check composed. Three local safety verdicts conjoined into a global safety verdict — by the theorem. The compound chain is the conjunction. The conjunction is sound. The gate blocks.
Why compound chains are sound
Each compound chain is a conjunction of safety properties:
chain: bedrock_agent_tool_phi_exposure
constituents:
- CTL.BEDROCK.AGENT.OVERPRIVILEGED.001 # safety property A
- CTL.LAMBDA.IAM.S3_ACCESS.001 # safety property B
- CTL.S3.PHI.TAGGED.001 # safety property C
escalation_threshold: 3
The chain fires when ALL constituents co-fire. Mathematically: Chain ≡ A ∧ B ∧ C. Because A, B, and C are each safety properties (each says "this state must not exist"), their conjunction is also a safety property — by Alpern-Schneider.
585 compound chains over 2,650 controls. Each chain is a conjunction. Each conjunction is sound by the theorem. The compound-chain machinery works because the mathematics guarantees it.
A correctness-based system could not do this. Composing three correctness-checked controls would yield a correctness PATTERN, not a correctness PROPERTY. The pattern might be wrong because correctness doesn't compose. Three individually-correct components can produce an incorrect composition. The theorem forbids assuming otherwise.
Why the kernel can stay at 1,030 lines
The kernel evaluates each control locally against the snapshot. It does not contain global reasoning logic. It does not enumerate interactions between controls. It does not check whether control A's verdict conflicts with control B's.
This is sufficient because the theorem guarantees that local verdicts compose to a global verdict. The kernel doesn't need to perform the composition explicitly. It evaluates each control locally, and the conjunction is sound by Alpern-Schneider.
A correctness-based kernel would need global reasoning: "does control A's verdict interact with control B's verdict?" That reasoning grows with the number of controls. The kernel could not stay at 1,030 lines because the interaction space would need to be represented somewhere.
Safety composes locally. Correctness requires global reasoning. The kernel is small because the property it checks composes locally.
Why the catalog can grow without breaking
Today: 2,650 controls. Next year: maybe 5,000. The year after: maybe 10,000.
Each new control adds one more local safety property to the conjunction. The conjunction extends. The mechanism is unchanged. The soundness is maintained by the theorem. The kernel doesn't grow. The test surface doesn't grow (the kernel tests cover every new control automatically). The composition is still sound.
2,650 controls: 2,650 local checks → global safety (by theorem)
5,000 controls: 5,000 local checks → global safety (by theorem)
10,000 controls: 10,000 local checks → global safety (by theorem)
Kernel: unchanged. Soundness: unchanged. Growth: linear in data.
A correctness-based catalog couldn't scale this way. Adding control #2,651 to a correctness system means checking its interactions with all 2,650 existing controls — 2,650 new interaction pairs. Adding control #5,001 means 5,000 new pairs. The work grows quadratically. The system becomes unmaintainable.
Safety grows linearly. Correctness grows quadratically. The theorem makes the catalog growth possible.
Why multiple solvers agree
The SIR exports facts to five external solvers: Z3, cvc5, Soufflé, Clingo, Prolog. Each solver runs independently against the same facts. The expectation: all produce the same verdict.
This is meaningful BECAUSE safety composes. The question each solver answers is: "does the conjunction of safety properties hold?" That question has ONE answer, regardless of which solver asks it. Z3 UNSAT and cvc5 UNSAT and Soufflé "no model" all mean the same thing: no forbidden state is reachable.
For a correctness question, different solvers might verify different behavioral aspects and there would be no guarantee their verdicts agree, because correctness is not a single composable property. With safety, the convergence of independent solvers is meaningful because the question has a unique answer.
Why compliance profiles compose
HIPAA is a subset of controls. PCI-DSS is a different subset. A snapshot evaluated under HIPAA is safe iff the HIPAA controls' conjunction holds. Under PCI-DSS, iff the PCI-DSS conjunction holds. Under BOTH, iff the conjunction of both subsets holds.
By Alpern-Schneider, the conjunction of two safety subsets IS a safety subset. Evaluating "HIPAA AND PCI-DSS" requires no special interaction reasoning. It's evaluating each subset locally and conjoining. The compliance projector doesn't need to be sophisticated. It selects controls. The theorem carries the composition.
What the theorem forbids
Three patterns common in cloud security that violate the soundness argument:
Cross-asset behavioral reasoning
"Does the workflow across Service A and Service B execute correctly?" This requires reasoning about the BEHAVIOR of the composition — sequences, ordering, timing. Correctness question. Not compositional. Stave doesn't check this. It checks: "is Service A in a forbidden state? Is Service B? Does the conjunction indicate an unsafe path?" All safety questions. All compositional.
Eventually-consistent verdicts
"This will be correct eventually, after convergence completes." This is a liveness property — something good eventually happens. Liveness properties are NOT safety properties. Stave doesn't produce eventually-consistent verdicts. Each evaluation is one-shot: the property holds or it doesn't. No "will hold eventually."
Heuristic risk scores
A weighted "risk score" combining multiple findings with interaction-dependent weights. This is a behavioral judgment that depends on interaction patterns being scored. Stave doesn't produce heuristic risk scores. The verdict is a conjunction: the safety properties hold, or they don't. The aggregation is mechanical (count findings, rank by declared severity), not heuristic (weight interactions).
Each forbidden pattern would require global reasoning that the safety-composition framework doesn't need. Each would break the soundness argument. Each is common in cloud security tooling. Each is why those tools can't scale.
The diagnostic test
For any proposed security check or control:
Is this a statement about STATES or about BEHAVIORS?
States: "this configuration must not exist." Safety property. Compositional. Sound under local enforcement. Admissible to the catalog.
Behaviors: "this workflow must execute correctly." Correctness property. Not compositional. Requires global reasoning. NOT admissible to the catalog.
The test keeps the catalog pure-safety as it grows. Every control that passes the test composes with every other control by the theorem. Every control that fails the test would break the soundness argument.
The industry's compositionality gap
The cloud security industry has spent 15 years building correctness tools:
| Tool category | Property it checks | Compositional? |
|---|---|---|
| Per-service scanners | Local correctness of individual resources | No — misses compound risks |
| CSPM scans | Global correctness at a single moment | No — can't predict cross-account interactions |
| ML risk ranking | Behavioral aggregation with learned weights | No — heuristic, not sound |
| Workflow-aware analysis | Correct behavior across services | No — explodes combinatorially |
| Behavior-anomaly detection | Deviation from expected behavior | No — not a safety property |
Every row checks a property that doesn't compose. More tools checking non-compositional properties produces more local verdicts and the composition is still not sound. The industry can add tools indefinitely without closing the gap, because the gap is mathematical, not engineering.
The gap closes when the industry builds tools that check SAFETY properties (forbidden states, compositional by theorem) instead of CORRECTNESS properties (required behaviors, non-compositional by theorem).
The theorem is 40 years old. Distributed databases adopted it in the 2000s. Cloud security is still building correctness tools.
Four words
Correctness emerges. Safety composes.
Correctness is emergent. It depends on coordination, ordering, timing, interaction. You can't guarantee it from local checks.
Safety is compositional. It depends on which states are forbidden. You CAN guarantee it from local checks. The conjunction of local safety verdicts is a global safety verdict. By theorem.
Every compound chain, small kernel, growing catalog, multi-solver verification and every composing compliance profile in the architecture rests on these four words. The math carries the soundness. The engineering carries the catalog. The catalog can grow forever because the math doesn't break.
How this relates to existing compliance mods
The compositional-safety theorem applies to every deterministic check tool. Each control in turbot/steampipe-mod-aws-compliance is a local safety verdict (this bucket is or isn't public; this user does or doesn't have MFA), and the conjunction theorem guarantees the framework benchmark's overall verdict is sound in the same way Stave's per-control verdicts are. The compositional layer Stave adds isn't "safer math" — it's different content under the same theorem. Per-resource framework controls and cross-resource compound controls are both local safety verdicts; their conjunction is the global safety verdict. Running both gives the same soundness guarantee over a strictly larger covered surface. The practical form the article's theorem takes when applied to the tool ecosystem. Comparison: aws-compliance-mod.
Safety composition — 2,650 safety properties enforced locally, 585 compound chains as conjunctions, one 1,030-line kernel with no global reasoning, five solvers that agree because the question has one answer. It is implemented in Stave, an open-source Risk Reasoner. Correctness emerges. Safety composes. The math carries the architecture. Try it: bash examples/demo-ai-security/run.sh
Top comments (0)