面向新一代互联网协议的基于模型检测的协议安全性测试研究

Protocol security testing aims to ensure the security of communication protocols, and can be used to detect vulnerabilities of protocol specifications and implementations, or to study the resistance ability of protocols against the well-known network attacks or malicious injections. Protocols in next generation Internet have more security requirements, so it is very important to study protocol security testing in the context of next generation Internet protocol. Model checking is a formal automatic verification technique, and protocol testing based on model checking is becoming a promising research direction. This project will study network protocol security testing based on model checking, formalizing and automating the whole testing process. In this project we will (1) study the generic framework of network protocol security testing based on model checking; (2) study protocol modeling methdology for model checking based security testing, by integrating protocol behavior description, network topology model and attacking model; (3) study the transformation from model checking sequences to abstract test cases, and generate distributed test cases by using standard testing language TTCN-3; (4) apply the method in real-life protocol security testing of next generation Internet protocol in order to demonstrate the correctness and effectiveness of the proposed theory and method.

协议安全性测试的目的在于发掘协议实现潜在的缺陷或漏洞，考察协议实现对已知攻击的防御能力，尽可能发现协议的安全问题。新一代互联网对于协议的安全性要求更高，在新一代互联网协议研究的大背景下研究协议安全性测试具有重要的意义。模型检测是一种形式化的模型自动验证技术，基于模型检测的协议测试技术是很有前景的研究方向。本项目基于模型检测技术研究网络协议安全性测试，实现了整个测试过程的形式化和自动化。主要研究内容包括：(1) 研究基于模型检测的网络协议安全性测试的一般性框架；(2) 面向模型检测和安全性测试研究网络协议建模，集成协议行为描述、网络拓扑模型和攻击者模型，得到可用于模型检测的模型；(3) 研究模型检测序列到抽象测试例的转换方法，采用标准测试描述语言TTCN-3作为测试例描述语言，生成分布式TTCN-3测试例；(4) 对新一代互联网协议进行安全性测试，通过实例研究进一步证明理论方法的正确有效性。

协议安全性测试的目的在于发掘协议实现潜在的缺陷或漏洞，考察协议实现对已知攻击的防御能力。新一代互联网对于协议的安全性要求更高，在新一代互联网协议研究的大背景下研究协议测试及安全性测试具有重要的意义。模型检测是一种形式化的模型自动验证技术，基于模型检测的协议测试技术是很有前景的研究方向。本项目面向新一代互联网协议研究网络协议测试及安全性测试，主要研究内容和研究成果包括：第一，提出了面向新一代互联网协议的网络协议测试及安全性测试的一般性框架：面向模型检测和安全性测试研究网络协议建模，集成协议行为描述、网络拓扑模型和攻击者模型，得到可用于模型检测的模型；基于协议形式化模型，可以直接采用测试生成方法得到相应的测试序列，也可以结合安全性属性的形式化模型，通过模型检测得到违反安全性属性的反例；进一步可将这些反例或序列转化为分布式TTCN-3测试例，并在TTCN-3测试系统上进行测试，基本实现了整个测试过程的形式化和自动化。第二，建立了并行多组件状态机的网络协议建模框架，提出了三种不同的扩展并行多组件状态机模型及其测试生成方法：(1) 为描述并行组件间采用共享数据通信的情况，提出了读取外部变量的并行扩展有限状态机模型，基于该模型分别提出了基于定义使用路径的测试生成方法和基于可达图的层次化测试生成方法,并应用于SAVI协议测试；(2) 为描述单向消息传递和存在共享变量读写的多级流水线结构，提出了流水线扩展有限状态机模型及其测试生成方法，并应用于SDN交换机测试；(3) 将消息传递与网络拓扑结合，初步提出了信息表扩展有限状态机模型及其测试生成方法，并应用于SDN应用测试。这些模型对网络协议测试模型进行了扩展，可适用于多种具有并行多组件的网络协议，面向新一代互联网协议的需求深化和发展了网络协议测试模型和理论。第三，提出了域间不相交多路径路由机制DIMR，建立了DIMR的网络系统形式化模型，并对其收敛性进行了形式化分析，证明了其稳定性；这一工作将形式化方法应用于网络协议分析中，拓展了网络协议形式化模型的应用领域。第四，作为测试方法的有益补充，进一步基于大数据技术研究了网络流量安全性异常检测，提出了新的流量异常检测指标可调节分段熵，并基于大数据平台Hadoop实现了一个基于信息熵的网络流量异常检测系统。项目执行期间共发表SCI/EI论文16篇，申请国家发明专利4项。