✓ Human-authored analysis; AI used for formatting and proofreading.
Every organization with a bastion host makes the same claim: "All SSH connections to production go through the bastion." Nobody proves it.
The bastion exists. It has a hardened security group. It logs sessions. The architecture diagram shows SSH flowing through it. The compliance report says bastion-mediated access is enforced.
But has anyone verified that production instances ONLY accept SSH from the bastion's security group? That no VPC peering connection creates a lateral path? That no security group rule with a broad internal CIDR (10.0.0.0/8) on port 22 silently bypasses the entire bastion architecture?
The answer is usually no. The claim is an architectural assumption, not a verified property. The difference between those two things is the difference between "we have a bastion" and "all SSH routes through it."
The verification gap
Standard security scanners check security group rules one at a time. They catch SSH open to 0.0.0.0/0 — port 22 from the internet. Every benchmark has this check. Every tool catches it.
They don't catch SSH from 10.0.0.0/8. That's an internal CIDR. It's not "open to the internet." It passes every existing check. But it allows any instance in the VPC and in any peered VPC whose CIDR falls within 10.0.0.0/8 to SSH directly to production, bypassing the bastion entirely.
The difference: checking a security group rule is a property of one resource. Proving that all SSH routes through the bastion is a property of the entire network graph including every security group, route table, peering connection, Transit Gateway route and VPC endpoint. No single-resource check can answer the graph-level question.
Formal proof
Instead of checking each security group rule and hoping you covered them all, you ask a different question: "Does any SSH path exist from any non-bastion source to any production host that doesn't traverse a bastion?"
That question has a definitive answer. Either such a path exists or it doesn't. If it exists, the proof engine produces the specific path including the exact source, destination, security group rule, and network route that creates the bypass. If it doesn't exist, you have a mathematical proof that the bastion routing property holds for the entire network configuration.
Not a scan result or a best-effort check. A proof.
When no bypass exists
═══════════════════════════════════════════
Bastion SSH Routing Proof
═══════════════════════════════════════════
Scope: 14 production hosts across 3 VPCs
Bastion: 2 bastion hosts (bastion-east, bastion-west)
Entry points enumerated: 47
SSH paths to production: 23
PROOF: All SSH paths to production traverse a bastion host.
Verified in 0.31s. No bypass path exists.
Twenty-three SSH paths exist to production. Every one goes through a bastion. The tool didn't check 23 paths individually. It proved the property holds for ALL paths, including any path the enumeration might have missed. The proof is over the network configuration, not over a list of paths.
When a bypass exists
═══════════════════════════════════════════
Bastion SSH Routing Proof — BYPASS FOUND
═══════════════════════════════════════════
Scope: 14 production hosts across 3 VPCs
Bastion: 2 bastion hosts (bastion-east, bastion-west)
COUNTEREXAMPLE:
Source: 10.1.5.47 (dev-workstation, vpc-dev)
Destination: 10.0.2.12 (prod-db-primary, vpc-prod)
Port: 22
Path: dev-workstation → [vpc-peering pcx-abc] → prod-db-primary
Bypass: VPC peering pcx-abc connects vpc-dev to vpc-prod.
Security group sg-prod-db allows SSH from 10.1.0.0/16.
No bastion in the path.
REMEDIATION:
Replace SSH ingress 10.1.0.0/16 on sg-prod-db with sg-bastion-east.
The tool didn't scan every security group looking for SSH rules. It found a specific path through a VPC peering connection that no individual SG check would catch. Because the SG rule (10.1.0.0/16 on port 22) isn't "SSH from the internet." It's SSH from an internal CIDR that happens to include the dev VPC on the other side of a peering connection.
The counterexample names the exact source, destination, path, security group rule, and the VPC peering connection that enables the bypass. The remediation is in the counterexample: replace the CIDR rule with a security group reference to the bastion's SG.
Catching the bypass
Pattern 1: Broad internal CIDR
The most common bypass. A production security group allows SSH from 10.0.0.0/8 or the VPC's CIDR range. Intended to allow "internal access." It allows any instance in the network including compromised instances, developer laptops connected via VPN, and instances in peered VPCs.
Every standard scanner passes this rule because it's not 0.0.0.0/0. The proof fails because a path exists from a non-bastion source to production.
Pattern 2: VPC peering or Transit Gateway
Two VPCs are peered such as prod and dev. The peering was created for an application integration. Nobody checked whether SSH is blocked across the peering connection. A dev workstation can SSH to a production database through the peering connection.
No individual security group check catches this because each SG is correct within its VPC. The bypass is in the network topology. The peering connection creates a route that the SGs don't deny.
Pattern 3: CIDR instead of SG reference
Legitimate bastion architectures use security group references: "allow SSH from sg-bastion." This binds the rule to the bastion's identity, not its IP. When someone replaces the SG reference with the bastion's subnet CIDR (10.0.1.0/24), the rule works. But now any instance in that subnet can SSH to production, not just the bastion. A new instance launched in the bastion subnet bypasses the bastion even though it's in the "bastion subnet."
The proof catches this because the CIDR-based rule creates a path from non-bastion sources (any instance in the CIDR) to production. The SG-reference rule wouldn't, because only traffic from the bastion's SG matches.
Why this matters beyond SSH
The bastion routing proof is one instance of a general pattern: proving that a security property holds over the entire network configuration, not just checking individual rules.
The same approach verifies:
Does any path exist from the internet to a database? Not "is the database's security group open to the internet" (which every scanner checks) but "is there ANY sequence of hops through a load balancer, an application server, a peering connection, a Transit Gateway that creates a network path from a public endpoint to the database's port?"
Does any path exist from a sandbox to production? Same question as the bastion proof, applied to the isolation intent discussed in a previous article. A sandbox VPC tagged as isolated should have no network path to production VPCs. The proof verifies this over the entire topology, including indirect paths through Transit Gateway or peering.
Does any egress path exist from a restricted VPC? A VPC with no internet gateway might still have egress through a peered VPC's NAT gateway, a Transit Gateway route to an internet-facing VPC, or a PrivateLink connection to a cross-account service. The proof finds any egress path that exists, including indirect ones.
Each of these is a graph-level property that no individual resource check can answer. The proof operates over the entire network configuration simultaneously. When it says UNSAT (no path exists), that's a guarantee about the graph, not a summary of individual checks.
The compliance value
Compliance frameworks require "bastion-mediated access" or "controlled administrative access" or "privileged access management." Auditors check the architecture diagram and the bastion's configuration. They don't verify that the rest of the fleet enforces bastion-only access.
The proof output is compliance evidence:
PROOF: All SSH paths to production traverse a bastion host.
Scope: 14 production hosts, 3 VPCs, 47 entry points.
Verified: 2026-07-30T14:00:00Z
Duration: 0.31s
Result: UNSAT (no bypass exists)
This is a stronger compliance artifact than a scan report. A scan report says "we checked 47 security group rules and all look fine." The proof says "we verified that no SSH path to production exists that doesn't traverse a bastion including paths through peering connections, Transit Gateway routes, and any security group rule, not just the ones we thought to check."
When the auditor asks "how do you know all SSH goes through the bastion?" the answer is a formal proof, not a checklist.
Continuous verification
The proof runs on every snapshot. Configuration drifts. A VPC peering connection added for a migration. A security group rule widened for debugging. A Transit Gateway route propagated during a merge. Each creates a potential bypass. Each is caught the next time the proof runs.
The first run establishes the baseline: UNSAT, bastion routing holds. Every subsequent run either confirms it still holds (UNSAT) or produces the specific change that broke it (SAT with counterexample). The operator doesn't monitor security group changes and try to reason about whether each change affects bastion routing. The proof does that reasoning for them over the entire graph, every time.
If a developer adds 10.1.0.0/16 to a production security group on port 22, the next proof run produces: "BYPASS FOUND: dev-workstation can reach prod-db-primary via this new rule." The developer didn't think they were breaking bastion routing. They were adding "internal access." The proof knows that "internal access" on port 22 is a bastion bypass.
Network entry point enumeration and bastion routing proof are implemented in Stave. The proof uses satisfiability checking over the network configuration graph, the same technique used by Azure's network verification (Jayaraman et al., NSDI 2015) and BGP configuration verification (Beckett et al., SIGCOMM 2017), applied to cloud security group and VPC topology. Apache 2.0.
Top comments (0)