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, 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.
Keywords: network security, distributed firewall configuration, formal verification, SMT solver.
Download Full-Text
ABOUT THE AUTHORS
Nihel Ben Youssef
Higher School of Communication of Tunis
Adel Bouhoula
Higher School of Communication of Tunis
Nihel Ben Youssef
Higher School of Communication of Tunis
Adel Bouhoula
Higher School of Communication of Tunis