| 基于模型检测的OpenFlow多交换机数据包转发协议的分析与验证 |
| |
| 引用本文： | 朱革,曾国荪,丁春玲,王伟.基于模型检测的OpenFlow多交换机数据包转发协议的分析与验证[J].计算机科学,2016,43(10):74-80. |
| |
| 作者姓名： | 朱革 曾国荪 丁春玲 王伟 |
| |
| 作者单位： | 同济大学计算机科学及技术系 上海201804;高效能服务器和存储技术国家重点实验室 济南250101,同济大学计算机科学及技术系 上海201804,同济大学化学系 上海201804,同济大学计算机科学及技术系 上海201804 |
| |
| 基金项目： | 本文受863863项目(2009AA012201),国家自然科学基金项目(61272107,61202173,61103068),上海市优秀学科带头人计划项目(10XD1404400),华为创新研究计划项目(IRP-2013-12-03),高效能服务器和存储技术国家重点实验室开放基金项目(2014HSSA10)资助 |
| |
| 摘 要： | OpenFlow协议是SDN网络中控制平面与数据转发平面之间进行交互的规范与标准,其正确性将直接影响到整个网络功能的实现。通过模型检测技术实现一种验证OpenFlow协议正确性的形式化方法。首先提取OpenFlow协议的核心子协议,即OpenFlow多交换机数据包转发协议作为验证的实例；然后运用协议行为自动机对该子协议进行形式化建模,并且通过时态逻辑描述协议需要进行验证的性质；最后给出算法验证协议模型是否满足给定的性质要求,以此检测OpenFlow协议是否存在正确性漏洞,以便对其进行修正。
|
| 关 键 词： | OpenFlow协议 模型检测 协议行为自动机 时态逻辑 |
| 收稿时间： | 2015/9/26 0:00:00 |
| 修稿时间： | 2016/2/26 0:00:00 |
Analysis and Verification for OpenFlow Multi-switch Protocol Based on Model Checking |
| |
| ZHU Ge,ZENG Guo-sun,DING Chun-ling and WANG Wei.Analysis and Verification for OpenFlow Multi-switch Protocol Based on Model Checking[J].Computer Science,2016,43(10):74-80. |
| |
| Authors: | ZHU Ge ZENG Guo-sun DING Chun-ling and WANG Wei |
| |
| Affiliation: | Department of Computer Science and Technology,Tongji University,Shanghai 201804,China;State Key Laboratory of High-end Server & Storage Technology,Jinan 250101,China,Department of Computer Science and Technology,Tongji University,Shanghai 201804,China,Department of Chemistry,Tongji University,Shanghai 201804,China and Department of Computer Science and Technology,Tongji University,Shanghai 201804,China |
| |
| 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. |
| |
| Keywords: | OpenFlow protocol Model checking Protocol action automata machine Temporary logic |
|
| 点击此处可从《计算机科学》浏览原始摘要信息 |
|
点击此处可从《计算机科学》下载全文 |
|
