Verification and synthesis of firewalls using SAT and QBF

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.