Verification and synthesis of firewalls using SAT and QBF

Shuyuan Zhang, Abdulrahman Mahmoud, Sharad Malik, Sanjai Narain

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Scopus citations

Abstract

Firewalls are widely deployed to safeguard the security of networks and it is critical for enterprise networks to have firewalls to prevent malicious attacks and to guarantee the normal functioning of the network. Firewalls prevent dangerous packets from entering the inner network by looking up the Access Control List (ACL) to permit or drop certain packets. However, ACLs often suffer from redundancy problems, which can degrade the performance of firewalls and the network. The contribution of this paper is threefold: 1) we present a Boolean Satisfiability (SAT) based technique that can compare the equivalence and inclusion relationship between two firewalls, which is very valuable for the testing between a given firewall and an optimized one, 2) we present a technique to discover redundancies within a firewall, and 3) we formulate the ACL optimization problem as a Quantified Boolean Formula problem (QBF) and explore its practical application using a QBF solver.

Original languageEnglish (US)
Title of host publication2012 20th IEEE International Conference on Network Protocols, ICNP 2012
DOIs
StatePublished - 2012
Event2012 20th IEEE International Conference on Network Protocols, ICNP 2012 - Austin, TX, United States
Duration: Oct 30 2012Nov 2 2012

Publication series

NameProceedings - International Conference on Network Protocols, ICNP
ISSN (Print)1092-1648

Other

Other2012 20th IEEE International Conference on Network Protocols, ICNP 2012
CountryUnited States
CityAustin, TX
Period10/30/1211/2/12

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications
  • Software

Fingerprint Dive into the research topics of 'Verification and synthesis of firewalls using SAT and QBF'. Together they form a unique fingerprint.

  • Cite this

    Zhang, S., Mahmoud, A., Malik, S., & Narain, S. (2012). Verification and synthesis of firewalls using SAT and QBF. In 2012 20th IEEE International Conference on Network Protocols, ICNP 2012 [6459944] (Proceedings - International Conference on Network Protocols, ICNP). https://doi.org/10.1109/ICNP.2012.6459944