KLOU Firewall Checker

Formal verification of AWS Security Group reachability using the Z3 SMT Solver.

SAT = traffic CAN reach target (proved reachable)
UNSAT = traffic CANNOT reach target (proved blocked)

---

What this does

Unlike heuristic checks, this formally proves whether a traffic flow is allowed or blocked — not just "no deny rule found". Z3 exhaustively checks all possible states against the constraint model.

Given a set of AWS Security Group rules and a traffic flow (source IP, port, protocol), the engine:

1. Encodes the flow as Z3 integer variables
2. Encodes each SG rule as a Z3 constraint
3. Runs the SMT solver to determine satisfiability
4. Returns SAT (reachable) or UNSAT (blocked), plus which rule allows/blocks it

---

Quick example

from firewall_checker import check_sg_reachability

result = check_sg_reachability(
    src_ip="203.0.113.5",
    dst_port=443,
    protocol="tcp",
    sg_rules=[{
        "rule_id": "sgr-001",
        "direction": "inbound",
        "action": "allow",
        "protocol": "tcp",
        "from_port": 443,
        "to_port": 443,
        "cidr": "0.0.0.0/0"
    }]
)

print(result["z3_result"])      # → "SATISFIABLE (Traffic allowed)"
print(result["allowing_rule"])  # → "sgr-001"

External IP blocked by VPC-only rule:

result = check_sg_reachability(
    src_ip="203.0.113.5",   # external — NOT in 10.0.0.0/8
    dst_port=8080,
    protocol="tcp",
    sg_rules=[{
        "rule_id": "sgr-vpc",
        "direction": "inbound",
        "action": "allow",
        "protocol": "tcp",
        "from_port": 8080,
        "to_port": 8080,
        "cidr": "10.0.0.0/8"   # VPC only
    }]
)

print(result["z3_result"])  # → "UNSATISFIABLE (No matching allow rule)"
print(result["reachable"])  # → False

---

Installation

pip install z3-solver==4.13.0

No other dependencies.

---

Run the tests

python -m pytest test_firewall_checker.py -v

Expected output:

PASSED test_public_https_is_reachable
PASSED test_port_80_blocked_when_only_443_allowed
PASSED test_external_ip_blocked_by_vpc_only_rule
PASSED test_internal_ip_allowed_by_vpc_rule
PASSED test_no_rules_means_implicit_deny
PASSED test_constraints_evaluated_count

6 passed in 0.62s

---

API Reference

check_sg_reachability(src_ip, dst_port, protocol, sg_rules) → dict

High-level convenience function.

Parameter	Type	Description
src_ip	str	Source IPv4 address (e.g. "203.0.113.5")
dst_port	int	Destination port (e.g. 443)
protocol	str	"tcp", "udp", "icmp", or "all"
sg_rules	list[dict]	List of SG rule dicts (see format below)

Rule dict format:

{
    "rule_id":   "sgr-001",    # unique identifier
    "direction": "inbound",    # "inbound" | "outbound"
    "action":    "allow",      # "allow" | "deny"
    "protocol":  "tcp",        # "tcp" | "udp" | "icmp" | "all"
    "from_port": 443,          # start of port range (-1 = all)
    "to_port":   443,          # end of port range (-1 = all)
    "cidr":      "0.0.0.0/0", # source CIDR
    "priority":  100           # lower = higher priority
}

Returns:

{
    "reachable":              bool,
    "z3_result":              str,   # "SATISFIABLE ..." | "UNSATISFIABLE ..."
    "proof":                  str,   # Z3 model or proof description
    "allowing_rule":          str | None,
    "blocking_rule":          str | None,
    "constraints_evaluated":  int
}

KLOUFirewallChecker (class)

Lower-level interface for advanced use:

from firewall_checker import KLOUFirewallChecker, SGRule, TrafficFlow, Protocol

checker = KLOUFirewallChecker()

flow = TrafficFlow(
    src_ip="10.0.1.42",
    dst_ip="10.0.2.1",
    dst_port=5432,
    protocol=Protocol.TCP,
    direction="inbound"
)

rules = [SGRule(
    rule_id="sgr-db",
    direction="inbound",
    action="allow",
    protocol=Protocol.TCP,
    from_port=5432,
    to_port=5432,
    cidr="10.0.0.0/8"
)]

result = checker.check_reachability(flow, rules)
print(result.z3_result)  # SATISFIABLE

# Also check for shadowed rules
shadows = checker.check_rule_shadowing(rules)

---

How it works

TrafficFlow                    SGRule[]
  src_ip = 203.0.113.5          sgr-001: allow tcp :443 from 0.0.0.0/0
  dst_port = 443          →
  protocol = TCP                      ↓
                              Z3 Solver
                         src_ip == 3405803525
                         dst_port == 443
                         protocol == 6
                         AND(port >= 443, port <= 443)
                                      ↓
                              check() → sat
                                      ↓
                         SATISFIABLE (Traffic allowed)
                         allowing_rule = "sgr-001"

The solver proves in < 1ms that the constraints are satisfiable (or not), providing a formal guarantee rather than a best-effort heuristic.

---

Related work

• Z3Prover/FirewallChecker by Andrew Helwer — the original Z3 firewall checker (generic firewalls)
• KLOU — full cloud governance platform with Z3-based formal verification applied to AWS, Azure, and GCP

---

Requirements

z3-solver==4.13.0

License

MIT — see LICENSE