602 CHAPTER 24 Formal Analysis of Policy-Based Security Configurations in Enterprise Networks specification language plays an important role in correctly and comprehensively modeling the security requirements as access policies in enter- prise networks. Zhang et al. [19] state the necessary features of a good security pol- icy specification language, which are stated as follows: ­ et al. [16] proposed algorithms for discovering policy anomalies in distributed firewalls. These algorithms can identify the anomalies through inter- and intra-firewall analysis and determine the proper rule placement in the firewalls. Al-Shaer and Hamed [17] worked on the Fire- wall Policy Advisor who can resolve the conflicts in firewall policy configurations. In this work, the authors formally defined all possible firewall rule relations and used these relations to classify fire- wall policy anomalies. Then, they modeled the firewall rule information and relations in a for- mal decision tree-based representation. Based on this model and formalization, the firewall policy advisor implements two management tools: ­ ­ ­ Policy Anomaly Detector for identifying con- flicting, shadowing, correlated, and redun- dant rules. When a rule anomaly is detected, users are prompted with proper corrective actions. Policy Editor for facilitating rules insertion, modification, and deletion. The policy editor automatically determines the proper order for any inserted or modified rule. It also gives a preview of the changed parts of the policy whenever a rule is removed to show the effect on the policy before and after the removal. ­ ­ Service oriented: The language should focus the user's attention on the security require- ments of network services rather than low- level traffic details as in the rule-oriented approach. Modular and reusable: The language objects are self-contained and can be reused and extended to scale to large networks. Rule order independent: The user should be able to define the security policies in any order without worrying about introducing conflicts. Conflict free: The compiled policies should not have conflicts in a single device (intrapolicy) or across multiple devices (interpolicy). However, the tool is not made interactive for query-based security analysis. In this line of work, Adiseshu et al. [18] proposed algorithms for detecting and resolving packet filtering con- flicts. Samak et al. [13] proposed another frame- work, namely, Firecracker for inferring firewall policies using probabilistic smart probing. How- ever, the notion of hidden access path analysis with a presence that may implicitly introduce security holes in the implementations has not yet been addressed. Researchers proposed different high-level net- work security policy specification languages, namely, HLFL [20], Firmato [11], FLIP [19], NSPSL [1, 21], etc. The high-level firewall lan- guage (HLFL) project is an approach to spec- ify high-level firewall policies and translate them into useful rules for IPChains, Netfilter, and oth- ers. The approach does an automatic transla- tion, but it lacks important feature of detecting and preventing conflicts in the firewall rules. FLIP [19] is a recently proposed high-level conflict-free firewall policy language for enforc- ing access control-based security and ensuring seamless configuration management. In FLIP, security policies are defined as high-level service- oriented goals, which can be translated automat- ically into access control rules to be distributed to appropriate enforcement devices. The key fea- tures of FLIP are stated as follows: ­ 24.2.2. Security Policy Specification Languages The security requirements of an enterprise net- work can be expressed in a natural way as high-level access policies. The security policy ­ FLIP decouples the policy from network topology and hides the configuration details related to different vendors and devices. FLIP allows the definition of policy groups, which is a collection of rules related to a set