【作者】 章志燮；

【导师】 赵保华；

【作者基本信息】 中国科学技术大学 ， 计算机软件与理论， 2009， 博士

【摘要】 随着通信协议的日益复杂,以及针对协议漏洞的攻击手段和技术的不断发展,因协议出错而引起的网络异常甚至崩溃现象层出不穷,危害了整个网络的信息安全。协议测试是协议工程的重要组成部分,是保证协议正常运行的关键技术。传统协议测试方法以一致性测试为代表,主要关注于协议的功能性,无法保证协议实现的安全性,因此需要进行协议安全测试的研究。协议存在的安全漏洞可以分为两类,一类是协议设计错误,例如导致使用者可以通过非法手段获取到不合法的权限。另一类是协议实现错误,由于通信协议是软件的一种,其实现过程不可避免的引入错误。本文中主要研究针对协议实现错误的安全测试理论和方法。现有针对协议安全测试的研究大都基于传统形式化模型如有限状态机等,采用随机或手动方法生成安全测试用例,通过观察待测协议实现在测试过程中是否崩溃来检测协议错误。现有方法中存在以下不足之处:首先,安全测试大都针对协议的数据流,而传统形式化模型描述协议数据流能力有限,不能满足安全测试的需求。其次,协议实现中可能存在的错误集合是无穷的,现有方法无法分析和评估测试的覆盖率。最后,协议崩溃只是协议错误可能导致的结果之一,现有方法更接近于鲁棒性测试,检错能力有限。本文中对基于构造类别代数的协议安全测试理论和方法进行了研究,主要工作集中在以下几个方面:1)提出了扩展的构造类别代数模型构造类别代数是代数规范的一个扩充,适用于描述协议的数据流。本文对构造类别代数的基本定义进行了扩展:首先增加了对协议控制流状态的描述,并将其同内部环境变量结合,给出了协议状态的定义。而后根据协议测试过程中报文的不同流向,重新定义了可控制和可观察操作,给出了可控制函数的一般形式。最后,对公理形式进行了扩展,增强其描述协议行为的能力。扩展后的模型具有同EFSM相同的控制流描述能力,但数据流描述能力更强,可用于协议安全测试的研究。2)提出了基于变异分析的协议安全测试方法变异分析是基于错误模型的测试方法,将其应用于基于构造类别代数的协议规范中,可以得到一系列规范的变异体,每个变异体对应于一类协议实现可能存在的错误。通过设计变异算子,可以限制协议实现中可能错误的规模,此外可以更有针对性构造测试用例,有效解决现有研究中存在的问题。本文对变异分析在构造类别代数中的应用进行了研究。首先设计了几类针对构造类别代数的变异算子,分析了应用算子以生成变异体的过程。而后分析了产生等价变异体的原因,给出了一个基于公理优先级动态递推,生成非等价变异体及其对应变异单元集合的算法。3)提出了协议安全测试序列生成方法本文中研究了基于变异体生成协议安全测试序列的方法,由于构造类别代数中同时描述了协议的控制流和数据流,因此在生成协议安全测试序列的过程中,需要同时考虑到控制流状态的可达性和数据流状态的可执行性。本文中分析了变异单元同安全测试序列的关系,先后给出了基于公理代入和逆向推导,以及基于可执行树正向推导安全测试序列生成方法。最后提出了一个结合主动和被动测试的协议安全测试序列生成方法,实验证明该方法可以有效减少协议测试序列的总长度,降低测试代价。4)设计并实现了分布式协议测试系统本文中设计并实现了一个分布式的协议安全测试系统,包括了一个主控中心和多个代理节点。系统基于底层支撑库的支持,将协议测试过程描述为对应的测试用例,并通过协调主控中心和分布式代理节点的行为,提供了对协议自动化测试的支持。该系统可用于协议的一致性测试和安全测试的研究中,大大提高测试用例开发和执行的效率。更多还原

【Abstract】 With the increasing complexity of communication protocols, as well as attacks against the protocol vulnerabilities and the continuous development of technology, network abnormal and crash caused by flaws occur frequently, endanger the whole network of information security. As an important part of protocol engineering, protocol testing is the key for a protocol to work properly. Traditional approaches of protocol testing like conformance testing focus more on the functionality of protocol implementation but not the security. Protocol security testing is gradually becoming one hotspot in protocol testing area.There are two types of protocol vulnerabilities. One is protocol design vulnerabilities, such as user can access unauthorized privacy through illegal path. Another is protocol implementation vulnerabilities, such as protocol is also a kind of software where flaws are inevitable in implementation. In this thesis the theory and methods of protocol security testing is studied, which mainly focus on protocol implementation vulnerabilities.Most existing methods of protocol security testing are based on traditional formal description models such as Finite State Machine. With security testing suites generated either manually or randomly, implementation flaws are checked by examining weather the IUT crashes during testing.The existing methods have the following deficiencies: first, security testing focuses on the part of protocol data flow, while traditional formal model have limited ability to describe protocol data flow and can not meet the requirement of security testing. Second, there could be infinite number of potential flaws in protocol implementation, while we can not evaluate the testing coverage of existing methods. Finally, protocol collapse is just one possible result caused by protocol flaws. The existing approaches are more like robustness testing which is poor at flaw detection.In this thesis, we discuss the theory and practice of security testing based on Constructed Type Algebra (CTA). We use CTA to describe protocol specifications, and then introduce a fault model based mutation analysis to generate mutants of specification. Security testing suites are constructed based on mutants.The work of this thesis includes:1、Extended CTA formal description model Construct Type Algebra is a formal description method based on algebraic specification, and is suitable to specify the data flow of protocols. In this thesis, we extend CTA to improve the ability of protocol description. Firstly, we add the description of control flow, and give the definition of protocol state based on control flow and environment variables. Secondly, we redefine the Point of Control and Observation description according to the packet directions. A generalized form of controllable function is given. Finally, the axiom is extended to improve the ability of describing protocol activities. Compared to EFSM, the extended CTA model has the same ability to descript the control flow of protocol, but better ability to descript the data flow part, which can be applied in the research of protocol security testing2、Theory and method of security testing based on mutation analysisMutation analysis is an efficient technique based on fault model. By applying mutation analysis, a series of mutants of protocol specification can be generated, each corresponding to one possible fault in protocol implementation. By the proper design of mutators, we can restrict the scale of possible fault set under test, and construct testing suites more pertinently. Thus protocol security testing based on mutation analysis can be an effective solution to the problems of existing methods.We discuss the application of mutation analysis in CTA. Several mutators for CTA are proposed, and the affect of their application to mutants are discussed. We analyzed the reason for equivalent mutant. Finally, a priority based method is proposed to generate non-equvalent and associated mutation item.3、Protocol security testing sequence generation algorithmIn this thesis, we study the protocol security testing suite generating method from mutatnt. Since both the data flow part and control flow part of protocol are considered in CTA, the testing suite should fulfill both the control flow reachability and data flow executability.We discuss the relation between mutation item and security testing sequence. We study the following three methods: First, a method based on axiom substitution and reverse deduction is discussed; then, a forward deduction method by creating testable tree is proposed; finally, a composition technique of active testing and passive testing is introduced to reduce the length of testing suites. Experiment results prove that the method can effectively reduce the testing cost.4、Design and implementation of a security testing systemAt last, we design and implement a distributed protocol security testing system in this thesis. This system consists of a server and several agent nodes. Automated Protocol testing is also supported. This system can improve the developing and executing efficiency of testing suite significantly, for protocol conformance testing and security testing.更多还原