Formal correctness of conflict detection for firewalls

ABSTRACT

We describe the formalization of a correctness proof for a conflict detection algorithm for firewalls in the Coq Proof Assistant. First, we give formal definitions in Coq of a firewall access rule and of an access request to a firewall. Formally, two rules are in conflict if there exists a request on which one rule would allow access and the other would deny it. We express our algorithm in Coq, and prove that it finds all conflicts in a set of rules. We obtain an OCaml version of the algorithm by direct program extraction. The extracted program has successfully been applied to firewall specifications with over 200,000 rules.

REFERENCES

• 1: Ehab Al-Shaer, Hazem Hamed, Raouf Boutaba, and Masum Hasan. Conflict classification and analysis of distributed firewall policies. IEEE Journal on Selected Areas in Communications, 23(10):2069--2084, October 2005.
• 2: Ehab S. Al-Shaer and Hazem H. Hamed. Firewall policy advisor for anomaly discovery and rule editing. In IFIP/IEEE Eighth International Symposium on Integrated Network Management, pages 17--30, 2003.
• 3: Ehab S. Al-Shaer and Hazem H. Hamed. Discovery of policy anomalies in distributed firewalls. In Proceedings of IEEE Infocom, volume 4, pages 2605- 2626, 2004.
• 4: Florin Baboescu , George Varghese, Fast and Scalable Conflict Detection for Packet Classifiers, Proceedings of the 10th IEEE International Conference on Network Protocols, p.270-279, November 12-15, 2002
• 5: Yair Bartal , Alain Mayer , Kobbi Nissim , Avishai Wool, Firmato: A novel firewall management toolkit, ACM Transactions on Computer Systems (TOCS), v.22 n.4, p.381-420, November 2004 [doi>10.1145/1035582.1035583]
• 6: Yves Bertot , Pierre Casteran, Interactive Theorem Proving and Program Development, SpringerVerlag, 2004
• 7: James Boney. CISCO IOS in a Nutshell. O'Reilly, first edition, 2001.
• 8: F. Cuppens, N. Cuppens-Boulahia, and J. García-Alfaro. Detection and removal of firewall misconfiguration. In IASTED International Conference on Communication, Network, and Information Security, 2005.
• 9: P. Dybjer, Comparing integrated and external logics of functional programs, Science of Computer Programming, v.14 n.1, p.59-79, Jun. 1990 [doi>10.1016/0167-6423(90)90058-L ]
• 10: David Eppstein , S. Muthukrishnan, Internet packet filter management and rectangle geometry, Proceedings of the twelfth annual ACM-SIAM symposium on Discrete algorithms, p.827-835, January 07-09, 2001, Washington, D.C., United States
• 11: Pasi Eronen and Jukka Zitting. An expert system for analyzing firewall rules. In 6th Nordic Workshop on Secure IT Systems, pages 100--107, 2001.
• 12: Jean-Yves Girard, Linear logic and parallelism, Advanced School on Mathematical models for the semantics of parallelism, p.166-182, January 1987, Rome, Italy
• 13: J. D. Guttman, Filtering postures: local enforcement for global policies, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.120, May 04-07, 1997
• 14: Joshua D. Guttman and Amy L. Herzog. Rigorous automated network security management. International Journal of Information Security, 2003. To appear.
• 15: Hazem Haded and Ehab Al-Shaer. Taxonomy of conflicts in network security policies. IEEE Communications Magazine, 44(3):134--141, March 2006.
• 16: Adiseshu Hari, Subhash Suri, and Guru Parulkar. Detecting and resolving packet filter conflicts. In Proceedings of IEEE Infocom, volume 3, pages 1203--1212, 2000.
• 17: W. A. Howard. The formulae-as-types notion of construction. In J. P. Selding and J. R. Hindley, editors, To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 479--490. Academic Press, 1980.
• 18: Pierre Letouzey. A new extraction for Coq. In Types for Proofs and Programs, Second International Workshop, volume 2646 of Lecture Notes in Computer Science, pages 200--219. Springer-Verlag, 2003.
• 19: Alex X. Liu and Mohamed G. Gouda. Complete redundancy detection in firewalls. In Data and Applications Security, volume 3654 of Lecture Notes in Computer Science, pages 196--209. Springer-Verlag, 2005.
• 20: Mahdi Mankai. Vérification et analyse des politiques de contrôle d'accès: Application au langage XACML. Master's thesis, Université du Québec en Outaouais, January 2005.
• 21: Mahdi Mankai and Luigi Logrippo. Access control policies: Modeling and validation. In K. Adi, D. Amyot, and L. Logrippo, editors, 5th NOTERE Conferenc (Nouvelles Technologies de la Répartition), pages 85--91, Gatineau, Canada, 2005.
• 22: Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984. Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980.
• 23: Alain Mayer , Avishai Wool , Elisha Ziskind, Fang: A Firewall Analysis Engine, Proceedings of the 2000 IEEE Symposium on Security and Privacy, p.177, May 14-17, 2000
• 24: C. Paulin-Mohring, Extracting &ohgr;'s programs from proofs in the calculus of constructions, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.89-104, January 11-13, 1989, Austin, Texas, United States [doi>10.1145/75277.75285]
• 25: J. Qian, ACLA: A framework for Access Control List (ACL) Analysis and Optimization, Proceedings of the IFIP TC6/TC11 International Conference on Communications and Multimedia Security Issues of the New Century, p.4, May 21-22, 2001
• 26: Jeff Sedayao, Cisco IOS access lists, O'Reilly & Associates, Inc., Sebastopol, CA, 2001
• 27: Morten Heine B. Sørensen and P. Urzyczyn. Lectures on the Curry-Howard Isomorphism. Elsevier Science, 2006.
• 28: Sun Microsystems. A brief introduction to XACML. http://-www.-oasis-open-.org/-committees/-download.php/-2713/-Brief_Introduction_to_XACML.html, 2003.
• 29: The Coq Development Team. LogiCal Project. The Coq Proof Assistant. Reference Manual. Version 8. INRIA, 2004. Available at the web page http://pauillac.inria.fr/coq/coq-eng.html+.
• 30: Tomás E. Uribe , Steven Cheung, Automatic analysis of firewall and network intrusion detection system configurations, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA [doi>10.1145/1029133.1029143]
• 31: Avishai Wool, Architecting the Lumeta firewall analyzer, Proceedings of the 10th conference on USENIX Security Symposium, p.7-7, August 13-17, 2001, Washington, D.C.
• 32: Lihua Yuan , Jianning Mai , Zhendong Su , Hao Chen , Chen-Nee Chuah , Prasant Mohapatra, FIREMAN: A Toolkit for FIREwall Modeling and ANalysis, Proceedings of the 2006 IEEE Symposium on Security and Privacy, p.199-213, May 21-24, 2006 [doi>10.1109/SP.2006.16]
• 33: Charles C. Zhang , Marianne Winslett , Carl A. Gunter, On the Safety and Efficiency of Firewall Policy Deployment, Proceedings of the 2007 IEEE Symposium on Security and Privacy, p.33-50, May 20-23, 2007 [doi>10.1109/SP.2007.32]

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Mechanical verification

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Security and protection (e.g., firewalls)

General Terms:
Security, Verification

Keywords:
coq, firewall