Abstract
A drawback of stateless firewalls is that they have no memory of previous packets which makes them vulnerable to specific attacks . A stateful firewall is connection-aware, offering finer-grained control of network traffic. Unfortunately, configuring stateful firewalls is highly error prone. That is due to the potentially large number of entangled filtering rules, besides the difficulty for the administrator to apprehend the stateful filtering notions. In this paper, we propose the first formal and automatic method to check whether a stateful firewall reacts correctly according to a security policy given in an high level declarative language. When errors are detected, some feedback is returned to the user in order to correct the firewall configuration. We show that our method is both correct and complete. Finally, it has been implemented in a prototype of verifier based on a satisfiability solver modulo theories (SMT). The results obtained are very promising..
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.
References
Abbes, T., Bouhoula, A., Rusinowitch, M.: Inference system for detecting firewall filtering rules anomalies. In: Proc. of the 23rd Annual ACM Symp. on Applied Computing (2008)
Al-Shaer, E., Hamed, H.: Discovery of policy anomalies in distributed firewalls. IEEE Infocomm (2004)
Brucker, A., Wolff, B.: Test-sequence generation with hol-testGen with an application to firewall testing. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 149–168. Springer, Heidelberg (2007)
Benelbahri, M., Bouhoula, A.: Tuple based approach for anomalies detection within firewall filtering rules. In: 12th IEEE Symp. on Computers and Communications (2007)
Gouda, M., Liu, A.X.: A Model of Stateful Firewalls and its Properties. In: Proc. of International Conference on Dependable Systems and Networks, DSN 2005 (2005)
Cupens, F., Cuppens-Boulahia, N., Sans, T., Miege, A.: A formal approach to specify and deploy a network security policy. In: Second Workshop on Formal Aspects in Security and Trust, pp. 203–218 (2004)
Dutertre, B., Moura, L.: The yices smt solver (2006), http://yices.csl.sri.com/tool-paper.pdf
Eronen, P., Zitting, J.: An expert system for analyzing firewall rules. In: Proc. of 6th Nordic Workshop on Secure IT Systems (2001)
Netfilter/IPTables (2005), http://www.netfilter.org/
Buttyan, L., Pek, G., Thong, T.: Consistency verification of stateful firewalls is not harder than the stateless case. Proc. of Infocommunications Journal LXIV (2009)
Hamdi, H., Mosbah, M., Bouhoula, A.: A domain specific language for securing distributed systems. In: Second Int. Conf. on Systems and Networks Communications (2007)
CheckPoint FireWall-1 (March 25, 2005), http://www.checkpoint.com/
Bartal, Y., Mayer, A.J., Nissim, K., Wool, A.: Firmato: A novel firewall management toolkit. In: IEEE Symposium on Security and Privacy (1999)
Cisco PIX Firewalls (March 25, 2005), http://www.cisco.com/
Lui, A.X., Gouda, M., Ma, H., Ngu, A.: Firewall queries. In: Proc. of the 8th Int. Conf. on Principles of Distributed Systems, pp. 197–212 (2004)
Pornavalai, C., Chomsiri, T.: Firewall policy analyzing by relational algebra. In: The 2004 Int. Technical Conf. on Circuits/Systems, Computers and Communications (2004)
Wool, A.: A quantitative study of firewall configuration errors. IEEE Computer 37(6) (2004)
Mayer, A., Wool, A., Ziskind, E.: Fang: A firewall analysis engine. In: Proc. of the 2000 IEEE Symp. on Security and Privacy, pp. 14–17 (2000)
Postel, J.: Internet control message protocol. RFC 792 (1981)
Chapman, D.B.: Network (in) security hrough IP packet filtering. In: Proceedings of the Third Usenix Unix Security Symposium, pp. 63–76 (1992)
Ben Youssef, N., Bouhoula, A.: Automatic Conformance Verification of Distributed Firewalls to Security Requirements. In: In Proc. of the IEEE Conference on Privacy, Security, Risk and Trust, PASSAT (2010)
Alfaro, J.G., Bouhalia-cuppens, N., Cuppens, F.: Complete analysis of configuration rules to guarantee reliable network security policies. In: IEEE Symposium on Security and Privacy (May 2006)
Postel, J., Reynolds, J.: File transfer protocol. RFC 959 (1985)
Liu, A.X., Gouda, M.: Firewall Policy Queries. Proceeding of IEEE Transactions on Parallel and Distributed Systems (2009)
Yuan, L., Chen, H., Mai, J., Chuah, C.-N., Su, Z., Mohapatra, P.: Fireman: a toolkit for firewall modeling and analysis. In: IEEE Symposium on Security and Privacy (May 2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ben Youssef, N., Bouhoula, A. (2011). Dealing with Stateful Firewall Checking. In: Cherifi, H., Zain, J.M., El-Qawasmeh, E. (eds) Digital Information and Communication Technology and Its Applications. DICTAP 2011. Communications in Computer and Information Science, vol 166. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21984-9_42
Download citation
DOI: https://doi.org/10.1007/978-3-642-21984-9_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21983-2
Online ISBN: 978-3-642-21984-9
eBook Packages: Computer ScienceComputer Science (R0)