MR-Verifier: Verifying Open Flow Network Properties Based on MapReduce

Since faults in the configurations of flow tables arise commonly in Open Flow network, this paper proposes a tool called MR-Verifier verifying network properties. Based on MapReduce, MR-Verifier can verify network properties in parallel, providing fast non-real-time verification. On the base of it, when network states change, MR-Verifier can conduct verification incrementally, realizing real-time verification. To accelerate verification process further, it converts operations on matching fields of rules with the help of atomic predicates. Theoretical analysis and experimental results demonstrate that MR-Verifier is about 40 times faster than Hassel on the average, and performs verifying within tens or hundreds of microseconds per link up while Net Plumber and Veriflow use several seconds. Additionally, MR-Verifier is much more space efficient than Hassel.