网络可信态的功能性能统一验证方法研究

Software defined networking technology brings a comprehensive reform to network infrastructure, while facing new security challenges on centralized control idea. This project focuses on network controller and network programming interface, and perform to solve the problem using formal verification methods to ensure trustworthness of the network. First, we carry out the requirement analysis against the SDN control system, as well as the network elements and abstract modeling and formal description of functional performance. Then, for trusted network state problems, we study the functional performance unified verification logic characterization and develop the process for correctly state decision of the network. We then propose a decision method for SDN controller correction based on interactive Markov chain, and converse it to a optimal reachability problems, thereby forming a unified verification algorithm. At the same time, we carry out bisimulation equivalence state reduction method to study the quotient model structure and behavior equivalent mechanism, and prove scheduling reduction consistency theory. Finally, through the expansion of existing SDN NBI programming language, we carry out verification of application development and develop verification tools. In this way, this project propose new idea and method to build a self-control network system and provide a security guarantee to the healthy development of the network infrastructure.

软件定义网络技术给网络基础设施带来了全面的革新，其集中控制的思想又面临新的安全挑战。本项目关注SDN控制器和编程接口的功能正确、性能可满足问题，采用形式化验证方法确保SDN控制系统的可信。首先开展SDN控制系统的验证需求，对网络元素进行抽象和建模，并描述功能性能特征；针对SDN控制器的可信态，研究功能性能统一验证的逻辑刻画和网络正确态可满足态的判定过程，从而构建统一的验证框架；研究基于交互式马尔科夫链的SDN控制器功能正确性判定，并转化为模型的最优可达问题，从而提出带空间约束的功能性能统一验证算法；同时，开展互模拟等价的SDN控制器行为状态约简方法，研究其商模型结构及等价行为机理，证明商调度构造及约简一致性；最后，通过扩展现有的SDN北向接口编程语言，开展理论方法的实际应用与验证工具的开发。可见本项目为构建自主可控的SDN系统提供了新思路和新方法，为网络基础设施的健康发展提供了安全保障。

软件定义网络技术给网络基础设施带来了全面的革新，其集中控制的思想又面临新的安全挑战。本项目关注SDN控制器和编程接口的功能正确、性能可满足问题，采用形式化验证方法确保SDN控制系统的可信。首先开展SDN控制系统的验证需求，对网络元素进行抽象和建模，并描述功能性能特征；针对SDN控制器的可信态，研究功能性能统一验证的逻辑刻画和网络正确态可满足态的判定过程，从而构建统一的验证框架；研究基于交互式马尔科夫链的SDN控制器功能正确性判定，并转化为模型的最优可达问题，从而提出带空间约束的功能性能统一验证算法；开展互模拟等价的SDN控制器行为状态约简方法，研究其商模型结构及等价行为机理，证明商调度构造及约简一致性；通过扩展现有的SDN北向接口编程语言，开展理论方法的实际应用与验证工具的开发；最后通过大规模在线实训平台中的应用，验证了成果的有效性与应用前景。整个项目期间发表了多篇国内外重要研究论文与研究报告，并在在线实训教育应用场景中进行了初步验证。