Abstract
In enterprise networks, the management of security policies and their configurations becoming increasingly difficult due to complex security constraints of the organizations. In such networks, the overall organizational security policy (global policy) is defined as a collection of rules for providing service accesses between various network zones. Often, the specification of the global policy is incomplete; where all possible service access paths may not be covered explicitly by the “permit” and “deny” rules. This policy is implemented in a distributed manner through appropriate sets of access control rules (ACL rules) in the network interfaces. However, the implementation must be complete i.e., all service access paths across the network must be implemented as “permit” and “deny” ACL rules. In that case, the unspecified access paths in a given policy must be implemented as either “permit” or “deny” rules; hence there may exist multiple ACL implementations corresponding to that policy. Formally verifying that the ACL rules distributed across the network interfaces guarantees proper enforcement of the global security policy is an important requirement and a major technical challenge. The complexity of the problem is compounded by the fact that some combination of network services may lead to inconsistent hidden access paths in the network. The ACL implementations ignoring these hidden access paths may result in violation of one or more policy rules implicitly. This paper presents a formal verification framework for analyzing security policy implementations in enterprise networks. It stems from boolean modeling of the network topology, network services and security policy where the unspecified access paths are modeled as “don’t-care” rules. The framework formally models the hidden access rules and incorporates them in the distributed ACL implementations for extracting a security implementation model, and finally formulates a QSAT (satisfiability of quantified boolean formulae) based decision problem to verify whether the ACL implementation conforms to the global policy both in presence and absence of the hidden access paths.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bartal, Y., Mayer, A., Nissim, K., Wool, A.: Firmato: A Novel Firewall Management Toolkit. ACM Transaction on Computer Systems 22(4), 381–420 (2004)
Al-Shaer, E.S., Hamed, H.H.: Discovery of Policy Anomalies in Distributed Firewalls. In: Proceedings of IEEE INFOCOM 2004, Hong Kong, China, March 2004, pp. 2605–2626 (2004)
Uribe, T.E., Cheung, S.: Automatic Analysis of Firewall and Network Intrusion Detection System Configurations. In: ACM Workshop on Formal Methods in Security Engineering, Washington, DC, USA, October 2004, pp. 66–71 (2004)
Yuan, L., Mai, J., Su, Z., Chen, H., Chuah, C., Mohapatra, P.: FIREMAN: A Toolkit for Firewall Modeling and Analysis. In: 27th IEEE Symposium on Security and Privacy, Oakland, CA, USA (May 2006)
Matsumoto, S., Bouhoula, A.: Automatic Verification of Firewall Configuration with Respect to Security Policy Requirements. In: Proceedings of the International Workshop on Computational Intelligence in Security for Information Systems (CISIS 2008), Barcelona, Spain, October 2008, pp. 123–130 (2008)
Liu, A.X., Gouda, M.G.: Complete Redundancy Detection in Firewalls. In: Jajodia, S., Wijesekera, D. (eds.) Data and Applications Security 2005. LNCS, vol. 3654, pp. 193–206. Springer, Heidelberg (2005)
High Level Firewall Language, http://www.hlfl.org/ (Accessed on April 2009)
Zhang, B., Al-Shaer, E.S., Jagadeesan, R., Riely, J., Pitcher, C.: Specifications of A High-level Conflict-Free Firewall Policy Language for Multi-domain Networks. In: 12th ACM Symposium on Access control models and Technologies (SACMAT 2007), France, June 2007, pp. 185–194 (2007)
CISCO: Configuring IP access lists. CISCO white papers 23602 edition (July 2007)
Mahajan, Y.S., Fu, Z., Malik, S.: Zchaff 2004: An efficient SAT solver. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 360–375. Springer, Heidelberg (2005)
Zhang, C.C., Winslet, M., Gunter, C.A.: On the Safety and Efficiency of Firewall Policy Deployment. In: 28th IEEE Symposium on Security and Privacy, Oakland, CA, USA, May 2007, pp. 33–50 (2007)
Matousek, P., Rab, J., Rysavy, O., Sveda, M.: A Formal model for Network-wide Security Analysis. In: Proceedings of 15th IEEE International Conference and Workshop on ECBS, Belfast, Ireland (2008)
Hofmeister, T., Schoning, U., Schuler, R., Watanabe, O.: A Probabilistic 3-SAT Algorithm further improved. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 192–202. Springer, Heidelberg (2002)
QDIMACS Standard Version 1.1., http://www.qbflib.org/qdimacs.html (Accessed on March 2009)
Yu, Y., Malik, S.: Yquaffle QBF solver, http://www.princeton.edu/chaff/quaffle.html (Accessed on March 2009)
Giunchinglia, E., Narrizzano, M., Tacchella, A.: QUBE: A System for deciding quantified boolean formulas satisfiability. In: International Joint Conference on Automated Reasoning (IJCAR), pp. 364–369 (2001)
Zhang, L., Malik, S.: Towards Symmetric treatment of Conflicts and satisfaction in quantified Boolean satisfiability. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 200–215. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bera, P., Ghosh, S.K., Dasgupta, P. (2009). Formal Verification of Security Policy Implementations in Enterprise Networks. In: Prakash, A., Sen Gupta, I. (eds) Information Systems Security. ICISS 2009. Lecture Notes in Computer Science, vol 5905. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-10772-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-642-10772-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-10771-9
Online ISBN: 978-3-642-10772-6
eBook Packages: Computer ScienceComputer Science (R0)