Network verification involves checking that the dataplane of a network validates formulas expressing network reachability properties such as “Virtual Machines cannot access Protected Servers”. Speedups have been achieved using symbolic execution, incremental verification, and predicate abstraction. However, large operational networks with ~10^5 hosts can still take days to verify as the number of station pairs grows quadratically.

Fortunately, such networks often employ design patterns that impose regularities. For example, modern data center networks often use fat trees containing nearly-identical backup routers interconnected in symmetrical patterns. To exploit these regularities, we introduce network transformations: given a reachability formula φ and a network N , we transform N into (a simpler to verify) network N’ and a corresponding transformed formula φ’ such that (for example) φ is valid in N if and only φ’ is valid in N’.

We introduce two kinds of network transformations: those that exploit network symmetry (say between backup routers) and those that involve what we call network surgery, in which irrelevant or redundant sets of nodes, headers, ports, or rules are “sliced” away. We prove the validity of our network transformations using Van Benthem-Hennessy-Milner style bisimulation, showing that one can associate bisimulations to each transformation connecting networks and formulas with their transforms. To do all this requires a formal theory of networks and their transforms. Our work is a development in an area of current wide interest: applying programming language techniques (in our case bisimulation and modal logic) to problems in switching networks.

We provide experimental evidence that our network transformations can speed up large datacenter network verifications by factors ranging from 10x to 100x.