Verification of Distributed Firewalls

The private computer network of any large enterprise has tens, or even hundreds, of firewalls. These firewalls are placed at the entry points of the network (where the network is connected with the rest of the Internet), and at many chosen points within the network. The result is a complex firewall network that seems hard to understand or analyze. In this paper, the authors propose a method for verifying the correctness of firewall networks with tree topologies. Their method is based on identifying two types of properties of firewall trees: accept and discard properties. An accept (or discard) property of a firewall tree specifies a class of packets that should be accepted (or discarded, respectively) by the firewall tree.