（计算机软件与理论专业论文）基于构造类别代数的协议安全测试研究.pdf

摘要诵矍随着通信协议的日益复杂，以及针对协议漏洞的攻击手段和技术的不断发展，因协议出错而引起的网络异常甚至崩溃现象层出不穷，危害了整个网络的信息安全。协议测试是协议工程的重要组成部分，是保证协议正常运行的关键技术。传统协议测试方法以一致性测试为代表，主要关注于协议的功能性，无法保证协议实现的安全性，因此需要进行协议安全测试的研究。协议存在的安全漏洞可以分为两类，一类是协议设计错误，例如导致使用者可以通过非法手段获取到不合法的权限。另一类是协议实现错误，由于通信协议是软件的一种，其实现过程不可避免的引入错误。本文中主要研究针对协议实现错误的安全测试理论和方法。现有针对协议安全测试的研究大都基于传统形式化模型如有限状态机等，采用随机或手动方法生成安全测试用例，通过观察待测协议实现在测试过程中是否崩溃来检测协议错误。现有方法中存在以下不足之处：首先，安全测试大都针对协议的数据流，而传统形式化模型描述协议数据流能力有限，不能满足安全测试的需求。其次，协议实现中可能存在的错误集合是无穷的，现有方法无法分析和评估测试的覆盖率。最后，协议崩溃只是协议错误可能导致的结果之一，现有方法更接近于鲁棒性测试，检错能力有限。本文中对基于构造类别代数的协议安全测试理论和方法进行了研究，主要工作集中在以下几个方面：1 ) 提出了扩展的构造类别代数模型构造类别代数是代数规范的一个扩充，适用于描述协议的数据流。本文对构造类别代数的基本定义进行了扩展：首先增加了对协议控制流状态的描述，并将其同内部环境变量结合，给出了协议状态的定义。而后根据协议测试过程中报文的不同流向，重新定义了可控制和可观察操作，给出了可控制函数的一般形式。最后，对公理形式进行了扩展，增强其描述协议行为的能力。扩展后的模型具有同e f s m 相同的控制流描述能力，但数据流描述能力更强，可用于协议安全测试的研究。提出了基于变异分析的协议安全测试方法变异分析是基于错误模型的测试方法，将其应用于基于构造类别代数的协议规范中，可以得到一系列规范的变异体，每个变异体对应于一类协议实现可能存在的错误。通过设计变异算子，可以限制协议实现中可能错误的规模，此外可以更有针对性构造测试用例，有效解决现有研究中存在的问题。本文对变异分析在构造类别代数中的应用进行了研究。首先设计了几类针对构造类别代数的变异算子，分析了应用算子以生成变异体的过程。而后分析摘要了产生等价变异体的原因，给出了一个基于公理优先级动态递推，生成非等价变异体及其对应变异单元集合的算法。3 ) 提出了协议安全测试序列生成方法本文中研究了基于变异体生成协议安全测试序列的方法，由于构造类别代数中同时描述了协议的控制流和数据流，因此在生成协议安全测试序列的过程中，需要同时考虑到控制流状态的可达性和数据流状态的可执行性。本文中分析了变异单元同安全测试序列的关系，先后给出了基于公理代入和逆向推导，以及基于可执行树正向推导安全测试序列生成方法。最后提出了一个结合主动和被动测试的协议安全测试序列生成方法，实验证明该方法可以有效减少协议测试序列的总长度，降低测试代价。钔设计并实现了分布式协议测试系统本文中设计并实现了一个分布式的协议安全测试系统，包括了一个主控中心和多个代理节点。系统基于底层支撑库的支持，将协议测试过程描述为对应的测试用例，并通过协调主控中心和分布式代理节点的行为，提供了对协议自动化测试的支持。该系统可用于协议的一致性测试和安全测试的研究中，大大提高测试用例开发和执行的效率。关键词：协议安全测试构造类别代数变异分析协议安全测试系统i i ia b s t r a c ta b s t r a c tw i t ht h ei n c r e a s i n gc o m p l e x i t yo fc o m m u n i c a t i o np r o t o c o l s ，a sw e l la sa t t a c k sa g a i n s tt h ep r o t o c o lv u l n e r a b i l i t i e sa n dt h ec o n t i n u o u sd e v e l o p m e n to ft e c h n o l o g y ,n e t w o r ka b n o r m a la n dc r a s hc a u s e db yf l a w so c c u rf r e q u e n t l y , e n d a n g e rt h ew h o l en e t w o r ko fi n f o r m a t i o ns e c u r i t y a sa l li m p o r t a n tp a r to fp r o t o c o le n g i n e e r i n g ，p r o t o c o lt e s t i n gi st h ek e yf o rap r o t o c o lt ow o r kp r o p e r l y t r a d i t i o n a la p p r o a c h e so fp r o t o c o lt e s t i n gl i k ec o n f o r m a n c et e s t i n gf o c u sm o r eo nt h ef u n c t i o n a l i t yo fp r o t o c o li m p l e m e n t a t i o nb u tn o tt h es e c u r i t y p r o t o c o ls e c u r i t yt e s t i n gi sg r a d u a l l yb e c o m i n go n eh o t s p o ti np r o t o c o lt e s t i n ga r e a t h e r ea r et w ot y p e so fp r o t o c o lv u l n e r a b i l i t i e s o n ei sp r o t o c o ld e s i g nv u l n e r a b i l i t i e s ，s u c ha su s e rc a l la c c e s su n a u t h o r i z e dp r i v a c yt h r o u g hi l l e g a lp a t h a n o t h e ri sp r o t o c o li m p l e m e n t a t i o nv u l n e r a b i l i t i e s ，s u c ha sp r o t o c o li sa l s oak i n do fs o f t w a r ew h e r ef l a w sa r ei n e v i t a b l ei ni m p l e m e n t a t i o n i nt h i st h e s i st h et h e o r ya n dm e t h o d so fp r o t o c o ls e c u r i t yt e s t i n gi ss t u d i e d , w h i c hm a i n l yf o c u so np r o t o c o li m p l e m e n t a t i o nv u l n e r a b i l i t i e s m o s te x i s t i n gm e t h o d so fp r o t o c o ls e c u r i t yt e s t i n ga r eb a s e do nt r a d i t i o n a lf o r m a ld e s c r i p t i o nm o d e l ss u c ha sf i n i t es t a t em a c h i n e w i t i ls e c u r i t yt e s t i n gs u i t e sg e n e r a t e de i t h e rm a n u a l l yo rr a n d o m l y , i m p l e m e n t a t i o nf l a w sa r ec h e c k e db ye x a m i n i n gw e a t h e rt h ei u tc r a s h e sd u r i n gt e s t i n g 1 1 1 ee x i s t i n gm e t h o d sh a v et h ef o l l o w i n gd e f i c i e n c i e s ：f i r s t ，s e c u r i t yt e s t i n gf o c u s e so nt h ep a r to fp r o t o c o ld a t af l o w , w h i l et r a d i t i o n a lf o r m a lm o d e lh a v el i m i t e da b i l i t yt od e s c r i b ep r o t o c o ld a t af l o wa n dc a nn o tm e e tt h er e q u i r e m e n to fs e c u r i t yt e s t i n g s e c o n d ，t h e r ec o u l db ei n f i n i t en u m b e ro fp o t e n t i a lf l a w si np r o t o c o li m p l e m e n t a t i o n ，w h i l ew ec a nn o te v a l u a t et h et e s t i n gc o v e r a g eo fe x i s t i n gm e t h o d s f i n a l l y , p r o t o c o lc o l l a p s ei sj u s to n ep o s s i b l er e s u l tc a u s e db yp r o t o c o lf l a w s 砀ee x i s t i n ga p p r o a c h e sa r em o r el i k er o b u s t n e s st e s t i n gw h i c hi sp o o ra tf l a wd e t e c t i o n i nt h i st h e s i s ，w ed i s c u s st h et h e o r ya n dp r a c t i c eo fs e c u r i t yt e s t i n gb a s e do nc o n s t r u c t e dt y p ea l g e b r a ( c t a ) w eu s ec t at od e s c r i b ep r o t o c o ls p e c i f i c a t i o n s ，a n dt h e ni n t r o d u c eaf a u l tm o d e lb a s e dm u t a t i o na n a l y s i st og e n e r a t em u t a n t so fs p e c i f i c a t i o n s e c u r i t yt e s t i n gs u i t e sa r ec o n s t r u c t e db a s e do nm u t a n t s t h ew o r ko ft h i st h e s i si n c l u d e s ：l 、e x t e n d e dc t af o r m a ld e s c r i p t i o nm o d e li va b s t r a c tc o n s t r u c tt y p ea l g e b r ai saf o r m a ld e s c r i p t i o nm e t h o db a s e do na l g e b r a i cs p e c i f i c a t i o n , a n di ss u i t a b l et os p e c i f yt h ed a t af l o wo fp r o t o c o l s i nt h i st h e s i s ，w ee x t e n dc t at oi m p r o v et h ea b i l i t yo fp r o t o c o ld e s c r i p t i o n f i r s t l y , w ea d dt h ed e s c r i p t i o no fc o n t r o lf l o w , a n dg i v et h ed e f i n i t i o no fp r o t o c o ls t a t eb a s e do nc o n t r o if l o wa n de n v i r o n m e n tv a r i a b l e s s e c o n d l y ，w er e d e f m et h ep o i n to fc o n t r o la n do b s e r v a t i o nd e s c r i p t i o na c c o r d i n gt ot h ep a c k e td i r e c t i o n s ag e n e r a l i z e df o r mo fc o n t r o l l a b l ef u n c t i o ni sg i v e n f i n a l l y , t h ea x i o mi se x t e n d e dt oi m p r o v et h ea b i l i t yo fd e s c r i b i n gp r o t o c o la c t i v i t i e s c o m p a r e dt oe f s m ，t h ee x t e n d e dc t am o d e lh a st h es a m ea b i l i t yt od e s c r i p tt h ec o n t r o lf l o wo fp r o t o c o l ，b u tb e t t e ra b i l i t yt od e s c r i p tt h ed a t af l o wp a r t ，w h i c hc a nb ea p p l i e di nt h er e s e a r c ho fp r o t o c o ls e c u r i t yt e s t i n g2 、t h e o r ya n dm e t h o do fs e c u r i t yt e s t i n gb a s e do nm u t a t i o na n a l y s i sm u t a t i o na n a l y s i si sa ne f f i c i e n tt e c h n i q u eb a s e do nf a u l tm o d e l b ya p p l y i n gm u t a t i o na n a l y s i s ，as e r i e so fm u t a n t so fp r o t o c o ls p e c i f i c a t i o nc a nb eg e n e r a t e d ，e a c hc o r r e s p o n d i n gt oo n ep o s s i b l ef a u l ti np r o t o c o li m p l e m e n t a t i o n b yt h ep r o p e rd e s i g no fm u t a t o r s ，w ec a nr e s t r i c tt h es c a l eo fp o s s i b l ef a u l ts e tu n d e rt e s t ，a n dc o n s t r u c tt e s t i n gs u i t e sm o r ep e r t i n e n t l y t h u sp r o t o c o ls e c u r i t yt e s t i n gb a s e do nm u t a t i o na n a l y s i sc a nb ea ne f f e c t i v es o l u t i o nt ot h ep r o b l e m so fe x i s t i n gm e t h o d s w ed i s c u s st h ea p p l i c a t i o no fm u t a t i o na n a l y s i si nc t a s e v e r a lm u t a t o r sf o rc t aa r ep r o p o s e d ，a n dt h ea f f e c to ft h e i ra p p l i c a t i o nt om u t a n t sa r ed i s c u s s e d w ea n a l y z e dt h er e a s o nf o re q u i v a l e n tm u t a n t f i n a l l y , ap r i o r i t yb a s e dm e t h o di sp r o p o s e dt og e n e r a t en o n e q u v a l e n ta n da s s o c i a t e dm u t a t i o ni t e m 3 、p r o t o c o ls e c u r i t yt e s t i n gs e q u e n c eg e n e r a t i o na l g o r i t h mi nt h i st h e s i s ，w es t u d yt h ep r o t o c o ls e c u r i t yt e s t i n gs u i t eg e n e r a t i n gm e t h o df r o mm u t a t n t s i n c eb o t ht h ed a t af l o wp a r ta n dc o n t r o lf l o wp a r to fp r o t o c o la r ec o n s i d e r e di nc t a ，t h et e s t i n gs u i t es h o u l df u l f i l lb o t ht h ec o n t r o lf l o wr e a c h a b i l i t ya n dd a t af l o we x e c u t a b i l i t y w ed i s c u s st h er e l a t i o nb e t w e e nm u t a t i o ni t e ma n ds e c u r i t yt e s t i n gs e q u e n c e w es t u d yt h ef o l l o w i n gt h r e em e t h o d s ：f i r s t ，am e t h o db a s e do na x i o ms u b s t i t u t i o na n dr e v e r s ed e d u c t i o ni sd i s c u s s e d ；t h e n ，af o r w a r dd e d u c t i o nm e t h o db yc r e a t i n gt e s t a b l et r e ei sp r o p o s e d ；f i n a l l y , ac o m p o s i t i o nt e c h n i q u eo fa c t i v et e s t i n ga n dp a s s i v et e s t i n gi si n t r o d u c e dt or e d u c et h el e n g t ho ft e s t i n gs u i t e s e x p e r i m e n tr e s u l t sp r o v et h a tt h em e t h o dc a ne f f e c t i v e l yr e d u c et h et e s t i n gc o s t 4 、d e s i g na n di m p l e m e n t a t i o no fas e c u r i t yt e s t i n gs y s t e ma tl a s t ，w ed e s i g na n di m p l e m e n tad i s t r i b u t e dp r o t o c o ls e c u r i t yt e s t i n gs y s t e mva b s t r a c ti nt h i st h e s i s t h i ss y s t e mc o n s i s t so fas e r v e ra n ds e v e r a la g e n tn o d e s a u t o m a t e dp r o t o c o lt e s d n gi sa l s os u p p o r t e d t h i ss y s t e mc a l li m p r o v et h ed e v e l o p i n ga n de x e c u t i n ge f f i c i e n c yo ft e s t i n gs u i t es i g n i f i c a n t l y , f o rp r o t o c o lc o n f o r m a n c et e s t i n ga n ds e c u r i t yt e s t i n g k e yw o r d s ：p r o t o c o ls e c u r i t yt e s t i n g ，i m p l e m e n t a t i o nv u l n e r a b i l i t i e s ，c o n s t r u c tt y p ea l g e b r a ，m u t a t i o na n a l y s i s ，d i s t r i b u t e dp r o t o c o ls e c u r i t yt e s t i n gs y s t e m中国科学技术大学学位论文原创性声明本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均已在论文中作了明确的说明。作者签名：童查：窒签字日期：中国科学技术大学学位论文授权使用声明作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论文的内容相一致。保密的学位论文在解密后也遵守此规定。忆医开口保密( 年)作者签名：耋多! 霉签字日期：五堕i ! ! 丝!导师签签字日荔乡移，、口一i 7第1 章绪论1 1 研究背景第1 章绪论随着计算机网络的不断普及，互联网逐渐成为人们生活中不可缺少的部分。通信协议是网络交互行为的主体，是计算机网络的灵魂所在。i s 0 - - 9 0 0 2 中规定了o s i 的七层架构，而采用五层架构的t c p i p 协议族则是事实上的标准。正是由于通信协议标准的统一和通用性，才使得不同产家的协议实现之间的交互成为可能，从而极大促进了通信网络的发展。然而随着网络技术的不断发展，网络协议的复杂度越来越高，这就给协议的开发带来了许多困难。协议开发过程中软件规模大、开发周期长、潜在错误多、标准化难以保证、移植性和可维护性差等问题相继出现。为解决上述问题，协议开发必须基于工程化方法进行。这种基于形式化的协议开发理论和技术，使用工程化的方法以保证协议开发效率以及通信系统性能的协议开发过程，称为协议工程( p r o t o c o le n g i n e e r i n g ) ( r u d i nh ，1 9 9 8 ，龚正虎，1 9 9 3 ) 。协议工程覆盖了协议生命期的各个阶段( a g g a r w a ls ，e ta 1 1 9 8 8 ，j o n s s o nb ，e ta 1 ，1 9 9 1 ，l i n nrj ，e ta 1 1 9 9 2 ) ，包括了协议设计、协议描述、协议验证与分析、协议实现和协议测试等过程。协议测试是协议工程的重要组成部分，是保证协议实现正常运行的关键技术。i s o9 6 4 6 - 2 中规定了四种协议测试方法：一致性测试( c o n f o r m a n c et e s t i n g ) ，主要测试协议实现同协议标准的一致性；互操作性测试( t e s t i n g ) ，主要测试不同协议实现之间的交互行为是否正确；性能测试( p e r f o r m a n c et e s t i n g ) ，主要测试协议实现的各方面性能指针，如传输率、速度、并发等；健壮性测试( r o b u s t n e s st e s t i n g ) ，主要测试协议实现在恶劣环境下的运行情况。随着协议的日益复杂，以及针对协议漏洞的攻击手段和技术的不断发展，因协议出错而引起网络异常甚至崩溃现象层出不穷，危害了整个网络的信息安全。传统协议测试方法以一致性测试为代表，大都关注于待测协议实现的功能性，假定其位于理想的网络环境中，通过同待测协议实现进行少量正常数据报文的交互，来测试其在是否实现了规范中定义的功能。在实际网络环境中，存在大量各种类型的网络数据报文，甚至包括人为构造的攻击报文，这些报文对协议实现的覆盖率远高于功能性测试，因此很可能触发协议安全漏洞，导致协议出错。现有协议测试方法无法保证协议实现的安全性，因此需要进行协议安第1 章绪论全测试的研究。协议存在的安全性漏洞可以分为两类( r a u l ik a k s o n e n ，2 0 0 1 ) ，一类是协议设计错误，例如导致使用者可以通过非法手段获取到不合法的权限，此类漏洞即狭义上的安全漏洞，通常需要较为复杂的触发条件。对此类错误，可采用协议验证方法加以检验，或基于已知的漏洞信息构造安全测试用例进行渗透测试等。另一类是协议实现错误，由于通信协议是软件的一种，其实现过程不可避免的会引入错误，此类错误的出现和触发均具有较高的随机性。本文中主要研究针对协议实现错误的安全测试理论和方法。协议安全测试可以做为现有功能性测试方法的有效补充，为协议的正常运行提供保障。目前协议安全测试已经逐渐成为测试领域一个新兴的热门研究问题，但现有针对安全测试的理论和方法的研究还远远不够深入，存在一些不足之处。1 2 研究现状1 2 1 形式化方法协议形式化方法( b l y t h ，d b o l d y r e f f , c ；r u g g l e s ，c ，e ta 1 ，1 9 9 0 ，h i n c h e y ,m q1 9 9 3 ) 是使用数学语言对协议规范或协议实现进行描述的技术。形式化方法可以消除协议文本基于自然语言描述导致的二义性，是协议工程的理论基础。协议形式化技术包括协议的形式化描述方法( f o r m a ld e s c r i p t i o nt e c h n i q u e ：f d t ) 和形式化描述语言( f o r m a ld e s c r i p t i o nl a n g u a g e s - f d l ) 。常见的协议形式化描述方法f d t 包括有限状态机( f i n i t es t a t em a c h i n e ：f s m ( g r e e np e ，1 9 8 6 ) ) 、p e t r i 网( p e t r i n e t ( c h e u n gt o y a t ，1 9 9 6 ) ) 、时序逻辑( t e m p o r a ll o g i c ：t l ( s c h w a r t zrl ，m e l l i a r - s m i t hpm ，1 9 9 4 ，m a r s h a l li ，1 9 9 4 ) ) 、进程代数( p r o c e s sa l g e b r a ( 如通讯进程演算c c s ( m i l n e rr ，1 9 8 0 ，龚正虎，1 9 9 5 ) 、通信顺序进程c s p ( h o a r ec a ，1 9 8 8 ) ) ) 和构造类别代数( 孙宇霖，屈玉贵，赵保华，2 0 0 1 ) 等。有限状念机是最常用的协议形式化描述方法，其将协议描述为一个有向图，图的节点表示协议所处的不同状态，图的有向边表示协议状态间的转移，有向边的权值记录了此状态转移所需要满足的输入激励和输出事件。有限状态机适用于描述协议的控制流，具有直观、描述简单和易于实现的优点，但其描述协议数据流的能力有限，且在描述复杂协议时，存在状态爆炸的问题。对有限状态机模型的扩展包括扩展有限状态机( e x t e n d e df i n i t es t a t em a c h i n e ：2第1 章绪论e f s m ( w a n gc h a n g j i a ，1 9 9 2 ) ) 、通信有限状态机( c o m u u n i c a t e df i n i t es t a t em a c h i n e ：c f s m ( y a ot i n g y u ，1 9 8 2 ) ) 等。p e t r i 网是对离散并行系统的数学表示，可用于表示系统部件异步并发操作，在协议验证方面有比较广泛的使用，能清楚的表达进程之间的通信( j i r a c h i e f p a t t a n a a ，1 9 9 5 ，d i a zme ta 1 ，1 9 9 7 ) 。p e t r i 网的扩展包括数字p e t r i网( n u m e r i c a lp e t r i n e t ：n p n ( m e h r p o u r h ，k a r b o w i a k a e ，1 9 9 0 ) ) 、时间p e 仃i网( t i m ep e t r in e t ：t p n ( l ix u a n d o n g ，l i l i u sj ，1 9 9 9 ) ) 和着色p e t r i 网( c o l o r e dp e t r i n e w ：c p n ( kj e a s e n ，1 9 8 1 ) ) 等。p e t r i 网清晰直观，具有坚实的数学基础和分析技术，其缺点主要在于描述复杂系统时过于繁琐，以及描述大型协议时同样存在着状态爆炸问题。时序逻辑模型使用时序算子对二阶谓词逻辑进行了扩展，可描述事件之间的顺序和相互关系。它能够描述程序的并发性质，具有完整的公理语义、指称语义、操作语义和证明系统。时序逻辑描述协议活动的能力强于f s m 和p e t r i网，其缺点主要是协议描述过于复杂，可读性较差。进程代数将协议描述为进程的集合，通过进程事件的集合和进程的迹来描述进程行为，并通过顺序、选择、并行算子来描述进程之间的关系。进程代数能严密的表述协议的逻辑结构和时序性，有助于协议验证和正确性证明。c c s和c s p 都是基于这样的理论。构造类别代数( c o n s t r u c t e dt y p ea l g e b r a ：c t a ) 是一种基于代数规范的协议形式化描述方法，通过在代数规范中引入构造函数，描述协议中实体对象的构造过程，定义了延拓函数集合以描述协议中对实体对象的操作，而通过公理集合限定了规范中各函数的处理过程。此外，在构造类别代数描述的协议规范中，通过指定函数的可观察和可控制性质，为协议规范增加了可控制观察点( p o i n to fc o n t r o la n do b s e r v e ：p c o ) 的描述。并通过定义偏代数对不完整的协议进行描述，或限制用于生成测试例的公式集合。构造类别代数方法适用于描述协议的数据流，也可以同有限状态机等描述协议控制流的模型相结合，达到对协议的完备描述。形式化描述语言f d l 是基于上述的一种或多种形式化模型，使用无二义的语法来描述协议规范，以消除自然语言歧义性的技术。国际标准化组织提出的形式化描述语言有三种：s d l 语言( b e l i n af ，h o g r e f ed ，1 9 8 9 ，i t u t ，1 9 9 6 ) 、l o t o s 语言( i s o i e c8 8 0 7 ，1 9 8 9 ) 和e s t e l l e 语言( i s o i e c9 0 7 4 ，1 9 8 9 ) 。s d l ( s p e c i f i c a t i o na n dd e s c r i p t i o nl a n g u a g e ) 语言是由国际电联组织c c i t t ( i t u - t ) 组织开发的电信领域的国际标准，它基于扩展有限状态机和抽象数据类型的混合技术，可精确定义通信系统的功能规格和行为描述，多用于3第1 章绪论实时分布式系统的形式化描述，目前已经被广泛应用在描述电子分布交换系统的形式化描述中。l o t o s ( l a n g u a g eo ft e m p o r a lo r d e rin gl a n g u a g e ) 是由国际标准化组织i s o 组织提出的形式化描述语言。l o t o s 包含以通信系统演算( c a l c u l u so fc o m m u n i c a t i n gs y s t e m ：c c s ) 为基础对协议的行为及交互作用进行描述的进程代数语言部分，以及基于代数规范的a c to n e 语言来描述协议中的抽象数据类型( a b s t r a c td a t at y p e ：a d t ) 的部分。l o t o s 抽象级别较高，比较容易转换为c c s 、c s p 或者t l 模型，但转变为程序设计语言则需要大量工作。e s t e l l e 语言也是由国际标准化组织i s o 提出的一种形式化描述语言，基于扩展有限状态机模型，通过对p a s c a l 语言进行扩展，可以较好的描述进程的并发、不确定性、超时、异步通讯状态。e s t e l l e 描述易于转换为实现，但缺乏有效描述递归共享通道( 广播通道) 、同步通讯、协议的性质( 如不变性) 等的手段，且不易转换为t l 或者c s p 等模型。1 2 2 协议一致性测试协议标准的制定虽然日益规范，但标准大都基于自然语言描述，容易存在歧义，因此实现者的不同理解可能导致协议实现同标准不一致的现象。协议一致性测试是测试协议实现是否符合协议标准的技术，是协议测试的重要分支，目前已有大量针对协议一致性测试的研究，并取得了一系列研究成果。国际标准i s o i e c9 6 4 6 “协议一性性测试的方法和框架 中提出了一致性测试的基本原理和抽象测试方法，包括抽象测试集a t s 的描述、树表结合表示法( t r e ea n dt a b u l a rc o m b i n e dn o t a t i o n ：t t c n ) 、一致性测试框架等。其中r ，r c n 语言不能描述并发的行为，因此对其进行了并发描述能力的扩展，即t t c n - 2 。虽然t t c n 是专门用于一致性测试的语言，但其对于新出现的不同领域的不同种类的测试仍然存在很多缺陷和不足。2 0 0 3 年，t t c n 一3 由欧洲电信标准协会( e t s i ) 发布，在保留t t c n 一2 良好特性的基础上，增加了对新的测试方式的支持。目前针对协议的一致性测试序列生成方法大都基于有限状态机模型，常见的生成方法包括转换回路法( t r a n s i t i o nt o u r ：t 方法( n a i t os ，t s u n o y a m am ，1 9 8 1 ) ) 、可区分序列法( d i s t i n g u i s h i n gs e q u e n c e s ：d 方法( g o n e n cg ，1 9 7 0 ) ) 、唯一输入输出序列方法( u n i q u ei n p u t 0 u t p u ts e q u e n c e s ：u 或u 1 0 方法( s a b n a mk ，d a h b u r a a ，1 9 8 8 ) ) 、特征集合方法( c h a r a c t e r i z i n gs e t ：w 方法( c h o w t ，1 9 7 8 ) ) 及其扩展w p - ( f u j i w a r as ，qv o nb o c h m a n n ，k h e n d e kfe ta 1 ，1 9 9 1 ) 方法等。o f f u t t ( 1 9 9 9 ) 等人提出了基于状态机模型的测试标准：转换覆盖、4第1 章绪论谓词覆盖、路径覆盖等。此外，f a b b r i 则将变异分析引入到有限状态机中，设计了针对有限状态机的几类变异算子，包括状态丢失、输出丢失等。针对扩展有限状态机的测试方法主要分为两类，类是将扩展有限状态机转化为只描述控制流的有限状态机，而后基于有限状态机模型下的测试方法生成测试序列( h e n n i g e ro l a f , n e u m a n np e t e r ，1 9 9 5 ) 。另一类是将扩展有限状态机分为控制流和数据流两部分，分别对两个部分进行测试( s ut 0 n g ，c h e nj u n l i a n g ，c h e n gs h i d u a n ，1 9 9 2 ，p a n gq i x i a n g ，c h e n gs h i d u a n ，j i ny u e h u i ，1 9 9 6 ，m a l o k un a i m ，f r e y p u c k om a r j e t a ，2 0 0 1 ) 。在协议的一致性测试中，同时考虑协议的控制流和数据流是一个很具有挑战的问题，l ih u a ( 1 9 9 8 ) 中提出了一种基于p e t r i 网的结合数据流和控制流的测试序列生成方法，该方法产生的测试序列在控制流上满足操作覆盖标准，在数据流方面满足a 1 1 - d e f s 、a 1 1 - u s e s 和最大i o d r - c h a i n 标准。针对针对s d l 语言的结合数据流和控制流的测试用例生成方法( u r a lh ，s a l e hk ，w i l l i a n m sa ，2 0 0 0 ，b o u r h f i rc ，a b o u i l h a m i de ，d s s o u l ire ta l ，2 0 0 1 ) ；郭雄辉( 2 0 0 3 )提出了一种基于构造类别代数的数据流和控制流相结合的协议测试方法。1 2 3 协议安全测试传统协议测试方法以一致性测试为代表，侧重于协议实现的功能性。这些方法大都假定协议运行于完全可靠无异常的网络环境下，通过构造少量正常的协议报文同待测协议实现进行交互，测试协议在理想环境下的功能实现情况。而在实际的复杂网络环境中，存在大量协议报文，甚至包括大量因意外或人为攻击产生的异常报文。这些协议报文有可能触发协议的安全漏洞，导致协议出错甚至崩溃。此外，传统协议测试方法大都只关注协议的控制流，即输入输出事件同协议状态转换之间的关系，而协议实现错误大多数是出现在对协议数据报文的处理过程中，即协议的数据流部分。综上所述，传统协议测试方法无法保证协议实现的安全性，有必要进行协议安全测试的研究。本文主要研究针对协议中可能存在的实现错误的协议安全测试理论和方法。同一致性测试相同，协议的安全测试也是黑盒测试，同样通过同协议实现之间的报文交互以完成测试过程。此外，协议安全测试的架构目前还处于研究过程中，没有专门的测试架构，现有工作中大都沿用协议一致性测试的框架。目前针对协议安全测试的研究大都集中在如何构造异常的输入数据报文上，常用技术包括随机测试、语法分析( s y n t a xa n a l y s i s ) 和错误注入技术( f a u l ti n j e c t i o n ) 等。随机测试通过随机生成测试数据，测试待测协议实现的数据处理过程。语法分析技术假定所有的输入报文都可以使用特定的语法表达第l 章绪论式加以描述，而后通过人为或随机的改变报文的各个数据域的取值，以达到构造特定测试数据的目的。错误注入技术将异常数据报文注入待测协议实现中，观察协议实现的响应，以判断是否存在漏洞。p r o t o s ( p r o t o s ，2 0 0 7 ，r a u l ik a k s o n e n ，2 0 0 1 ) 项目组使用属性方法( a t t r i b u t eg r a m m a r ) 来描述协议规范，将协议报文数据格式描述为巴科斯范式( b a c k u s n a u rf o r m ：b n f ) ，而后通过语法分析技术构造错误协议报文，项目组给出了针对b g p 、o s p f 等协议的一