KLOUCEO/klou-firewall-checker

# KLOU Firewall Checker **SAT** = 流量**可以**到达目标（已证明可达） **UNSAT** = 流量**无法**到达目标（已证明阻断） ## 功能说明 与启发式检查不同，这会**形式化证明**流量是被允许还是被阻断——而不仅仅是“未找到拒绝规则”。Z3 会根据约束模型详尽检查所有可能的状态。 给定一组 AWS Security Group 规则和一个流量（源 IP、端口、协议），引擎会： 1. 将流量编码为 Z3 整数变量 2. 将每条 SG 规则编码为 Z3 约束 3. 运行 SMT 求解器以判定可满足性 4. 返回 **SAT**（可达）或 **UNSAT**（阻断），以及允许/阻断它的具体规则 ## 快速示例 ``` 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" ``` 外部 IP 被仅限 VPC 的规则阻断： ``` 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 ``` ## 安装说明 ``` pip install z3-solver==4.13.0 ``` 无其他依赖。 ## 运行测试 ``` python -m pytest test_firewall_checker.py -v ``` 预期输出： ``` 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 参考 ### `check_sg_reachability(src_ip, dst_port, protocol, sg_rules) → dict` 高级便捷函数。 | 参数 | 类型 | 描述 | |-----------|------|-------------| | `src_ip` | `str` | 源 IPv4 地址（例如 `"203.0.113.5"`） | | `dst_port` | `int` | 目标端口（例如 `443`） | | `protocol` | `str` | `"tcp"`、`"udp"`、`"icmp"` 或 `"all"` | | `sg_rules` | `list[dict]` | SG 规则字典列表（格式见下文） | **规则字典格式：** ``` { "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 } ``` **返回值：** ``` { "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` (类) 用于高级用法的底层接口： ``` 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 # 还要检查 shadowed rules shadows = checker.check_rule_shadowing(rules) ``` ## 工作原理 ``` 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" ``` 求解器在 **< 1ms** 内证明约束是否可满足，从而提供**形式化保证**，而非尽力而为的启发式判断。 ## 相关工作 - [Z3Prover/FirewallChecker](https://github.com/Z3Prover/FirewallChecker)，作者 Andrew Helwer —— 原始的 Z3 防火墙检查器（通用防火墙） - [KLOU](https://klou.com.br) —— 完整的云治理平台，将基于 Z3 的形式化验证应用于 AWS、Azure 和 GCP ## 环境要求 ``` z3-solver==4.13.0 ``` ## 许可证 MIT —— 详见 [LICENSE](LICENSE)

标签：AWS, DPI, Python, Z3求解器, 安全, 安全规则引擎, 形式化验证, 无后门, 超时处理, 逆向工具, 防火墙规则