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, we propose a method for verifying the correctness of firewall networks with tree topologies. Our 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. We present two algorithms that can be used to decide whether a given firewall tree satisfies a given, accept or discard, property of that tree.