Projection and Division: Linear-Space Verification of Firewalls

A firewall is a packet filter that is placed at the entrance of a private network. It checks the header fields of each incoming packet into the private network and decides, based on the specified rules in the firewall, whether to accept the packet and allow it to proceed, or to discard the packet. A property of a firewall is a set of packets that the firewall is required to accept or discard. Associated with each firewall is a very large set of properties that the firewall needs to satisfy. The space and time complexity of the best known deterministic algorithm, for verifying that a given firewall satisfies a given property, is 0(n^d), where n is the number of rules in the given firewall and d is the number of fields checked by the firewall. Usually, n is around 2000 and d is 5. In this paper, we propose the first deterministic firewall verification algorithm whose space complexity is 0(n^d), linear in both n and d. This algorithm consists of three components: a projection pass, a division pass, and a probe algorithm. We applied our verification algorithm to over two million firewall-property pairs, varying n from 100 to 10000 and fixing d at 5. From this experiment, we observed that the algorithm requires (900 + 0.5n) Kilobytes of storage and in the order of 10 seconds execution time.