Automated, Formally Proven Conversion of Listed-Rule Firewalls to Tree-Rule Firewalls

Listed-Rule Firewalls (LRF) evaluate rules by first match: matching cost grows linearly with policy size, and ordered lists accumulate shadowing and redundancy anomalies. Tree-Rule Firewalls (TRF) match in a fixed number of levels, but their trees were built by hand; no procedure was known that turns an existing LRF policy into an equivalent tree. This paper presents an automated conversion whose correctness is proven end-to-end within a stated four-attribute IPv4 packet model. A four-dimensional range decomposition and a projection-normalization algorithm construct, from any LRF policy, a tree returning the same action for every packet; a deterministic O(n2) classifier first removes shadowed and redundant rules. A tree is fixed by a permutation of the four packet attributes; the framework admits the twelve permutations placing protocol before destination port. The tree’s decisions are invariant across these twelve orderings while its size is not: protocol-elsewhere orderings need 1.93× as many nodes as protocol-first orderings at 50 rules, matching time reaches statistical equivalence by 200 rules, and on a second policy sample the structural gap closes by 400 rules; the advantage is thus distribution-dependent. Across 73 million packet comparisons, no discrepancy from the original policy was observed; tree depth stayed at four on eight ClassBench-ng rulesets. All evaluated policies are synthetic or industry-calibrated synthetic and contain at most 400 rules.