A fast method of verifying network routing with back-trace header space analysis

It is a tough job for operators to make perfectly accurate configuration of many network elements in large networks. Erroneous configurations may cause critical incidents in network, on which many ICT systems are running. It may also result in a security hole as well as system incidents. There has been much work on preventing erroneous configurations, but this has taken a lot of time to verify routing with large networks. We propose a new method of verifying network routing. It only focuses on verifying isolation and reachability, but it can verify these properties with O(R 2 ), where R is the number of flow entries, while the performance of an existing method of verification is O(R 3 ). We also provide a proof of the correctness of our method.