TY - JOUR
T1 - Static equivalence checking for openflow networks
AU - Lee, Hyuk
AU - Choi, Jin Young
N1 - Funding Information:
This work was partly supported by a Korea University Grant and the National Research Foundation of Korea(NRF) grant funded by the Korea government(MSIT) (No. NRF-2018R1A2B6009122) and Institute of Information & communications Technology Planning & Evaluation (IITP) grant funded by the Korea government(MSIT) (No.2018-0-00532, Development of High-Assurance (?EAL6) Secure Microkernel).
Publisher Copyright:
© 2021 by the authors. Licensee MDPI, Basel, Switzerland.
PY - 2021/9
Y1 - 2021/9
N2 - Software-defined networking (SDN) provides many advantages over traditional networking by separating the control and data planes. One of the advantages is to provide programmability, which allows administrators to control the behavior of the network. The network configuration may need to be changed for some reason. Whenever such changes are made, it can be required to verify that the forwarding behavior is preserved from the existing configuration, that is, whether the ruleset is properly reflected. In this paper, we propose the forwarding behavior based equivalence checking of OpenFlow networks. We present the formal definition of the network model and the forwarding behavior of the packet flow. Based on the definition, We present a method for checking the equivalence of OpenFlow network forwarding behaviors. Next, we present the implementation of the proposed method, using the constraint satisfaction method, which will be the basis for further extension.
AB - Software-defined networking (SDN) provides many advantages over traditional networking by separating the control and data planes. One of the advantages is to provide programmability, which allows administrators to control the behavior of the network. The network configuration may need to be changed for some reason. Whenever such changes are made, it can be required to verify that the forwarding behavior is preserved from the existing configuration, that is, whether the ruleset is properly reflected. In this paper, we propose the forwarding behavior based equivalence checking of OpenFlow networks. We present the formal definition of the network model and the forwarding behavior of the packet flow. Based on the definition, We present a method for checking the equivalence of OpenFlow network forwarding behaviors. Next, we present the implementation of the proposed method, using the constraint satisfaction method, which will be the basis for further extension.
KW - Constraint satisfaction problem
KW - Formal modeling
KW - Forwarding behavior equivalence check
KW - OpenFlow
KW - Software-defined networking
UR - http://www.scopus.com/inward/record.url?scp=85114602757&partnerID=8YFLogxK
U2 - 10.3390/electronics10182207
DO - 10.3390/electronics10182207
M3 - Article
AN - SCOPUS:85114602757
VL - 10
JO - Electronics (Switzerland)
JF - Electronics (Switzerland)
SN - 2079-9292
IS - 18
M1 - 2207
ER -