Computer Science ›› 2016, Vol. 43 ›› Issue (10): 74-80.doi: 10.11896/j.issn.1002-137X.2016.10.014

Previous Articles     Next Articles

Analysis and Verification for OpenFlow Multi-switch Protocol Based on Model Checking

ZHU Ge, ZENG Guo-sun, DING Chun-ling and WANG Wei   

  • Online:2018-12-01 Published:2018-12-01

Abstract: In software defined networking (SDN),OpenFlow protocol is the communication standard between the control plane and forwarding plane.Its validity and rationality will influence the performance of the whole network.This paper focused on a formal method to verify the correctness of the OpenFlow protocol by model checking.Firstly,a key protocol called OpenFlow multi-switch protocol was proposed,which is regarded as an important example.Then,a basic model for this protocol is built by protocol action automata machine.The temporary logic is used to describe some major properties that this protocol has.A model checking algorithm is given to verify these properties.Finally,the special analysis and verification for OpenFlow multi-switch protocol are conducted so that the existing faults hidden in this protocol can be found and modified.

Key words: OpenFlow protocol,Model checking,Protocol action automata machine,Temporary logic

[1] Rotsos C,Sarrar N,Uhlig S,et al.OFLOPS:An open framework for OpenFlow switch evaluation[M]∥Passive and Active Mea-surement.Springer Berlin Heidelberg,2012:85-95
[2] Canini M,Venzano D,Peresini P,et al.A NICE Way to TestOpenFlow Applications[C]∥NSDI.2012,12:127-140
[3] Ku′niar M,Canini M,Kosti′ D.OFTEN testing OpenFlow networks[C]∥2012 European Workshop on Software Defined Networking (EWSDN).IEEE,2012:54-60
[4] Shi Y.The formal verification of openfiow protocol using SPIN[J].Network & Computer Security,2014,3(9):38-43(in Chinese) 石颖.利用 SPIN实现对 OpenFlow 协议的形式化验证[J].计算机安全,2014,3(9):38-43
[5] OFTest.
[6] Khurshid A,Zhou W,Caesar M,et al.Veriflow:verifying network-wide invariants in real time[J].ACM SIGCOMM Computer Communication Review,2012,42(4):467-472
[7] Al-Shaer E,Al-Haj S.FlowChecker:Configuration analysis and verification of federated OpenFlow infrastructures[C]∥Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration.ACM,2010:37-44
[8] Ni H T.Design and Implementation of the Conformance TestSystem for OpenFlow Protocol[D].Beijing:Beijing Jiaotong University,2015(in Chinese) 倪海铜.OpenFlow 协议一致性测试系统设计与实现[D].北京:北京交通大学,2015
[9] OpenFlow Switch Consortium.OpenFlow Switch SpecificationVersion1.3.4(2014). openflow/openflow-switch-v1.3.4.pdf
[10] Lin H M,Zhang W H.Model checking:Theories,techniques andapplications[J].Chinese Journal of Electronics,2002,30(S1):1907-1912(in Chinese) 林惠民,张文辉.模型检测:理论,方法与应用[J].电子学报,2002,30(12):1907-1912
[11] Emerson E A.Temporal and modal logic[M].MIT Press Cambridge,1995
[12] Clarke E M,Grumberg O,Peled D.Model checking[M].MIT Press,1999
[13] Zhang Y Z.Research on symbolic model-checking algorithm[D].Jilin:Jilin University,2009(in Chinese) 张衍志.符号化模型检测算法的研究[D].吉林:吉林大学,2009
[14] Granas A,Dugundji J.Fixed point theory[M].Springer Science &Business Media,2013

No related articles found!
Full text



[1] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure[J]. Computer Science, 2018, 45(4): 71 -75, 88 .
[2] XIA Qing-xun and ZHUANG Yi. Remote Attestation Mechanism Based on Locality Principle[J]. Computer Science, 2018, 45(4): 148 -151, 162 .
[3] LI Bai-shen, LI Ling-zhi, SUN Yong and ZHU Yan-qin. Intranet Defense Algorithm Based on Pseudo Boosting Decision Tree[J]. Computer Science, 2018, 45(4): 157 -162 .
[4] WANG Huan, ZHANG Yun-feng and ZHANG Yan. Rapid Decision Method for Repairing Sequence Based on CFDs[J]. Computer Science, 2018, 45(3): 311 -316 .
[5] SUN Qi, JIN Yan, HE Kun and XU Ling-xuan. Hybrid Evolutionary Algorithm for Solving Mixed Capacitated General Routing Problem[J]. Computer Science, 2018, 45(4): 76 -82 .
[6] ZHANG Jia-nan and XIAO Ming-yu. Approximation Algorithm for Weighted Mixed Domination Problem[J]. Computer Science, 2018, 45(4): 83 -88 .
[7] WU Jian-hui, HUANG Zhong-xiang, LI Wu, WU Jian-hui, PENG Xin and ZHANG Sheng. Robustness Optimization of Sequence Decision in Urban Road Construction[J]. Computer Science, 2018, 45(4): 89 -93 .
[8] LIU Qin. Study on Data Quality Based on Constraint in Computer Forensics[J]. Computer Science, 2018, 45(4): 169 -172 .
[9] ZHONG Fei and YANG Bin. License Plate Detection Based on Principal Component Analysis Network[J]. Computer Science, 2018, 45(3): 268 -273 .
[10] SHI Wen-jun, WU Ji-gang and LUO Yu-chun. Fast and Efficient Scheduling Algorithms for Mobile Cloud Offloading[J]. Computer Science, 2018, 45(4): 94 -99, 116 .