Semantics-preserving simplification of real-world firewall rule sets

The security provided by a firewall for a computer network almost completely depends on the rules it enforces. For over a decade, it has been a well-known and unsolved problem that the quality of many firewall rule sets is insufficient. Therefore, there are many tools to analyze them. However, we found that none of the available tools could handle typical, real-world iptables rulesets. This is due to the complex chain model used by iptables, but also to the vast amount of possible match conditions that occur in real-world firewalls, many of which are not understood by academic and open source tools. In this paper, we provide algorithms to transform firewall rulesets. We reduce the execution model to a simple list model and use ternary logic to abstract over all unknownmatch conditions.These transformations enable existingtools tounderstandreal-worldfirewall rules,whichwe demonstrate on four decently-sized rulesets. Using the Isabelle theorem prover, we formally showthat all our algorithms preserve the firewall’s filtering behavior.