Packet Reachability Verification in OpenFlow Networks
Noriaki Yoshiura, Keigo Sugiyama · 2020
OpenFlow is a network technology that enables to control network equipment centrally, to realize complicated forwarding of packets and to change network topologies flexibly. In OpenFlow networks, network equipment is separated into OpenFlow switches and OpenFlow controllers. OpenFlow networks are configured by programs in OpenFlow controllers. NetCore is one of programming languages for OpenFlow and is used in functional programming language Haskell. Programs in Haskell may be verified in Coq which is a formal proof management system. For NetCore, a method which verifies OpenFlow networks was proposed. In the method, the properties that are verified must be described in logic manually. This paper proposes a method of automatic verification of packet reachability by automatically generating logical formulas for reachability verification. This paper also evaluates the proposed method by experiment.