Formal integrated network security analysis tool: formal query-based network security configuration analysis

Owing to increasing complexity of network configurations with large topology and use of heterogeneous network services, enterprise networks deploy various security measures based on the organisational security policies. Typically, security policy represents the high level requirements for controlling the resource accesses by traffic source, destination, protocol, access time and so on. Security policies are implemented in the network devices (routers, firewalls and so on) in a distributed fashion through various access control lists (ACLs). The ACL configurations may contain different level of inconsistencies which may make the network vulnerable. In addition, there may exist inconsistent `hidden access paths´ in the implementation because of transitive access relationships between the network services. Further, the failure of network link(s) may form alternative routing paths that violate ACL. Manual analysis of this problem can be overwhelming and potentially inaccurate. In this study, a query-based formal security analysis tool has been presented that automates the process using Boolean satisfiability (SAT). The tool allows network administrators to systematically evaluate the distributed ACL configurations through various standard and complex service access queries. The tool evaluates the static access queries through SAT-based decision procedures, and the fault-based queries (under network link failures) through graph mining procedures.