An Algebra for Two-Layer Cloud Filtering: Detecting Redundancy, Shadowing, and Dominance Anomalies Across Stateless Network ACLs and Stateful Security Groups

Traffic inside a cloud Virtual Private Cloud (VPC) is filtered by two layers with fundamentally different semantics: a stateless, ordered, first-match Network ACL (NACL) and a stateful, unordered, allow-only Security Group (SG). Existing analyzers decide point-to-point reachability using satisfiability solvers, Datalog engines, or binary decision diagrams, but do not identify, at the rule level, which rules are dead, redundant, or dominated, nor explain why. We provide a closed-form set algebra over the two layers. Representing each rule field by its boundaries makes a rule a hyper-rectangle and a layer a union of boxes; the effective admitted region Φ = A(N) ∩ A(G) is then a finite union of disjoint boxes computable from rule endpoints alone. We define a taxonomy of single- and cross-layer anomalies—shadowed NACL rules, dead SG rules, Φ-redundant rules, Φ-ineffective NACL allows, and layer disagreement—characterize each by a decidable region predicate, and prove an exact iff-condition for SG Φ-redundancy. A boundary-only detection algorithm is sound and complete for the exactly decidable anomaly classes, running in O((k + t)^d) time for fixed dimension d, and the disjoint box decomposition of Φ gives a minimal anomaly-free form that is unique up to merging adjacent coplanar boxes. A single-file implementation matches brute force on millions of packets, staying orders of magnitude below the worst-case bound; the parametric model extends unchanged to IPv6 and ICMP.