Discover Inconsistencies between Firewall Policies

Firewalls are core elements in network security, the effectiveness of firewall security is dependent on configuring firewall policy correctly. Firewall policy describes the access that will be permitted or denied from the trusted network. In corporate network, several firewalls are set up and administrated by different teams. The consistency between those firewall policies is crucial to corporate network security. In this paper, we present a method of discover the inconsistencies between two given firewall policies. Firstly, Firewall policies are represented with logic formulas, the consistency regarded as a property of firewall policies is represented with logic formulas. The inconsistencies are discovered from the semantics of the union of the logic formulas. Furthermore, we prove that the method has the unique answer which can be computed in polynomial time. Firewall policies often need to be updated, as networks evolve. Many firewall policy errors are caused by the side effects of policy updates. Our method can be used to verify the updates of firewall policy by comparing the policy before changes and the policy after changes.