Formal Checking of Multiple Firewalls
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, the authors propose a formal and automatic method for checking whether multiple firewalls reacts 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, they propose a priority-based approach to ensure that no incoherencies exist within the security policy.