基于构造类别代数的协议安全测试研究
|
摘要
随着通信协议的日益复杂,以及针对协议漏洞的攻击手段和技术的不断发展,因协议出错而引起的网络异常甚至崩溃现象层出不穷,危害了整个网络的信息安全。协议测试是协议工程的重要组成部分,是保证协议正常运行的关键技术。传统协议测试方法以一致性测试为代表,主要关注于协议的功能性,无法保证协议实现的安全性,因此需要进行协议安全测试的研究。
协议存在的安全漏洞可以分为两类,一类是协议设计错误,例如导致使用者可以通过非法手段获取到不合法的权限。另一类是协议实现错误,由于通信协议是软件的一种,其实现过程不可避免的引入错误。本文中主要研究针对协议实现错误的安全测试理论和方法。
现有针对协议安全测试的研究大都基于传统形式化模型如有限状态机等,采用随机或手动方法生成安全测试用例,通过观察待测协议实现在测试过程中是否崩溃来检测协议错误。现有方法中存在以下不足之处:首先,安全测试大都针对协议的数据流,而传统形式化模型描述协议数据流能力有限,不能满足安全测试的需求。其次,协议实现中可能存在的错误集合是无穷的,现有方法无法分析和评估测试的覆盖率。最后,协议崩溃只是协议错误可能导致的结果之一,现有方法更接近于鲁棒性测试,检错能力有限。
本文中对基于构造类别代数的协议安全测试理论和方法进行了研究,主要工作集中在以下几个方面:
1)提出了扩展的构造类别代数模型
构造类别代数是代数规范的一个扩充,适用于描述协议的数据流。本文对构造类别代数的基本定义进行了扩展:首先增加了对协议控制流状态的描述,并将其同内部环境变量结合,给出了协议状态的定义。而后根据协议测试过程中报文的不同流向,重新定义了可控制和可观察操作,给出了可控制函数的一般形式。最后,对公理形式进行了扩展,增强其描述协议行为的能力。扩展后的模型具有同EFSM相同的控制流描述能力,但数据流描述能力更强,可用于协议安全测试的研究。
2)提出了基于变异分析的协议安全测试方法
变异分析是基于错误模型的测试方法,将其应用于基于构造类别代数的协议规范中,可以得到一系列规范的变异体,每个变异体对应于一类协议实现可能存在的错误。通过设计变异算子,可以限制协议实现中可能错误的规模,此外可以更有针对性构造测试用例,有效解决现有研究中存在的问题。
本文对变异分析在构造类别代数中的应用进行了研究。首先设计了几类针对构造类别代数的变异算子,分析了应用算子以生成变异体的过程。而后分析了产生等价变异体的原因,给出了一个基于公理优先级动态递推,生成非等价变异体及其对应变异单元集合的算法。
3)提出了协议安全测试序列生成方法
本文中研究了基于变异体生成协议安全测试序列的方法,由于构造类别代数中同时描述了协议的控制流和数据流,因此在生成协议安全测试序列的过程中,需要同时考虑到控制流状态的可达性和数据流状态的可执行性。
本文中分析了变异单元同安全测试序列的关系,先后给出了基于公理代入和逆向推导,以及基于可执行树正向推导安全测试序列生成方法。最后提出了一个结合主动和被动测试的协议安全测试序列生成方法,实验证明该方法可以有效减少协议测试序列的总长度,降低测试代价。
4)设计并实现了分布式协议测试系统
本文中设计并实现了一个分布式的协议安全测试系统,包括了一个主控中心和多个代理节点。系统基于底层支撑库的支持,将协议测试过程描述为对应的测试用例,并通过协调主控中心和分布式代理节点的行为,提供了对协议自动化测试的支持。该系统可用于协议的一致性测试和安全测试的研究中,大大提高测试用例开发和执行的效率。
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 testing
2、Theory and method of security testing based on mutation analysis
Mutation 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 algorithm
In 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 system
At 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.
协议存在的安全漏洞可以分为两类,一类是协议设计错误,例如导致使用者可以通过非法手段获取到不合法的权限。另一类是协议实现错误,由于通信协议是软件的一种,其实现过程不可避免的引入错误。本文中主要研究针对协议实现错误的安全测试理论和方法。
现有针对协议安全测试的研究大都基于传统形式化模型如有限状态机等,采用随机或手动方法生成安全测试用例,通过观察待测协议实现在测试过程中是否崩溃来检测协议错误。现有方法中存在以下不足之处:首先,安全测试大都针对协议的数据流,而传统形式化模型描述协议数据流能力有限,不能满足安全测试的需求。其次,协议实现中可能存在的错误集合是无穷的,现有方法无法分析和评估测试的覆盖率。最后,协议崩溃只是协议错误可能导致的结果之一,现有方法更接近于鲁棒性测试,检错能力有限。
本文中对基于构造类别代数的协议安全测试理论和方法进行了研究,主要工作集中在以下几个方面:
1)提出了扩展的构造类别代数模型
构造类别代数是代数规范的一个扩充,适用于描述协议的数据流。本文对构造类别代数的基本定义进行了扩展:首先增加了对协议控制流状态的描述,并将其同内部环境变量结合,给出了协议状态的定义。而后根据协议测试过程中报文的不同流向,重新定义了可控制和可观察操作,给出了可控制函数的一般形式。最后,对公理形式进行了扩展,增强其描述协议行为的能力。扩展后的模型具有同EFSM相同的控制流描述能力,但数据流描述能力更强,可用于协议安全测试的研究。
2)提出了基于变异分析的协议安全测试方法
变异分析是基于错误模型的测试方法,将其应用于基于构造类别代数的协议规范中,可以得到一系列规范的变异体,每个变异体对应于一类协议实现可能存在的错误。通过设计变异算子,可以限制协议实现中可能错误的规模,此外可以更有针对性构造测试用例,有效解决现有研究中存在的问题。
本文对变异分析在构造类别代数中的应用进行了研究。首先设计了几类针对构造类别代数的变异算子,分析了应用算子以生成变异体的过程。而后分析了产生等价变异体的原因,给出了一个基于公理优先级动态递推,生成非等价变异体及其对应变异单元集合的算法。
3)提出了协议安全测试序列生成方法
本文中研究了基于变异体生成协议安全测试序列的方法,由于构造类别代数中同时描述了协议的控制流和数据流,因此在生成协议安全测试序列的过程中,需要同时考虑到控制流状态的可达性和数据流状态的可执行性。
本文中分析了变异单元同安全测试序列的关系,先后给出了基于公理代入和逆向推导,以及基于可执行树正向推导安全测试序列生成方法。最后提出了一个结合主动和被动测试的协议安全测试序列生成方法,实验证明该方法可以有效减少协议测试序列的总长度,降低测试代价。
4)设计并实现了分布式协议测试系统
本文中设计并实现了一个分布式的协议安全测试系统,包括了一个主控中心和多个代理节点。系统基于底层支撑库的支持,将协议测试过程描述为对应的测试用例,并通过协调主控中心和分布式代理节点的行为,提供了对协议自动化测试的支持。该系统可用于协议的一致性测试和安全测试的研究中,大大提高测试用例开发和执行的效率。
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 testing
2、Theory and method of security testing based on mutation analysis
Mutation 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 algorithm
In 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 system
At 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.
引文
Welch B B.2001.Tcl/Tk组合教程[M].王道义等译.第2版.电子工业出版社.
Hoare C A.1988.通讯顺序进程[M].周巢尘译.北京大学出版社.
陈伟琳,周颢,赵保华.2008a.利用构造类别代数的协议安全测试方法[J].西安交通大学学报:12:1481-1485.
陈伟琳. 2008b.协议安全测试理论和方法的研究[D].博士论文,合肥:中国科学技术大学.
龚正虎.1993.计算机网络协议工程[M].国防科技大学出版社.
龚正虎. 1995.利用CCS的协议描述和验证技术的研究[J].计算机研究与发展: 32(3):61-65.
郭雄辉,赵保华,周颢等.2003.基于构造类别代数的数据流和控制流相结合的协议测试[J].北京邮电大学学报:26(增刊):7-11.
刘政,赵保华,屈玉贵.2004a.一种描述安全协议的形式化规范语言[J].小型微型计算机系统:25(7):1246-1249.
刘政,赵保华,屈玉贵.2004b.使用构造类别代数描述和验证密码协议[J].通信学报:25(3):91-96.
刘政. 2004c.基于形式化描述的协议一致性测试方法的研究[D].博士论文,合肥:中国科学技术大学.
孙宇霖,屈玉贵,赵保华.2001.一种通信协议测试序列生成的新方法[J].通信学报: 22(6):122-127.
孙宇霖. 2002.基于构造类别代数协议测试理论的研究[D].博士论文,合肥:中国科学技术大学.
周晓煜,屈玉贵,赵保华.2002.基于构造类别代数的变异分析[J].电子学报: 30(12A):2155-2157.
周晓煜. 2004.基于形式化描述的协议一致性测试方法的研究[D].博士论文,合肥:中国科学技术大学.
Aggarwal S,et al.1988.Protocol Specification,Testing, and Verification (VIII)[S]. Amsterdam: North-Holland.
Agrawal H, DeMillo R A,et al.1989.Design of Mutant Operators for the C Programming Language[R]. Technical report SERC-TR-41-P, Software Engineering Research Center, Purdue University
Belina F, Hogrefe D.1989. The CCITT-Specification and Description Language SDL[J]. Computer Networks and ISDN Systems: 16(3): 311-341.
Blyth D,Boldyreff C, Ruggles C et al..1990.The case for formal methods in standards[J]. IEEE Software:7(5):65-67.
Bourhfir C, Abouilhamid E, Dssouli R et al. 2001. A Test Case Generation Approach for Conformance Testing of SDL Systems [J]. Computer Communications: 24(3-4): 319-333.
Budd T A, Gopal A. 1985. Program Testing by Specification Mutation[J]. Computer Languages:10(1): 63-73
Cheung T.-y. 1996. Petri nets for protocol engineering[J]. Computer Communications:1 9:1250-1257.
Chow T.S.1978. Testing Software Designs Modeled by Finite-State Machines[J]. IEEE Transactions on Software Engineering:4(3): 178-187.
Dave Aitel. 2002. The Advantages of Block-Based Protocol Analysis for Security Testing[EB/OL]. http://www.babilonics.com/files/advantages_of_block_based_analysis.pdf
David Lee, Netravali A.N., Sabnani K.K. etc. 1997. Passive Testing and Applications to Network Management[C]. International Conference on Network Protocols: 113 -122.
David Lee, Dongluo Chen, Ruibing Hao, etc. 2002. A Formal Approach for Passive Testing of Protocol Data Portions[C]. Proceeding of the 10th IEEE International Conference on Network Protocols(ICNP'02).
Dean T, Knigth S. 2004. Applying Software Transformation Techniques to Security Testing[C]. International Workshop on Software Evolution and Transformation:49-52.
Eugene H, Spafford. 1990. Extending Mutation Testing to find Environmental bugs[J]. Software practice and Principle, 20(2):181-189.
Fabbri S. C., Delamaro M E, et al. 1994.Mutation Analysis Testing for Finite State Machine [M]. Proceedings of 5th International Symposium on Software Reliability Engineering: 220-229.
Fujiwara S, G von Bochmann, Khendek F, et al. 1991. Test Selection Based on Finite State Models [J]. IEEE Transactions on Software Engineering: 17(6): 591-603.
Gonenc G. 1970. A Method for the Design of Fault Detection Experiments[J]. IEEE Transactions on Computer:19(6):551-558.
Green P E. 1986. Protocol Conversion [J]. IEEE Transactions on Communications:34(3):2 57-268.
Hamlet R G. 1977. Testing programs with the aid of a compiler[J]. IEEE Transactions on Software Engineering: 3(4):279-290.
Henniger O, Neumann P. 1995. Test Case Generation Based on Formal Specification in Estelle[C]. Proceedings of WFCS’95, IEEE International Workshop on Factory Communication Systems: 135-141.
Hinchey M G. 1993. Formal methods for system specification[J]. IEEE Potentials, 12 (3):50-52.
ISO/IEC 8807: Information Processing Systems– Open Systems Interconnection– LOTOS–A Formal Description Technique Based on the Temporal Ordering of Observational Behavior[S]. 1989.
ISO/IEC 9074: Information Processing Systems - Open Systems Interconnection–ESTELLE– A Formal Description Technique Based on an Extended State Transition Model[S].1989
ITU-T.1996.Recommendation Z.100: Specification and Description Languages SDL[S]. Jeasen K.1981. Colored Petri Nets and the Invariant Method[J].Tehor Comput Sci:317-336.
Jonsson B, et al .1991. Protocol Specification, Testing, and Verification (XI)[S]. Amsterdam: North-Holland.
Li Hua, Ye Xin Ming. 1998. Generation Executable Test Sequences Based on Petri-net for Combined Control and Data Flow of Communication Protocol[C]. Proceedings of ICCT ' 98, Intenrational Conference on Communication Technology, 2:1-5.
Linn R J, et al. 1992.Protocol Specification, Testing, and Verification(X III)[S].Amsterdam: North-Holland.
Maloku N, Pucko M F. 2001. SDL-based Feasible Test Generation for Communication Protocols[C]. EUROCON’2001, International Conference on Trends in Communications:2: 536-539.
Marquis S,Dean T H,Knight S.2005. SCL-a language for security testing of network applications[C]. Proceedings of the 2005 conference of the Centre for Advanced Studies on Collaborative research:155-164
Marshall I. 1994. Specification and synthesis in interval temporal logic[C]. IEEE Colloquium on Structured Methods for Hardware System Design: 4/1-4/3.
Miller, R.E. 1998. Passive testing of networks using a CFSM specification. Proceedings of the IEEE International Performance, Computing and Communications Conference: 111 -116.
Milner R. 1980.Calculus of Communication Systems[C], volume 94 of Lecture Notes in Computer Science, Springer-Verlag, Heidelberg, Germany.
Naito S, Tsunoyama M. 1981. Fault Detection for Sequential Machines by Transition Tours[C]. Proceedings of IEEE Fault Tolerant Computing Conference: 238-243.
Oded Tal, Scott Knight. 2004. Syntax-based Vulnerability Testing of Frame-based Network Protocols. 2nd Annual Conference on Privacy, Security and Trust.
Offutt A J, Voas J, et al.1996.Mutation Operators for Ada[R]. Tech. Report ISSE-TR-96-09,Department of Information and Software Systems Engineering, George Mason University.
Offutt A J, Xiong Yiwei, Liu Shaoying.1999.Criteria for Generating Specification-Based Tests[C]. ICECCS’99, Fifth IEEE International Conference on Engineering of Complex Computer Systems:119-129.
Pang Qixiang, Cheng Shiduan, Jin Yuehui. 1996. Protocol Conformance Test Suite Generation[C]. Proceedings of ICCT’96, International Conference on Communication Technology:1: 218-222.
Patrice Godefroid, Michael Y, Levin. 2007. Automated Whitebox Fuzz Testing[EB/OL]. http://research.microsoft.com/users/pg/public_psfiles/SAGE-external-v1.pdf. Microsoft Technical Report.
PROTOS. 2007. PROTOS-Security Testing of Protocol Implementations[EB/OL]. http://www.ee.oulu.fi/research/ouspg/protos/index.html.
Rauli Kaksonen. 2001. A Functional Method for Assessing Protocol Implementation Security. VTT Technical Research Centre of Finland. ESPO 2001.
Rudin H. 1988. Protocol engineering: a Critical assessment. Protocol Specification, Testing and Verification (VIII) [S].Amsterdam: North-Holland.
Sabnani K, Dahbura A. 1988.A Protocol Test Generation Procedure[J]. Computer Networks and ISDN Systems: 15(2):285-297.
Schwartz Richard L, Melliar-Smith P. M. 1982. From state machines to temporal logic: specification methods for protocol standards[J]. IEEE Transactions on Communications: 30(12): 2486-2496.
S. do Rocio Senger de Souza, Maldonado J C, S. Camargo Pinto Ferraz Fabbri, and W.Lopes de Souza. 2000. Mutation Testing Applied to Estelle Specifications[C]. Proceedings of the 33rd Annual Hawaii International Conference on System Sciences: 2940-2949.
Su Tong, Chen Junliang, Cheng Shiduan. 1992. Test Sequence Generation for Protocol Conformance Testing[C]. Singapore ICCS/ISITA’92:1:204-208.
Turcotte Y,Tal O ,Knight S et al. 2004. Security vulnerabilities assessment of the X.509 protocol by syntax-based testing[C].Military Communications Conference: 3:1572-1578
Ural H, H. van der Schoot. 1995. Data flow oriented test selection for LOTOS[J]. Computer Networks and ISDN Systems:27(7):1111-1136.
Ural H, Saleh K, Willianms A. 2000. Test Generation Based on Control and Data Dependencies within System Specifications in SDL[J]. Computer Communications:23(7): 609-627.
Wang Chang-Jia, Liu Ming T. 1992. Axiomatic test sequence generation for extended finitestate machines[C]. Proceedings of the 12th International Conference on Distributed Computing Systems:252-259.
William H, Allen, Chin Dou. 2006. A Model-based Approach to the Security Testing of Network Protocol Implementations[C]. Local Computer Networks, Proceedings 2006 31st IEEE Conference:1008-1015
Xiao Shu, Deng Lijun, Li Sheng et al. 2003. PDUS-Integrated TCPIP protocol software testing for vulnerability detection[C]. Proceedings of the 2003 International Conference on Computer Networks and Mobile Computing (ICCNMC’03).
Yao TinYu , Gouda M. 1982. Deadlock detection for a class of communicating finite stat e machines[J]. IEEE Transactions on Communications: 30 (12):2514-2518.
Zhang Songtao, Dean T, Knight S. 2006. A Lightweight Approach to State Based Security Testing[C]. CASCON’06:341-344.
Zhang Songtao, Dean T, Kngiht S. 2007. Lightweight State Based Mutation Testing for Security[C]. TAICPART-MUTATION '07(00):223-232.
Hoare C A.1988.通讯顺序进程[M].周巢尘译.北京大学出版社.
陈伟琳,周颢,赵保华.2008a.利用构造类别代数的协议安全测试方法[J].西安交通大学学报:12:1481-1485.
陈伟琳. 2008b.协议安全测试理论和方法的研究[D].博士论文,合肥:中国科学技术大学.
龚正虎.1993.计算机网络协议工程[M].国防科技大学出版社.
龚正虎. 1995.利用CCS的协议描述和验证技术的研究[J].计算机研究与发展: 32(3):61-65.
郭雄辉,赵保华,周颢等.2003.基于构造类别代数的数据流和控制流相结合的协议测试[J].北京邮电大学学报:26(增刊):7-11.
刘政,赵保华,屈玉贵.2004a.一种描述安全协议的形式化规范语言[J].小型微型计算机系统:25(7):1246-1249.
刘政,赵保华,屈玉贵.2004b.使用构造类别代数描述和验证密码协议[J].通信学报:25(3):91-96.
刘政. 2004c.基于形式化描述的协议一致性测试方法的研究[D].博士论文,合肥:中国科学技术大学.
孙宇霖,屈玉贵,赵保华.2001.一种通信协议测试序列生成的新方法[J].通信学报: 22(6):122-127.
孙宇霖. 2002.基于构造类别代数协议测试理论的研究[D].博士论文,合肥:中国科学技术大学.
周晓煜,屈玉贵,赵保华.2002.基于构造类别代数的变异分析[J].电子学报: 30(12A):2155-2157.
周晓煜. 2004.基于形式化描述的协议一致性测试方法的研究[D].博士论文,合肥:中国科学技术大学.
Aggarwal S,et al.1988.Protocol Specification,Testing, and Verification (VIII)[S]. Amsterdam: North-Holland.
Agrawal H, DeMillo R A,et al.1989.Design of Mutant Operators for the C Programming Language[R]. Technical report SERC-TR-41-P, Software Engineering Research Center, Purdue University
Belina F, Hogrefe D.1989. The CCITT-Specification and Description Language SDL[J]. Computer Networks and ISDN Systems: 16(3): 311-341.
Blyth D,Boldyreff C, Ruggles C et al..1990.The case for formal methods in standards[J]. IEEE Software:7(5):65-67.
Bourhfir C, Abouilhamid E, Dssouli R et al. 2001. A Test Case Generation Approach for Conformance Testing of SDL Systems [J]. Computer Communications: 24(3-4): 319-333.
Budd T A, Gopal A. 1985. Program Testing by Specification Mutation[J]. Computer Languages:10(1): 63-73
Cheung T.-y. 1996. Petri nets for protocol engineering[J]. Computer Communications:1 9:1250-1257.
Chow T.S.1978. Testing Software Designs Modeled by Finite-State Machines[J]. IEEE Transactions on Software Engineering:4(3): 178-187.
Dave Aitel. 2002. The Advantages of Block-Based Protocol Analysis for Security Testing[EB/OL]. http://www.babilonics.com/files/advantages_of_block_based_analysis.pdf
David Lee, Netravali A.N., Sabnani K.K. etc. 1997. Passive Testing and Applications to Network Management[C]. International Conference on Network Protocols: 113 -122.
David Lee, Dongluo Chen, Ruibing Hao, etc. 2002. A Formal Approach for Passive Testing of Protocol Data Portions[C]. Proceeding of the 10th IEEE International Conference on Network Protocols(ICNP'02).
Dean T, Knigth S. 2004. Applying Software Transformation Techniques to Security Testing[C]. International Workshop on Software Evolution and Transformation:49-52.
Eugene H, Spafford. 1990. Extending Mutation Testing to find Environmental bugs[J]. Software practice and Principle, 20(2):181-189.
Fabbri S. C., Delamaro M E, et al. 1994.Mutation Analysis Testing for Finite State Machine [M]. Proceedings of 5th International Symposium on Software Reliability Engineering: 220-229.
Fujiwara S, G von Bochmann, Khendek F, et al. 1991. Test Selection Based on Finite State Models [J]. IEEE Transactions on Software Engineering: 17(6): 591-603.
Gonenc G. 1970. A Method for the Design of Fault Detection Experiments[J]. IEEE Transactions on Computer:19(6):551-558.
Green P E. 1986. Protocol Conversion [J]. IEEE Transactions on Communications:34(3):2 57-268.
Hamlet R G. 1977. Testing programs with the aid of a compiler[J]. IEEE Transactions on Software Engineering: 3(4):279-290.
Henniger O, Neumann P. 1995. Test Case Generation Based on Formal Specification in Estelle[C]. Proceedings of WFCS’95, IEEE International Workshop on Factory Communication Systems: 135-141.
Hinchey M G. 1993. Formal methods for system specification[J]. IEEE Potentials, 12 (3):50-52.
ISO/IEC 8807: Information Processing Systems– Open Systems Interconnection– LOTOS–A Formal Description Technique Based on the Temporal Ordering of Observational Behavior[S]. 1989.
ISO/IEC 9074: Information Processing Systems - Open Systems Interconnection–ESTELLE– A Formal Description Technique Based on an Extended State Transition Model[S].1989
ITU-T.1996.Recommendation Z.100: Specification and Description Languages SDL[S]. Jeasen K.1981. Colored Petri Nets and the Invariant Method[J].Tehor Comput Sci:317-336.
Jonsson B, et al .1991. Protocol Specification, Testing, and Verification (XI)[S]. Amsterdam: North-Holland.
Li Hua, Ye Xin Ming. 1998. Generation Executable Test Sequences Based on Petri-net for Combined Control and Data Flow of Communication Protocol[C]. Proceedings of ICCT ' 98, Intenrational Conference on Communication Technology, 2:1-5.
Linn R J, et al. 1992.Protocol Specification, Testing, and Verification(X III)[S].Amsterdam: North-Holland.
Maloku N, Pucko M F. 2001. SDL-based Feasible Test Generation for Communication Protocols[C]. EUROCON’2001, International Conference on Trends in Communications:2: 536-539.
Marquis S,Dean T H,Knight S.2005. SCL-a language for security testing of network applications[C]. Proceedings of the 2005 conference of the Centre for Advanced Studies on Collaborative research:155-164
Marshall I. 1994. Specification and synthesis in interval temporal logic[C]. IEEE Colloquium on Structured Methods for Hardware System Design: 4/1-4/3.
Miller, R.E. 1998. Passive testing of networks using a CFSM specification. Proceedings of the IEEE International Performance, Computing and Communications Conference: 111 -116.
Milner R. 1980.Calculus of Communication Systems[C], volume 94 of Lecture Notes in Computer Science, Springer-Verlag, Heidelberg, Germany.
Naito S, Tsunoyama M. 1981. Fault Detection for Sequential Machines by Transition Tours[C]. Proceedings of IEEE Fault Tolerant Computing Conference: 238-243.
Oded Tal, Scott Knight. 2004. Syntax-based Vulnerability Testing of Frame-based Network Protocols. 2nd Annual Conference on Privacy, Security and Trust.
Offutt A J, Voas J, et al.1996.Mutation Operators for Ada[R]. Tech. Report ISSE-TR-96-09,Department of Information and Software Systems Engineering, George Mason University.
Offutt A J, Xiong Yiwei, Liu Shaoying.1999.Criteria for Generating Specification-Based Tests[C]. ICECCS’99, Fifth IEEE International Conference on Engineering of Complex Computer Systems:119-129.
Pang Qixiang, Cheng Shiduan, Jin Yuehui. 1996. Protocol Conformance Test Suite Generation[C]. Proceedings of ICCT’96, International Conference on Communication Technology:1: 218-222.
Patrice Godefroid, Michael Y, Levin. 2007. Automated Whitebox Fuzz Testing[EB/OL]. http://research.microsoft.com/users/pg/public_psfiles/SAGE-external-v1.pdf. Microsoft Technical Report.
PROTOS. 2007. PROTOS-Security Testing of Protocol Implementations[EB/OL]. http://www.ee.oulu.fi/research/ouspg/protos/index.html.
Rauli Kaksonen. 2001. A Functional Method for Assessing Protocol Implementation Security. VTT Technical Research Centre of Finland. ESPO 2001.
Rudin H. 1988. Protocol engineering: a Critical assessment. Protocol Specification, Testing and Verification (VIII) [S].Amsterdam: North-Holland.
Sabnani K, Dahbura A. 1988.A Protocol Test Generation Procedure[J]. Computer Networks and ISDN Systems: 15(2):285-297.
Schwartz Richard L, Melliar-Smith P. M. 1982. From state machines to temporal logic: specification methods for protocol standards[J]. IEEE Transactions on Communications: 30(12): 2486-2496.
S. do Rocio Senger de Souza, Maldonado J C, S. Camargo Pinto Ferraz Fabbri, and W.Lopes de Souza. 2000. Mutation Testing Applied to Estelle Specifications[C]. Proceedings of the 33rd Annual Hawaii International Conference on System Sciences: 2940-2949.
Su Tong, Chen Junliang, Cheng Shiduan. 1992. Test Sequence Generation for Protocol Conformance Testing[C]. Singapore ICCS/ISITA’92:1:204-208.
Turcotte Y,Tal O ,Knight S et al. 2004. Security vulnerabilities assessment of the X.509 protocol by syntax-based testing[C].Military Communications Conference: 3:1572-1578
Ural H, H. van der Schoot. 1995. Data flow oriented test selection for LOTOS[J]. Computer Networks and ISDN Systems:27(7):1111-1136.
Ural H, Saleh K, Willianms A. 2000. Test Generation Based on Control and Data Dependencies within System Specifications in SDL[J]. Computer Communications:23(7): 609-627.
Wang Chang-Jia, Liu Ming T. 1992. Axiomatic test sequence generation for extended finitestate machines[C]. Proceedings of the 12th International Conference on Distributed Computing Systems:252-259.
William H, Allen, Chin Dou. 2006. A Model-based Approach to the Security Testing of Network Protocol Implementations[C]. Local Computer Networks, Proceedings 2006 31st IEEE Conference:1008-1015
Xiao Shu, Deng Lijun, Li Sheng et al. 2003. PDUS-Integrated TCPIP protocol software testing for vulnerability detection[C]. Proceedings of the 2003 International Conference on Computer Networks and Mobile Computing (ICCNMC’03).
Yao TinYu , Gouda M. 1982. Deadlock detection for a class of communicating finite stat e machines[J]. IEEE Transactions on Communications: 30 (12):2514-2518.
Zhang Songtao, Dean T, Knight S. 2006. A Lightweight Approach to State Based Security Testing[C]. CASCON’06:341-344.
Zhang Songtao, Dean T, Kngiht S. 2007. Lightweight State Based Mutation Testing for Security[C]. TAICPART-MUTATION '07(00):223-232.