Cordon

Attacks are getting cheaper

AI tools have cut the time and skill it takes to find an exposed service. The window between shipping a misconfiguration and someone exploiting it keeps shrinking. Pre-deploy checks need to keep up.

Amazon Threat Intelligence reportedly saw one low-skill actor use commercial AI tools to compromise 600+ FortiGate devices in 55 countries in about five weeks (Picus Security).
The Cloud Security Alliance ranks misconfiguration and inadequate change control as the #1 cloud threat (SecurityBrief).
The "meow" attacks wiped 25,000+ internet-exposed databases and services. No exploit was needed, the databases were just reachable (TechTarget).

Scanners only report the paths they try. A proof covers every path in the plan. Cordon keeps the question narrow (can A reach B?) so proofs run in seconds, on every pull request.

How it works

Name your boundaries in a short policy file. Cordon models every route, gateway, NACL and security group in the plan, searches for a path, and hands its answer to an independent checker. You get one of three results.

PROVENexit 0

No path exists. The checker verified the proof. Every assumption it relies on is listed in the report.

VIOLATEDexit 1

A path exists. See it hop by hop: route, gateway, NACL, security group rule. The checker verifies the path too.

UNKNOWNexit 2

Cordon couldn't decide, and tells you why: an unsupported resource, a value only known after apply, or an assumption you haven't accepted. UNKNOWN never passes silently.

Every answer is double-checked

The engine finds the answer. A separate checker, with no shared code and no solver, verifies it before you see it. If the engine makes a mistake, the checker rejects it and you get UNKNOWN, never a false PROVEN.

Tested three ways

Differential testing: a third, brute-force implementation must agree with the engine and the checker.
Mutation testing: deliberately corrupted certificates must be rejected.
Machine-checked proof: a Lean 4 proof of the checker's soundness is written and in review.
Secrets stay secret: sensitive plan values are never written to reports.

See it in action

Synthetic AWS architectures, planned with Terraform 1.15.5 and checked with the current build. Output is unedited; trimmed lines are marked with …

VIOLATED · PR CHECK

Catch a PR that opens SSH into cardholder data

A PCI-style VPC with web, app, cardholder data (cde) and corp subnets. Before the change, Cordon proves corp and cde are isolated. The PR adds one security group rule and one NACL rule. Cordon flags it with the full 12-hop path from the corp host to the cde instance on port 22.

The second property stays UNKNOWN at all@2. Its proof needs two scope assumptions, which you accept by name.

Requires: DNS support off in the VPC, web and app tiers marked trusted, a new deployment (no prior state).

pr.tf (added)

resource "aws_vpc_security_group_ingress_rule" "cde_ssh_from_corp" {
  security_group_id = aws_security_group.cde.id
  cidr_ipv4         = local.subnets.corp.cidr
  ip_protocol       = "tcp"
  from_port         = 22
  to_port           = 22
}

resource "aws_network_acl_rule" "cde_in_corp_ssh" {
  network_acl_id = aws_network_acl.cde.id
  rule_number    = 110
  egress         = false
  protocol       = "tcp"
  rule_action    = "allow"
  cidr_block     = local.subnets.corp.cidr
  from_port      = 22
  to_port        = 22
}

cordon.yaml

boundaries:
  cde:
    select: { tags: { zone: cde } }
  corp:
    select: { tags: { zone: corp } }
components:
  app:
    select: { tags: { zone: app } }
  web:
    select: { tags: { zone: web } }
properties:
  - isolated: { a: corp, b: cde }
  - no_path: { from: cde, to: internet }
trust:
  assume_uncompromised: [app, web]

before the PR · T1Sexit 0

# cordon verify — PROVEN

| 1 | ` isolated ` | ` cde `, ` corp ` | PROVEN | PROVEN | none |
| 2 | ` no_path ` | ` cde ` | PROVEN | PROVEN | none |

after the PR · all@2exit 1

# cordon verify — VIOLATED

| 1 | ` isolated ` | ` cde `, ` corp ` | VIOLATED | VIOLATED | none |
| 2 | ` no_path ` | ` cde ` | ` UNKNOWN (model: PROVEN; pending A-FLOWS-NEW-ONLY@1, A-NO-RUNTIME-NET-MUTATION@1) ` | PROVEN | UNACCEPTED\_ASSUMPTIONS |

**Attack path** (strength must, origin ` boundary `, service port ` tcp/22 `, 1 cells):

1. sends ` aws_instance.corp ` — rule ` R-EMIT-AI `, ENI ` eni0 `
2. security group allows egress ` aws_vpc_security_group_egress_rule.corp_any ` — rule ` R-SGOUT `
3. NACL allows outbound ` nacl:default(aws_vpc.pci):egress#100 ` — rule ` R-LOCAL `
4. routes via ` aws_route_table.private:local[0] ` — rule ` R-LOCAL `
5. NACL allows inbound ` aws_network_acl_rule.cde_in_corp_ssh ` — rule ` R-LOCAL `
6. security group allows ingress ` aws_vpc_security_group_ingress_rule.cde_ssh_from_corp ` — rule ` R-DELIV-INIT `
7. delivered to ` aws_instance.cde[0] ` — rule ` R-DELIV-INIT `, ENI ` eni0 `, address ` addr(eni:aws_instance.cde[0]#eni0) `
8. responds (tracked connection) ` aws_instance.cde[0] ` — rule ` R-RESP-B `, ENI ` eni0 `
9. NACL allows outbound ` aws_network_acl_rule.cde_out_corp ` — rule ` R-LOCAL `
10. routes via ` aws_route_table.private:local[0] ` — rule ` R-LOCAL `
11. NACL allows inbound ` nacl:default(aws_vpc.pci):ingress#100 ` — rule ` R-LOCAL `
12. delivered to ` aws_instance.corp ` — rule ` R-DELIV-RESP-EX `, ENI ` eni0 `, address ` addr(eni:aws_instance.corp#eni0) `

VIOLATED · INBOUND EXPOSURE

Find databases exposed to the internet

Three databases in a public subnet, open to 0.0.0.0/0: the mistake behind the mass database wipes. Outbound traffic is blocked, so the databases never start a connection. Cordon still finds the inbound path: through the internet gateway, to port 5432, and the response back out.

All three hosts share the security group, so the Elasticsearch host accepts 5432 too. That's the path shown. The rule index ingress[1] currently follows Cordon's sorted order, not the HCL order.

With only all@2 accepted, the answer is UNKNOWN and names the pending assumption: VPC Block Public Access is off. A plan can't show account-level settings, so Cordon asks you to confirm them instead of guessing.

main.tf

resource "aws_security_group" "db" {
  name        = "db-sg"
  description = "database access"
  vpc_id      = aws_vpc.main.id

  dynamic "ingress" {
    for_each = local.db_ports   # postgres 5432, elasticsearch 9200, mongodb 27017
    content {
      description = ingress.key
      protocol    = "tcp"
      from_port   = ingress.value
      to_port     = ingress.value
      cidr_blocks = ["0.0.0.0/0"]
    }
  }
  # No egress rules: the database never starts a connection.
  egress = []
}

cordon.yaml

boundaries:
  db:
    select: { tags: { role: database } }
properties:
  - no_path: { from: db, to: internet, ports: ["tcp/5432"] }

all@2exit 2

# cordon verify — UNKNOWN

| 1 | ` no_path ` | ` db ` | ` UNKNOWN (model: VIOLATED; pending A-VPC-BPA-OFF@1) ` | VIOLATED | UNACCEPTED\_ASSUMPTIONS |

all@2 + scope + A-VPC-BPA-OFF@1exit 1

# cordon verify — VIOLATED

| 1 | ` no_path ` | ` db ` | VIOLATED | VIOLATED | none |

**Attack path** (strength must, origin ` boundary `, service port ` tcp/5432 `, 512 cells):

1. enters via internet gateway ` aws_internet_gateway.igw ` — rule ` R-IGW-DNAT `
2. NACL allows inbound ` nacl:default(aws_vpc.main):ingress#100 ` — rule ` R-ENTER `
3. security group allows ingress ` aws_security_group.db:ingress[1] ` — rule ` R-DELIV-INIT `
4. delivered to ` aws_instance.db["elasticsearch"] ` — rule ` R-DELIV-INIT `, ENI ` eni0 `, address ` addr(eni:aws_instance.db["elasticsearch"]#eni0) `
5. responds (tracked connection) ` aws_instance.db["elasticsearch"] ` — rule ` R-RESP-B `, ENI ` eni0 `
6. NACL allows outbound ` nacl:default(aws_vpc.main):egress#100 ` — rule ` R-IGW-MAP `
7. routes via ` aws_route_table.public:route[0] ` — rule ` R-IGW-MAP `
8. leaves via internet gateway ` aws_internet_gateway.igw ` — rule ` R-IGW-MAP `

PROVEN · CHECKED SEPARATELY

Re-check any proof, any time

Save any PROVEN as a problem and certificate pair. Re-check it later with cordon check-cert against the hashes you recorded, without trusting the engine. The output lists every assumption the proof depends on. In this example that is 29 assumptions, and all of them are currently marked unvalidated.

check-cert · isolated(corp, cde), before the PRexit 0

check-cert: VALID PROVEN
problem SHA-256: 0b77239b66f308ddcd4aeabe0a69b45a555dd1f2607fd4e1ccf3994b9da342f5
certificate SHA-256: 05e8d629f2c06548dfcc7830366cdea52afbbff9e5753cd03d32b348ca64482b
dependency set: A-ARTIFACT-COMPLETE@1, A-FLOWS-NEW-ONLY@1, A-NO-RUNTIME-NET-MUTATION@1, A-PLAN-JSON-VISIBILITY@1, A-PROVIDER-ENFORCEMENT@1, A-PROVIDER-VERSION-REVIEWED@1, … (29 ids)

Where it stands today

We tested the current build on 13 typical AWS architectures, from a three-tier app to EKS, PCI segmentation and 1,280-resource composites, with policies written the way you would on a first try. Most real-world plans aren't decidable yet. Here are the numbers.

4 / 40

Properties decided on the plans as first written (README tier). All four were real violations on the public-database setup. None was proven.

PROVEN results we disagree with after checking each one by hand. Every PROVEN required DNS support off in the VPC.

1.4–9.3 s

Per run, for 7 to 1,280 resources. Plans of 320 resources and more ran out of proof budget and came back UNKNOWN.

Why most answers were UNKNOWN

Resource types not yet modeled, such as RDS, load balancers, Auto Scaling groups, EKS node groups and VPC endpoints. Today one IAM role or S3 bucket in the plan blocks every network property.
Common HCL idioms Cordon can't resolve yet: module outputs, dynamic blocks that reference security groups, map lookups and conditionals.
The VPC DNS resolver, which is on by default, is treated as an open channel. That keeps internal isolation from being proven.
Assumptions that have to be accepted by name before any PROVEN.

Coming next

Stop IAM and S3 resources from blocking network questions.
Make a VIOLATED always show a path that starts in the boundary you named. Today a public host elsewhere in the plan can be reported against an unrelated boundary.
Resolve module outputs and dynamic blocks, and model RDS, ALB/NLB, Auto Scaling groups, EKS node groups and VPC endpoints.
Make the realistic case decidable: a documented assumption profile, and reasoning about DNS that you opt into by name.

We re-run this study after every round of fixes and publish the results. Pilot teams get the full study: every plan, policy and report.

Works alongside your linter

Tool	When it runs	What it answers	Can it prove a path is absent?
Checkov, tfsec, Trivy	Before apply	Does any single resource break a known rule?	No. Each rule looks at one resource.
AWS Reachability Analyzer, Network Access Analyzer	After deploy	Is there a path in the live account?	For deployed resources, after the change is live
Cordon	Before apply, on every PR	Can traffic get from boundary A to boundary B, through everything in the plan?	Yes, with a checked certificate, or it says UNKNOWN

Keep your linter for fast, rule-by-rule checks. Add Cordon for the question a linter can't answer: after this plan is applied, can anything reach the database?

What it covers

The most damaging cloud breaches chain a reachable service to stolen credentials, as at Capital One. Cordon covers the network half today. Instance metadata and IAM support is next. Until then, those questions return UNKNOWN.

Incident pattern	Example	Cordon today	Next
Database or search cluster reachable from the internet	Mass wipes of exposed Elasticsearch and MongoDB	Decided for databases on EC2	RDS, load balancers, Auto Scaling groups
Segmentation: dev to prod, PCI scope, tenant isolation	Lateral movement after a foothold	Decided within one VPC, with DNS off	DNS resolver, peering, Transit Gateway, endpoints
Web flaw → metadata service → role credentials → S3	Capital One, 2019	UNKNOWN	IMDS + IAM model
Compromised pod → node credentials → cluster secrets	Default EKS node-credential exposure	UNKNOWN	IMDS + IAM + Kubernetes RBAC
Over-privileged IAM	The most common root cause in 2025 reports	UNKNOWN	`no_action`, `no_credential`
Stolen passwords, no MFA	Snowflake customers, 2024	Out of scope	—

Every PROVEN is relative to Cordon's model of AWS networking and the assumptions printed with it. Validation against live AWS accounts is planned; until then, every assumption is marked unvalidated. Changes made outside Terraform aren't visible in a plan, and the report says so.

Get started in three steps

Run Cordon locally or in CI. No credentials, no agents, no access to your AWS account.

Export your plan

shell

terraform plan -out=tfplan
terraform show -json tfplan > plan.json
terraform providers schema -json > schema.json

Name your boundaries

Use the tags you already have. Write each property from the side you want to protect; the internet attacker is built in.

boundaries:
  web:  {select: {tags: {tier: web}}}
  data: {select: {tags: {tier: data}}}
properties:
  - no_path: {from: data, to: internet}
  - no_path: {from: web, to: {boundary: data}, ports: ["tcp/22"]}

Gate every pull request

shell

cordon verify --plan plan.json --schema schema.json --policy cordon.yaml \
  --accept-unvalidated all@2 --format markdown

Fail the build on exit 1 (VIOLATED) or 3 (bad input). Route exit 2 (UNKNOWN) to a reviewer with its reasons. Use --accept-unvalidated to choose which modeling assumptions you accept; each one is printed with the verdict.

Let Claude Code write the policy

Ask "can anything in this plan reach the payments database?" The Cordon skill finds your boundaries, drafts a policy for your approval, runs the check, and proposes the smallest HCL fix for any path it finds. It never loosens your policy to get a PROVEN.

Your plan never leaves your machine

Cordon is a single binary. It never runs your HCL or provisioners, never calls AWS, and never needs credentials. Sensitive values stay out of reports, so output is safe to post on a pull request.

Join the pilot

Cordon is in pre-release. We're working with platform and security teams running AWS and EKS on Terraform or OpenTofu. Run it on your own plans, on your own machines, and help decide what we model next.

Sources: Tenable/CSA 2025 · SecurityBrief · ThreatDown 2026 · Picus Security · Wiz: Capital One · Datadog: EKS node credentials · Mandiant on Snowflake · Meow attacks

Ship Terraform changes without opening a path to your data.

Attacks are getting cheaper

How it works

Every answer is double-checked

Tested three ways

See it in action

Catch a PR that opens SSH into cardholder data

Find databases exposed to the internet

Re-check any proof, any time

Where it stands today

Why most answers were UNKNOWN

Coming next

Works alongside your linter

What it covers

Get started in three steps

Export your plan

Name your boundaries

Gate every pull request

Let Claude Code write the policy

Your plan never leaves your machine

Join the pilot