  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.
