A declarative approach for global network security configuration verification and evaluation

With the increasing number of security devices and rules in the network, the complexity of detecting and tracing network security configuration errors become a very challenging task. This in turn increases the potential of security breaches due to rule conflicts, requirement violations or lack of security hardening. Most of the existing tools are either limited in scope as they do not offer a global analysis of different network devices or hard to comprehensively use because these tools are not declarative. Declarative logic programming can readily express network configurations and security requirements for verification analysis. In this paper, we use Prolog to model the entire network security configurations including topology, routing, firewall and IPSec. This is implemented in a tool called ConfigAnalyzer, which was also evaluated with large network and policy sizes. The tool allows for verifying reachability and security properties in flexible and expressive manner. It also allows for evaluating security configurations in terms of accessibilities credentials and rules.