Efficient verification of packet networks

Network management will benefit from automated tools based upon formal methods. In these tools, the algorithm for computing reachability is the core algorithm for verifying network properties in the data plane. This dissertation presents efficient algorithms for computing reachability and verifying network properties for a single network with both packet filters and transformers, and for interconnected networks.

For computing port to port reachability in a network, we present a new formal method for a new tool, Atomic Predicates (AP) Verifier, which is much more time and space efficient than existing tools. Given a set of predicates representing packet filters, AP Verifier computes a set of atomic predicates, which is minimum and unique. The use of atomic predicates dramatically speeds up computation of network reachability. AP Verifier also includes algorithms to process network update events and check compliance with network policies and properties in real time.

Packet transformers are widely used in Internet service provider networks, datacenter infrastructures, and layer-2 networks. Existing network verification tools do not scale to such networks with large numbers of different transformers. We present a new tool, AP+ Verifier, based upon a new algorithm for computing atomic predicates for networks with both packet filters and transformers. For performance evaluation, we use network datasets with different types of transformers (i.e., MPLS tunnels, IP-in-IP tunnels, and NATs). We found that AP+ Verifier is more time and space efficient than prior tools by orders of magnitude.

The Internet consists a large collection of networks. To debug reachability problems, a network operator often asks operators of other networks for help by telephone or email. We present a new protocol, COVE, and an efficient data structure for automating the exchange of data plane reachability information between networks in a business relationship. COVE is designed to improve a network's views of forward and reverse reachability with partial deployment in mind. COVE is scalable to very large networks in the Internet. We illustrate applications of COVE to perform useful network management tasks, which cannot be done effectively using existing methods and tools.