Model Checking Firewall Policy Configurations

The use of firewalls to enforce access control policies can result in extremely complex networks. Each individual firewall may have hundreds or thousands of rules, and when combined in a network, they may result in unexpected combined behavior. To mitigate this problem, there has been interest in the use of model checking techniques for analyzing the behavior of firewall policy configurations, and reporting anomalies. Existing techniques for firewall policy analysis are based on decision diagrams, most normally reduced ordered binary decision diagrams (BDDs). BDDs are a rich data structure, supporting more logical operations than just solving Boolean formulae. Typically, search algorithms for Boolean satisfiability (so-called SAT-solvers) outperform BDDs. In this paper, we show that the extra structure provided by BDDs is not necessary for firewall policy analysis, and that SAT solvers are sufficient. This argument is supported both by theoretical analysis and by experimental data.