A formal framework for verifying inter-firewalls consistency

The main problem of firewall configuration is to ensure the filtering rules consistency w.r.t. a global security policy. However, the overall firewalls configuration on a network, which requires a human intervention, is often an error-prone process. Therefore, automated solutions are needed in order to detect firewall configuration inconsistencies and to check the inter-firewalls consistency. In this paper, we propose a formal modeling and verification framework based on model checking. It allows to verify automatically the end-to-end security behavior of a set of firewalls w.r.t. a global security policy. To deal with state explosion problem, two abstractions are proposed and evaluated in term of space and time complexity, according to the network size and connectivity rate.