Research On Protocol Security Testing Based On Constructed Type Algebra

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.