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.http://www.projectfloodlight.org/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).https://www.opennetworking.org/images/stories/downloads/sdn-resources/onf-specifications/ 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!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
No Suggested Reading articles found!