Validating Network Security Policies via Static Analysis of Router ACL Configuration

The security of a network depends on how its design fulfils the organization’s security policy. One aspect of security is reachability: whether two hosts can communicate. Network designers and operators face a very difficult problem in verifying the reachability of a network, because of the lack of automated tools, and calculations by hand are impractical because of the often sheer size of networks. The reachability of a network is influenced by packet filters, routing protocols, and packet transformations. A general framework for calculating the joint effect of these three factors was published recently. This thesis partially validates that framework through a detailed Java implementation, with the creation of an automated solution which demonstrates that the effect of statically configured packet filters on the reachability upper bounds of a network can be computed efficiently. The automated solution performs its computations purely based on the data obtained from parsing router configuration files. Mapping all packet filter rules into a data structure called PacketSet, consisting of tuples of permitted ranges of packet header fields, is the key to easy manipulation of the data obtained from the router configuration files. This novel approach facilitates the validation of the security policies of very large networks, which was previously not possible, and paves the way for a complete automated solution for static analysis of network reachability.