Formal Verification of Firewall Policies

Firewalls are the mainstay of enterprise security and the most widely adopted technology for protecting private networks. The quality of protection provided by a firewall directly depends on the quality of its policy (i.e., configuration). Due to the lack of tools for verifying firewall policies, most firewalls on the Internet have been plagued with policy errors. A firewall policy error either creates security holes that will allow malicious traffic to sneak into a private network or blocks legitimate traffic and disrupts normal business processes, which in turn could lead to irreparable, if not tragic, consequences. We propose a firewall verification tool in this paper. Our tool takes as input a firewall policy and a given property, then outputs whether the policy satisfies the property. Despite of the importance of verifying firewall policies, this problem has not been explored in previous work. Due to the complex nature of firewall policies, designing algorithms for such a verification tool is challenging. In this paper, we designed and implemented a verification algorithm using decision diagrams, and tested it on both real-life firewall policies and synthetic firewall policies of large sizes. The experimental results show that our algorithm is very efficient. In practice, our firewal verification algorithm can be used in the iterative process of firewall policy design, verification, and maintenance. Note that the firewall policy verification algorithm proposed in this paper is not limited to firewalls. Rather, they can be potentially applied to other rule- based systems as well.