【作者】 陈伟琳；

【导师】 赵保华；

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

【摘要】 协议工程是一体化、形式化的协议开发过程,其研究内容包含协议的形式化描述,协议验证,协议实现和协议测试等。协议测试是协议工程中的一个重要内容。当前的网络环境日趋复杂,各种安全威胁事件层出不穷。作为计算机网络基础的通信协议,也面临着多种安全威胁。一些原来在封闭环境中使用的协议被逐渐用作公开协议,这也增加了协议的安全风险。传统的协议一致性测试是协议测试的基础,其目的是检查待测协议实现的行为与协议规范是否一致。但它作为一种传统的功能性测试,并不能完全保证协议实现的安全。因此协议安全测试正逐渐成为协议测试领域中的一个新热点。本文针对协议安全性测试进行了研究,主要讨论了协议攻击测试以及基于构造类别代数的安全变异测试两个方面。在协议安全性的评价过程中,这两个方面是相辅相成的。协议攻击测试本质上是一种针对网络设备上运行的协议实现的渗透测试,是检验网络设备对已知协议攻击的抵御能力的测试。而基于构造类别代数的安全变异测试则通过针对协议的形式化描述设计变异算子,作用于一致性公式集来产生安全测试例集,以试图覆盖未知的协议错误和安全漏洞。本文的研究工作主要集中在以下几个方面:1)协议攻击测试模型和方法本文对协议攻击测试进行了系统性、整体性的研究,对测试的每一阶段都提出了解决方案。首先提出了面向测试的协议攻击描述模型,用于描述协议攻击的原理、发生位置、影响、彼此关联等多项属性,作为后续执行算法和安全性量化评价的基础。然后针对分布式协议攻击测试框架实际部署中的测试者分布问题,提出一个基于网络路径信息的测试者选择算法,可以均衡测试流量和提高测试结果的可靠性。考虑了攻击测试例之间的序列相关性和因果关系的影响,提出基于攻击测试例关联性的优化测试执行算法,通过动态执行减少测试中的重复操作,提高测试效率。最后提出了基于改进的RBD and Criticality模型的安全性度量方法,根据协议攻击测试的结果集合对被测设备进行安全性量化评价。2)基于构造类别代数的安全变异测试方法传统的协议安全测试方法大多是单纯地对协议PDUs进行变异或随机扰动,并不涉及协议形式化模型技术。针对这种情况,本文提出了基于构造类别代数的安全变异测试方法。该方法兼顾了协议安全漏洞的总结和构造类别代数的结构特点,通过对基于构造类别代数形式化描述得到的一致性测试公式集施加安全变异以产生安全测试例集。该方法具有发现潜在安全问题的能力,并能充分利用一致性测试的中间成果,有利于安全测试过程和一致性测试过程的有机结合。3)设计和实现了一个协议安全测试系统本文还设计和实现了一个协议安全测试系统。该系统是分布式的,能灵活的适应多种网络环境和多种测试要求,既适用于协议攻击测试,也能用于安全变异测试。基于该系统能完成测试例开发、调试、执行、测试结果回收和分析的整个安全测试流程。更多还原

【Abstract】 Protocol Engineering is an integrated and formalized process of protocol development, including protocol formal description, protocol verification, protocol implementation and protocol testing based on formal description. Protocol testing is an important part of protocol engineering.These days the network becomes more and more complicated, and security threats and exploits emerge in endlessly. Communication protocols, acting as the foundation of the modern computer network, are also faced with multiple kinds of security threats. The protocol conformance testing, which is the basis of protocol testing, generally aims at checking whether the implementation of a protocol conforms to its specification. However, as a traditional functional testing method,it can’t ensure the implementation’s security. Protocol security testing is gradually becoming one hotspot in protocol testing area.In this paper, protocol security testing is discussed, mainly including protocol attack testing and protocol security mutation testing based on Constructed Type Algebra. Protocol attack testing is in nature a penetration testing method on protocol implementations running on network equipment, which verifies the equipment’s resistance ability against known protocol attacks. On the other hand, Construct Type Algebra (CIA) based protocol security mutation testing targets the disclosure of unknown faults and security problems. It first designs imitators based on the formal description model, then uses these mutators on conformance formulas to obtain security testing cases. These security testing cases are then used to verify or evaluate the protocol implementation’s security.The work of this paper includes:1. Protocol attack testing model and methodThis paper studies protocol attack testing systematically and holistically, and proposes solutions for each testing phrases.Firstly an protocol attack description model in the view of testing is proposed. This model has the ability of describing multiple attributes of a protocol attack detailedly, including its principle, location, influence, relationship with other attacks, etc. It also helps in attack test cases generation, selection and execution.Secondly, a uniform protocol attack testing framework is brought forward. A network path information based tester selection algorithm is proposed, in order to solve the tester distributing problem in the framework’s practical deployment . This algorithm helps in averaging testing data flows and improve test result’s reliability.Thirdly, the sequences relationships and causalities between different test cases are discussed. An optimized test execution algorithm is proposed base on these relevancies. It decreases duplicated operations to improve test efficiency.At last a security measurement method based on extended RBD and Criticality model is proposed, which draws quantitive security evaluation of the equipment under testing out of the test results.2. Security mutation testing based on CTAConstruct Type Algebra is a formal description method based on algebraic specification, and is suitable for specifying the data parts and related processes of a protocol. Mutation analysis is a common technique in current security testing area. In this paper, mutation analysis is integrated with CTA specification, while the security vulnerabilities summarized by the above description method and the structural characteristic of CTA are both considered. All these result in a new protocol security testing method which bases on conformance formulas generated out from the conformance test generation algorithm. This method can generate security test cases through performing security related mutations on the formulas. This method has the ability of revealing potential security threats, and helps in evaluating the protocol’s security. In addition, it can make full use of conformance testing’s intermediate achievements, and organically integrates security testing with normal conformance testing procedure.3. Design and implementation of a security testing systemAt last, a protocol security testing system is designed and implemented in this paper. This system has a distributed architecture and therefore is flexible to multiple environments and different test requirements, and also has considerable expansibility. It is suitable for protocol attack testing, and also can be used in security mutation testing. In this system, the whole security testing procedure can be implemented ,including test cases development and debug, test execution and data collection, results analysis and report generation.更多还原