基于CSP的OpenFlow包消息机制形式化建模与验证

发布时间：2020-07-03 19:55

【摘要】：软件定义网络(Software-Defined Networking,简称SDN)是一种区别于传统网络的新型网络架构,它打破了传统网络的限制,实现了网络的灵活性和可编程性。传统网络将管理层和数据层紧密联系在一起,导致网络的部署及应用变得十分复杂且难以管理,长期局限并妨碍了网络基础设施的创新和发展。SDN突破性地将网络中的控制逻辑和底层转发设备分离,将网络管理集中化。OpenFlow协议是SDN的核心技术之一,也是SDN底层实现的最理想方式之一。OpenFlow协议简化了对网络的管理,并且增强了网络配置的一致性和准确性,在全球范围内取得了重要影响,具有广阔的应用前景,但同时也给网络的安全性和可靠性带来新的挑战。本文的研究对象OpenFlow包消息机制(OpenFlow Bundle Mechanism)是OpenFlow协议针对网络安全性提出的一种消息通信方式,其目的是通过保障消息的一致性和完整性来提高网络的安全性和可靠性。本文基于形式化方法的高可信特性和OpenFlow协议安全性和可靠性的需求,利用形式化方法中的通信顺序进程(Communicating Sequential Processes,简称CSP)理论对OpenFlow包消息机制进行形式化分析和验证。通过对系统内组件的抽象和建模,将系统抽象为控制器组件、交换机组件以及包组件三个模块,并分别完成三个模块的CSP建模,构建各模块之间的联系,完成对整个通信系统的CSP建模。然后,我们使用模型检测工具PAT(Process Analysis Toolkit,简称PAT)对构建的CSP模型进行编码和模拟验证,从验证结果得出OpenFlow包消息机制满足无死锁性、原子性、顺序性、并发性以及可调度性这五项性质,通过严密完整的形式化验证方法证明了OpenFlow包消息机制能够保障消息的一致性和完整性。最后,我们在原模型的基础上引入现实世界中入侵者的攻击行为案例,对入侵者的行为进行建模后与原系统进行并发,对攻击行为进行分析和验证,发现了机制中存在的不安全性,并提出了符合实际的优化方案,从而提高了OpenFlow协议的安全性和可靠性。
【学位授予单位】：华东师范大学
【学位级别】：硕士
【学位授予年份】：2019
【分类号】：TP393.02
【图文】：

OpenFlow包消息机制五项性质验证结果

#define FakeSuccess(aplNum[0][0]==4 && isFaked==1);#assert IntruderSystem() reaches FakeSuccess;验证结果如图5.2所示，系统可以达到 的状态，说明 OpenFlow 包消息机制不能抵御伪装攻击。根据实验结果给出的攻击成功轨迹分析，入侵者通过通道 向编号为 0 的交换机内编号为 0 的包发送添加包消息后，进程进行了内部操作 之后，返回的结果是 ，表示伪装的消息通过了交换机的预验证步骤被成功添加到包内。根据 OpenFlow 包消息机制，交换机在执行包内消息时会首先验证该消息是否合法。但是入侵者通过窃听学习

【相似文献】

相关期刊论文 前10条

1 曾春金;;基于数据库消息机制技术的企业应用集成[J];铁道通信信号;2010年06期

2 传老鹰;;深入理解BCB的消息机制[J];中文信息;2002年04期

3 王德群;在VB中运用Windows消息机制[J];滁州师专学报;2001年03期

4 杜俊勇;王国胤;;基于消息机制的实时屏幕共享技术[J];计算机科学;2005年08期

5 吕钊,顾君忠;关于CORBA消息机制的研究[J];计算机应用研究;2001年08期

6 林应，陈奇，俞瑞钊;分布式IDSS系统中基于客户／服务器思想的消息机制[J];电子计算机外部设备;1996年03期

7 闻怡洋;;理解Windows消息机制[J];软件;2001年08期

8 刘立芳;Unix/Windows NT消息机制的比较[J];电脑与信息技术;1997年05期

9 程岩;孙继昌;任国兴;张颖;;基于消息机制的算法与应用[J];山东科学;2006年05期

10 黎媛,刘日升;基于消息机制的B2B系统研究[J];计算机应用研究;2003年10期

相关会议论文 前5条

1 唐良招;罗永康;雷升楷;刘红阳;;电子商务在个性化气象服务中的应用[A];创新驱动发展 提高气象灾害防御能力——S3第三届气象服务发展论坛——公众、专业气象预报服务技术与应用[C];2013年

2 张天成;岳德君;陈迪生;于戈;;分布式专家系统中时序控制的研究与设计[A];2007年全国开放式分布与并行计算机学术会议论文集(下册)[C];2007年

3 盛腾飞;卢宏生;斯添浩;曹志强;周建毅;;基于HPNTsim的网络接口模拟平台的设计与实现[A];第二十一届计算机工程与工艺年会暨第七届微处理器技术论坛论文集[C];2017年

4 寇玮华;徐扬;;基于消息机制的分布式数据库数据请求模式研究[A];第二十一届中国数据库学术会议论文集（技术报告篇）[C];2004年

5 雷杰;;一种嵌入式实时多任务操作系统的研究与应用[A];第三届全国嵌入式技术和信息处理联合学术会议论文集[C];2009年

相关重要报纸文章 前2条

1 ;小公司推出Web Services语言[N];计算机世界;2003年

2 哈佛尼曼学者、专栏作家 安替;以开放来回应暴力[N];21世纪经济报道;2011年

相关博士学位论文 前1条

1 刘梦晓;基三体系结构存储系统相关问题的研究[D];北京理工大学;2010年

相关硕士学位论文 前10条

1 王惠文;基于CSP的OpenFlow包消息机制形式化建模与验证[D];华东师范大学;2019年

2 孙晋选;基于SOA的安全可控消息机制的研究[D];华东师范大学;2008年

3 鲁晋;现代编程方法中几项技术的研究与应用[D];中国科学院研究生院（长春光学精密机械与物理研究所）;2003年

4 罗成;基于Windows消息机制的HTTP隐蔽通道的设计与实现[D];上海交通大学;2008年

5 付亚臣;基于Windows消息机制的VB编程题评分系统的研究与应用[D];大连海事大学;2012年

6 李文烨;一种基于消息机制的程序框架及其应用研究[D];中国科学院研究生院（软件研究所）;2003年

7 徐禄;基于软件总线的无线电数据采集系统研究[D];西华大学;2014年

8 陈振东;台风预报系统关键技术的研究与实现[D];福州大学;2011年

9 刘世军;文档协同系统客户端的设计与实现[D];吉林大学;2010年

10 于军华;异地协同设计系统的开发[D];山东大学;2005年

本文编号：2740103