Date Added: Jun 2009
A firewall is a key security component in computer networks. It filters network traffic based on an ordered list of filtering rules. Firewall configurations must be correct and complete with respect to security policies. A security policy is a set of predicates, which is a high level description of traffic controls. This paper proposes an automatic method to verify the correctness of firewall configurations with respect to security policies. The paper defines Boolean formulae to represent security policy and firewall configuration and then one verifies their equivalence using the SAT solver. If the configuration is incorrect, the method produces a counterexample to help the user to correct his firewall configuration. The paper implemented this new technique and the first results were very promising.