Verification of switching network properties using satisfiability

In this paper, we consider a network of OpenFlow switches as an acyclic network of high-dimensional Boolean functions. We reduce classic network properties to logic functions over the variables of this network, and demonstrate that these properties hold if and only if the conjunction of the derived Boolean network and proposition is satisfied. We demonstrate that the derived satisfiability instance is polynomially related to the size of the switch network and the network property. The problem of verification of OpenFlow networks is thus demonstrated to be in the class NP. We show that OpenFlow Verification is NP-complete by a reduction from SAT. We further consider a slight restriction in the OpenFlow rule set to prefix rules, and demonstrate that OpenFlow Verification is polynomial when the ruleset is restricted to prefix rules.