Automatic Conformance Verification of Distributed Firewalls to Security Requirements

Distributed firewalls are often deployed by large enterprises to filter the network traffic. However, it has been observed that the resulting complex firewall network is highly error prone and causes serious security holes. Hence, automated solutions are needed in order to check its correctness. In this paper, we propose a formal and automatic method for checking whether distributed firewalls react correctly with respect to a security policy given in a high level declarative language. When errors are detected, some useful feedback is returned to the user in order to correct the firewall configurations. Furthermore, the procedure verifies that no conflicts exist within the security policy. We show that our method is both correct and complete. Finally, it has been implemented in a prototype of verifier based on a satisfiability solver modulo theories (SMT). Experiment conducted on relevant case studies demonstrate the efficiency of our approach.