Formal Checking of Multiple Firewalls
This addresses security vulnerabilities for enterprises deploying multiple firewalls, though it appears incremental as it builds on existing formal verification techniques.
The paper tackles the problem of errors in complex firewall networks by proposing a formal, automatic method to check multiple firewalls against a security policy, with experiments demonstrating its efficiency.
When enterprises deploy multiple firewalls, a packet may be examined by different sets of firewalls. 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 multiple 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 in order to correct the firewall configurations. Furthermore, we propose a priority-based approach to ensure that no incoherencies 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. Experiment conducted on relevant case studies demonstrates the efficiency of our approach.