Formal Checking of Multiple Firewalls

TL;DR

This paper presents a formal, automated method for verifying the correctness of multiple firewalls against high-level security policies, providing feedback for correction and ensuring policy consistency.

Contribution

It introduces a novel formal verification approach for multi-firewall configurations, including a priority-based method to prevent policy incoherencies, implemented with a satisfiability solver.

Findings

Method is correct and complete

Efficient verification demonstrated on case studies

Provides useful feedback for configuration correction

Abstract

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.