软件定义网络(Software-Defined Networking,SDN)是一种新兴的网络架构,能够解决传统网络层级复杂,以至难以管理和创新的问题。该架构将控制逻辑从转发设备上分离出来,形成逻辑上集中的中心控制器,并提供网络可编程性。SDN的出现不仅推动了网络架构的更迭,更带来了网络开发方法的变革,可以预见在未来的网络开发流程之中,形式化方法必定处于极其重要的地位。本文通过形式化方法建模SDN并验证相关性质。对于与数据转发逻辑有关的性质,扩展了知名的软件定义网络编程语言NetKAT,提出了能描述虚拟局域网(VLAN)、拥有更强表达能力并且支持模型检测的语言PDNet,研究了PDNet的操作语义,并基于操作语义证明了PDNet和NetKAT在表达能力上的联系与差别。对于与SDN模块或应用的设计、功能和安全有关的性质,基于图灵奖得主C.A.R.Hoare教授提出的通信顺序进程(CSP)设计了系统建模框架,并在模型检测工具PAT(Process Analysis Toolkit)中进行了实现。基于该框架,本文建模并验证了开源控制器Floodlight的基础模块以及安全控制器TopoGuard的防御策略,以展示该框架的使用方法和实际价值。本文的主要内容和贡献包括以下三点:·提出了基于克莱尼代数(KA)的网络编程语言PDNet,来刻画数据层的转发逻辑。该语言对高级网络编程语言NetKAT(由康奈尔大学等研究机构提出)进行了扩展,从而能描述SDN的重要应用场景VLAN。同时,本文基于下推系统研究了PDNet的操作语义,并定义了语法导出规则。此外本文基于操作语义证明了PDNet的表达能力强于NetKAT。·总结归类了SDN三层架构以及外部环境中的软硬件设备,分析了各类对象在模型中的行为,提出了基于CSP的SDN系统建模框架。同时,本文建立了可实例化的数据层模型和四类主机模型,并为九种可能的攻击提供了建模方案,此外,为两种已知的,危害范围极广的攻击建立了攻击者模型。·基于系统建模框架,建模验证了开源控制器Floodlight的六个基本模块和安全控制器TopoGuard的攻击防御机制。对于Floodlight,我们验证了其基本模块的设计、功能与安全相关的性质。验证结果显示其拓扑发现和设备管理模块会受到链路攻击和主机攻击的危害,因此一大批与Floodlight使用类似的拓扑发现和设备管理方案的开源控制器都被这两种攻击影响。基于此,本文验证了为防御这两种攻击而设计的安全控制器TopoGuard,发现了两个严重问题,并提出了解决方案。