Modeling and Verification of Firewall and IPSec Policies Using Binary Decision Diagrams

Abstract

As firewall is the main front-end defense, IPSec is the standard for secure Internet communications, providing traffic integrity, confidentiality and authentication. Although IPSec supports a rich set of protection modes and operations, its policy configuration remains a complex and error-prone task. Unlike firewalls, IPSec exhibits more complex semantic that allows for triggering multiple rule actions of different security modes. This inherent complexity increases significantly the potential of policy misconfiguration and can violate the integrity of IPSec VPN security. Secure and safe deployment of IPSec requires thorough and automated analysis of the policy configuration consistency for firewall and IPSec devices across the entire network. In this chapter, we present a general composable model based on using Boolean expressions that can represent different ACL filtering semantics. We use this model to derive a canonical representation for firewall and IPSec policies using Ordered Binary Decision Diagrams. Based on this representation, we develop a comprehensive framework to classify and identify conflicts in a single firewall and IPSec device (intra-policy conflicts) or between different firewall and IPSec devices (inter-policy conflicts) in enterprise networks. Our testing and evaluation study on different network environments demonstrates the effectiveness and efficiency of our approach for identifying conflicts in firewall and IPSec policies.