软件定义网络的形式化建模与验证

发布时间：2022-11-05 07:03

　　软件定义网络（Software-Defined Networking,SDN）是一种新兴的网络架构,能够解决传统网络层级复杂,以至难以管理和创新的问题。该架构将控制逻辑从转发设备上分离出来,形成逻辑上集中的中心控制器,并提供网络可编程性。SDN的出现不仅推动了网络架构的更迭,更带来了网络开发方法的变革,可以预见在未来的网络开发流程之中,形式化方法必定处于极其重要的地位。本文通过形式化方法建模SDN并验证相关性质。对于与数据转发逻辑有关的性质,扩展了知名的软件定义网络编程语言NetKAT,提出了能描述虚拟局域网（VLAN）、拥有更强表达能力并且支持模型检测的语言PDNet,研究了PDNet的操作语义,并基于操作语义证明了PDNet和NetKAT在表达能力上的联系与差别。对于与SDN模块或应用的设计、功能和安全有关的性质,基于图灵奖得主C.A.R.Hoare教授提出的通信顺序进程（CSP）设计了系统建模框架,并在模型检测工具PAT（Process Analysis Toolkit）中进行了实现。基于该框架,本文建模并验证了开源控制器Floodlight的基础模块以及安全控制器TopoGua... 

【文章页数】：147 页

【学位级别】：博士

【文章目录】：
摘要
Abstract
第一章 绪论
    1.1 研究背景和动机
    1.2 研究现状和相关工作
    1.3 本文的主要工作
    1.4 本文的组织结构
第二章 背景知识
    2.1 软件定义网络
    2.2 虚拟局域网
    2.3 形式语言与形式语义
    2.4 NetKAT语言
    2.5 本章小结
第三章 网络编程语言PDNet
    3.1 NetKAT的第二种操作语义
    3.2 PDNet语言
    3.3 NetKAT与PDNet对比与证明
    3.4 本章小结
第四章 SDN系统建模框架
    4.1 框架概述
    4.2 转发设备模型
    4.3 主机模型
    4.4 攻击者模型
    4.5 本章小节
第五章 Floodlight控制器的建模与验证
    5.1 Floodlight基本模块
    5.2 Floodlight模型
    5.3 系统模型与验证
    5.4 本章小节
第六章 TopoGuard安全机制的建模与验证
    6.1 Topo Guard机制
    6.2 Topo Guard模型
    6.3 系统模型与验证
    6.4 改进的Topo Guard建模与验证
    6.5 本章小节
第七章 总结与展望
    7.1 本文工作总结
    7.2 后续工作展望
参考文献
致谢
研究成果


【参考文献】：
期刊论文
[1]软件定义网络（SDN）研究进展[J]. 张朝昆,崔勇,唐翯翯,吴建平.  软件学报. 2015(01)
[2]基于OpenFlow的SDN技术研究[J]. 左青云,陈鸣,赵广松,邢长友,张国敏,蒋培成.  软件学报. 2013(05)

博士论文
[1]基于质量演算的无线网络形式语义与分析[D]. 吴茜.华东师范大学 2016



本文编号：3702130