Specification, Analysis and Resolution of Anomalies in Firewall Security Policies

摘要: Firewalls are essential components in network security solutions. Managers have to specify their organizational security policies using low level and order-dependent rules in firewalls. Furthermore, dependency of firewalls to the network topology, frequent changes in network topology and lack of an automatic method for analysis and verification of anomalies in specified security policy lead to inconsistencies and security holes. In this paper we present a formal language for specification of security policy in firewalls. Based on the language, the specified security policy, simple anomalies and total anomalies are translated to propositional logic formulas. Furthermore we have designed and implemented a tool based on theorem proving for detection of the anomalies in the specified policy. In addition, based on the formal model, two algorithms are presented for resolving anomalies in the policy. These algorithms minimize the number of rules without changing the security policy.