Model Checking the OpenFlow Protocol Using SPIN

6th Annual 2018 International Conference on Geo-Spatial Knowledge and Intelligence

Shi, Huiling^1 ; Zhang, Wei^1 ; Zhang, Xinchang^1

Shandong Provincial Key Laboratory of Computer Networks, Shandong Computer Science Center, National Supercomputer Center in Jinan, Qilu University of Technology, Shandong Academy of Sciences, Jinan, China^1

关键词: Data-forwarding;    Formal model;    Logical control;    Model checker;    Model description languages;    Model-checking technology;    Protocol verification;    Software defined networking (SDN);   

Others  :  https://iopscience.iop.org/article/10.1088/1755-1315/234/1/012071/pdf
DOI  :  10.1088/1755-1315/234/1/012071

来源: IOP

【 摘 要 】

Software-Defined Networking (SDN) is a new architecture of separation of logical control and data forwarding. Although this separation has brought many benefits to the network, it also exposes the network to more risks. OpenFlow protocol is a communication protocol between them. The correct behavior of OpenFlow protocol is critical to SDN. Model checking technology has been widely applied to the protocol verification. This paper presents the process of model checking the OpenFlow protocol using SPIN. First, we describe an abstract formal model of OpenFlow protocol. And then we translate the model with PROMELA which is a model description language. Finally we apply the model checker (SPIN) to verify properties. In the process, it is realized that to pay more attention to the delay of SDN is more efficient when updating OpenFlow protocol version.