计算机科学 ›› 2016, Vol. 43 ›› Issue (10): 74-80.doi: 10.11896/j.issn.1002-137X.2016.10.014
朱革,曾国荪,丁春玲,王伟
ZHU Ge, ZENG Guo-sun, DING Chun-ling and WANG Wei
摘要： OpenFlow协议是SDN网络中控制平面与数据转发平面之间进行交互的规范与标准,其正确性将直接影响到整个网络功能的实现。通过模型检测技术实现一种验证OpenFlow协议正确性的形式化方法。首先提取OpenFlow协议的核心子协议,即OpenFlow多交换机数据包转发协议作为验证的实例；然后运用协议行为自动机对该子协议进行形式化建模,并且通过时态逻辑描述协议需要进行验证的性质；最后给出算法验证协议模型是否满足给定的性质要求,以此检测OpenFlow协议是否存在正确性漏洞,以便对其进行修正。
| [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! |
|
||
首页