Here's the gap every configuration analysis tool hits: the configuration tells you what exists. It doesn't tell you what was intended.
An S3 bucket is public. Is that a mistake? Or is it a static website origin? A database has no encryption at rest. Is that a compliance violation? Or is it a dev sandbox with synthetic data? An IAM role has s3:* on *. Is that dangerous? Or is it a break-glass emergency role that's supposed to have broad access?
The configuration is the same in each case. The intent is different. Intent doesn't live in the configuration, it lives in someone's head.
Until you put it in a tag.
The tag as a state variable
When a human applies a tag to a cloud resource — Sensitivity: High, DataClassification: PII, Environment: Production, Owner: team-payments — they're doing something that looks routine but is profound. They're converting subjective human intent into a machine-readable state variable.
Before the tag, "this bucket holds sensitive customer data" is a sentence in a design document that nobody reads after week two. After the tag, Sensitivity: High is a property of the resource that automated tools can query, evaluate, and enforce on every change, forever.
In Lamport's framework, the state of a system is the collection of all its variables at a point in time. A configuration snapshot captures the state of every cloud resource: its properties, its relationships, its permissions. When you add a tag, you add a variable to the state vector. The resource's state goes from:
Bucket_1 = { is_public: true, encryption: none, region: us-east-1 }
to:
Bucket_1 = { is_public: true, encryption: none, region: us-east-1,
tag_sensitivity: "High", tag_environment: "Production" }
That single addition — tag_sensitivity: "High" — transforms the resource from "a bucket with some configuration" into "a bucket with declared intent." The intent is now data. And data can be part of an invariant.
Writing the invariant
A Lamport safety invariant says: "this property must hold in every reachable state." With tags as state variables, the invariant can reference intent directly:
For every bucket b:
if b.tag_sensitivity = "High" then b.is_public = false
In CEL (the predicate language that evaluates against configuration snapshots):
asset.type == "aws_s3_bucket" &&
asset.tags.exists(t, t.key == "Sensitivity" && t.value == "High") &&
asset.public_access_block.block_public_acls == false
This predicate fires when a bucket tagged as high-sensitivity has public access. The invariant doesn't need to know why the bucket is sensitive — whether it holds PII, PHI, financial records, or trade secrets. The tag encodes the intent. The invariant enforces the boundary. The "why" lives in the tag. The "what must be true" lives in the invariant.
The power of this separation: the invariant is universal. "No high-sensitivity resource may be publicly accessible" applies to every resource type — S3 buckets, RDS databases, Elasticsearch domains, EBS volumes. One invariant, one tag convention, universal coverage. The developer who tags a resource Sensitivity: High gets the protection of every invariant that references that tag, without knowing what those invariants check.
The invariant your team already has but hasn't written down
Most cloud teams already have implicit invariants about tagged resources. They just haven't formalized them.
Ask any security engineer: "Should a bucket tagged DataClassification: PII be publicly accessible?" The answer is always no. That "always no" is a safety invariant. It's just stored in the security engineer's head instead of in a predicate file.
Ask any operations lead: "Should a database tagged Environment: Production have deletion protection disabled?" Always no. Another invariant, stored implicitly.
Ask any compliance officer: "Should any resource tagged Framework: HIPAA lack encryption at rest?" Always no. Another invariant.
Each of these can be written as a CEL predicate in under five lines. It can be evaluated against every configuration snapshot automatically. It can run in CI and block changes that violate the invariant before they reach production.
The work is writing down the rules everyone already knows and making them machine-enforceable. The tag is the bridge. The predicate is the enforcement. The CI gate is the guarantee.
The compound risk nobody talks about: intent tampering
Here's where it gets interesting — and where most tagging strategies stop short.
If tags encode intent, and invariants enforce boundaries based on tags, then changing or deleting a tag bypasses the invariant.
An attacker (or a misconfigured automation script, or a well-meaning developer who doesn't understand the tagging convention) removes the Sensitivity: High tag from a production bucket. The invariant that says "high-sensitivity resources must not be public" no longer fires — because the resource is no longer tagged as high-sensitivity. The bucket is now public AND unprotected by the invariant. The safety envelope has a hole.
This is a compound risk — not a single-resource misconfiguration but a composition of two changes that together bypass the safety boundary. The first change (remove the tag) looks benign. The second change (make the bucket public) violates the invariant that would have caught it, if the tag still existed.
This is the class of risk that per-resource scanners can't detect. They check: "is this bucket public?" (yes/no). They don't check: "was this bucket's sensitivity tag recently removed, and is that removal what enabled the public access change to pass the safety gate?"
The meta-invariant: protecting the tags themselves
The solution is a second-level invariant — an invariant that protects the integrity of the tagging system itself:
For every action a:
if a.target = "ModifyTag" and a.tag_key in {"Sensitivity", "DataClassification", "Environment"}
then a.actor must be in SecurityDataOwners group
In CEL, applied to IAM policy analysis:
asset.type == "aws_iam_policy" &&
asset.permissions.actions.exists(a,
a.startsWith("s3:PutBucketTagging") ||
a.startsWith("s3:DeleteBucketTagging")) &&
!asset.principal_groups.exists(g, g == "SecurityDataOwners")
This invariant says: only members of the SecurityDataOwners group can modify or delete security-relevant tags. Anyone else with PutBucketTagging or DeleteBucketTagging permissions on a sensitive bucket is a risk — even if they have no other dangerous permissions.
Two layers of invariants, composing:
Layer 1 (resource invariant): No resource tagged Sensitivity: High may be publicly accessible.
Layer 2 (meta-invariant): Only authorized principals may modify the tags that Layer 1 depends on.
Layer 1 enforces the safety boundary. Layer 2 protects the integrity of Layer 1's inputs. Without Layer 2, Layer 1 can be bypassed by modifying the tags. With both layers, the safety envelope is closed — you can't violate the boundary (Layer 1 catches it) and you can't remove the boundary's preconditions (Layer 2 catches it).
This is the compound risk detection that Lamport's framework makes natural: the invariant ranges over the composition of tag state and permission state, not over either one individually. A per-resource check can't express "the combination of tag-modification permission and the absence of SecurityDataOwners membership is dangerous." A compound invariant can.
ABAC: the industry already knows this pattern
The strategy of using tags to express intent and enforce boundaries has an industry name: Attribute-Based Access Control (ABAC). AWS, Azure, and GCP all support it natively.
AWS Service Control Policies can enforce: "Deny s3:PutBucketPolicy if the resource has tag Sensitivity: High." Azure Policies can enforce: "Deny public network access on any resource tagged Environment: Production." Open Policy Agent (OPA) can evaluate arbitrary tag-based rules against any structured data.
These are all implementations of Lamport-style invariants over tagged state. The tooling exists. The cloud providers support it. The missing piece in most organizations isn't the technology — it's the discipline of:
- Choosing a tagging convention that encodes intent (not just cost allocation)
- Writing the invariants that reference the tags
- Writing the meta-invariants that protect the tags
- Running both layers in CI, on every change, before production
Most organizations have tagging policies. Few have tag-referenced invariants. Fewer still have meta-invariants protecting tag integrity. The gap between "we have tags" and "our tags are safety invariants" is the gap between documentation and enforcement.
The architecture journey in five steps
This article — and the broader Lamport-to-cloud-security framing — follows a five-step progression:
Step 1: Accept that you cannot map the infinite cloud state space. Your cloud has more possible configurations than atoms in the observable universe. Enumerating safe states is intractable. You specify unsafe states instead — the patterns and properties that must never hold.
Step 2: Adopt the safety envelope. Define a boundary of allowed states, exactly as aviation defines the flight envelope. States inside the envelope are safe. States outside are blocked. The envelope is a set of invariants, evaluated mechanically.
Step 3: Limit scope to configurations and compound risks. Stave doesn't detect runtime exploits. It detects configuration states that violate safety invariants — including compound states where the composition of multiple resources creates a risk no individual resource exhibits.
Step 4: Recognize that human intent cannot be computed — so encode it. Resource tags turn subjective intent into objective state variables. The tag is the bridge between what a human knows ("this bucket holds PII") and what the invariant checks (tag_sensitivity == "High" → is_public == false).
Step 5: Write invariants over the tagged state, and protect the tags with meta-invariants. The invariant enforces the boundary. The meta-invariant ensures the boundary can't be silently dismantled by tag modification. Two layers, composing, covering both the safety property and the integrity of its inputs.
Each step builds on the previous. Skip Step 4 and your invariants can't reference intent. They're limited to structural properties ("is this bucket public?") without knowing whether public access is intended or accidental. Skip Step 5's meta-invariants and your safety envelope has a hole — any principal who can modify tags can bypass the boundary.
The tag is the theory
The cognitive debt series argued that the theory of the system must be externalized. It must be moved from human heads into machine-readable artifacts. Resource tags are one of the simplest forms of externalized theory. When a developer tags a bucket Sensitivity: High, they're externalizing a piece of their understanding: "this resource matters, and here's how much."
That understanding was previously implicit — stored in the developer's head, in a design document, in a Slack message, in tribal knowledge that evaporates with team turnover. The tag makes it explicit, durable, machine-queryable, and — with invariants — machine-enforceable.
The progression from implicit to explicit is the same progression the Parnas article described for interfaces, the same progression the TRIZ analysis described for system theory, and the same progression the nuclear industry made when it moved from operator mental models to written operating envelopes. Each domain found the same resolution: the theory is too important to store in memory. Store it in an artifact. Then enforce the artifact mechanically.
The tag is the smallest possible artifact of externalized intent. The invariant is the smallest possible artifact of externalized enforcement. Together they close the loop between what a human knows and what a machine verifies — without requiring the machine to understand intent, and without requiring the human to understand implementation.
This article is part of a series connecting Lamport's safety invariant framework to practical cloud security. Related: "The Missing Primitive in Cloud Security Was Discovered in 1977", "Four Security Problems That Don't Need a Scanner", and "A 1972 Paper Predicted the AI Coding Crisis" (Parnas and cognitive debt).
Top comments (0)