Analyzing and resolving anomalies in firewall security policies based on propositional logic

Firewalls are essential components in network security solutions. In order to implement correct security policy, the anomalies in firewall rules should be analyzed carefully, especially in enterprise network. In this paper, we present a new formal framework for analysis and resolution of anomalies in firewall rules. First of all, a formal model based on propositional logic is presented to specify rules. Then we specify all anomalies that identified in the latest researches based on our model. Current studies for analysis of anomalies are based on one to one rule anomalies, but we identify total version of anomalies based on one to many relationship of rules. Furthermore we have designed and implemented a tool based on theorem proving for verification of the specified anomalies. In addition, we present two algorithms for resolving anomalies in a rule database based on our formal model. These algorithms minimize the number of rules without changing the policy. Experimental results indicate that our algorithms for discovery single and total anomalies run in 2-3 seconds for a very large firewall with thousands of rules.