利用构造类别代数的协议安全测试方法

针对协议安全测试中数据流的描述问题,在构造类别代数的基础上引入变异分析,由此提出了一种协议安全测试方法.基于协议的描述设计了变异算子,然后对一致性公式集进行变异分析,从而得到安全变异项集.将变异项转换为实际的安全测试例集,并描述由此进行的协议安全测试步骤.测试实践表明,所提方法能与一致性测试良好地结合,在一定程度上覆盖已知安全漏洞,并具有发现潜在问题的能力.     

SPMutation:存储过程变异工具的设计与实现

针对存储过程混合了SQL语句以及流程控制等语句的特点,设计了一个变异工具SPMutation.定义了一个覆盖存储过程语法规则的变异算子集合,该算子集包含22个算子,能够对存储过程进行元素级、表达式级和语句级三种不同层次的变异操作.SPMutation通过配置变异算子集文件可以实现对存储过程新的语法规则的错误模拟,具有良好的可扩展性.实验表明:SPMutation能有效地生成变异体集合,生成的等价变异体数量少于总变异体数15%;通过变异测试过程完善测试用例集,可以使测试用例集的变异分数高于0.9,并趋近于1;对存储过程的变异测试可以在有限的时间内完成.     

基于二进制序列集合的策略合成代数框架

从代数建模和实现机制相融合的角度出发,提出了一种基于二进制序列集合的策略合成代数框架.首先通过定义二进制序列集合元素及构造集合运算规则,将策略抽象成逻辑模型.然后针对多终端二进制决策树（MTBDD）的逻辑建模机制中存在的编码次序敏感以及规则冗余问题,提出了基于二进制序列的移位合并算法.最后推导基于二进制序列的合成语义算子,建立该代数框架.通过时间复杂性分析和仿真实验,验证了该框架的有效性,其合成性能优于基于MTBDD策略树的合成机制.     

面向命题投影时序逻辑的安全协议模型检测

针对无条件安全通信协议,特别是Russian Cards协议的安全性验证问题,提出基于命题投影时序逻辑(PPTL)的模型检测方法.根据协议构造规则建立了Russian Cards协议的ProMeLa模型;利用chop算子将多个交互事件进行顺序复合,以表达协议所期望的通信序列;由projection算子定义了协议在该序列上的安全性质,再将该性质转为Never Claim语法结构并连同协议模型作为模型检测器SPIN的输入,以完成验证工作.验证结果表明,由协议规则构造的Russian Cards通信协议是安全可靠的,该方法也适用于一般的无条件安全通信协议的验证.     

基于OPTICS算法的变异体约简技术

为了降低变异测试的计算代价,提出了一种基于OPTICS算法的变异体约简方法。首先利用OPTICS算法对变异体进行聚类,让相似的变异体在同一类簇中,然后从每个类簇中随机选取一个变异体作为代表,与其余离散的变异体组成新的变异体集合,从而达到约简变异体数量的目的。为了验证算法的效果,选择一组常用的被测程序进行实验,并和K-means算法进行比较。实验结果表明,该方法在不降低变异充分度的情况下取得了良好的约简效果,有效地减少了变异体的数量,从而降低了变异测试所产生的计算代价。     

拟代数Domain的若干性质

基于拟连续Domain的等价定义及其构造，研究了拟代数Domain的一系列性质，并且给出了它的等价刻画，由此得到拟代数Domain一定是拟连续Domain．通过讨论Scott连续闭包算子保持集合与集合之间的Waybelow关系这一特性，证明了拟代数Domain在Scott连续闭包算子下的像仍是拟代数Domain；得到了拟代数Domain上赋予Scott拓扑构成Baire空间，拟代数格上赋予Lawson拓扑构成Priestley空间等结论．     

一种新的电子邮件协议及其形式化分析

在安全协议的形式化分析方法中,串空间模型和基于串空间模型的协议认证分析方法是比较常用的验证方法.分析了DKNRP协议存在一定的缺陷,并提出一种新的电子邮件协议,基于扩展的串空间模型采用认证测试方法,验证了新协议可以满足其安全目标.     

基于启发式变异的改进演化规划算法

常用的演化规划算法(EP)的变异是基于固定的概率分布,鲁棒性较差.文中分析了变异算子对演化规划算法计算效率的影响,指出了Gauss变异、Cauchy变异和Lévy变异算子缺少启发式信息的不足,并据此设计了一种根据种群个体差异信息的启发式变异算子,用算子抽取的个体差异来更新变异步长,允许个体有机会在某些维数保持原状,只是进行部分维数上的变异.启发式变异算子能使演化规划算法更好地适应不同特点的连续优化问题,从总体上增强算法的鲁棒性.在求解多个Benchmark测试问题的数值实验中,基于启发式变异的改进演化规划算法比当前6种等概率分布演化规划算法有更快的收敛速度和更优的平均性能.     

一种安全DSR协议的形式化分析方法

目前安全 DSR协议由于缺乏有效的形式化分析方法,难以发现一些隐蔽的安全漏洞.针对这一问题,通过分析DSR协议路由过程,给出了安全DSR协议的安全目标.提出了一种基于逻辑的安全DSR协议形式化分析方法,定义了能够反映安全DSR协议特性的基本逻辑构件(包括主体、目标和公式)和推理规则.首先用逻辑公式描述协议初始假设及过程,然后用推理规则进行推导产生推导结果,最后依据推导结果判断协议安全性.使用这种方法对SADSR协议进行了形式化分析与改进,发现了SADSR协议存在的安全漏洞.分析结果表明,提出的方法能够用于安全DSR协议形式化分析,能够发现一些较为隐蔽的安全缺陷.     

用分布式时序逻辑形式化分析IEEE802.11i协议

基于Caleiro提出的分布式时序逻辑,在其模型中增加了挑战问题集合和挑战应答集合,将IEEE802.11i协议转化为分布式时序逻辑的事件结构语义模型.形式化分析并证明了该协议的保密性以及协议中申请者、认证者、认证服务器之间的相互认证性.结果表明,IEEE802.11i协议是安全的.     

一种压缩向量对测试集的新方法

通过施加一个测试向量对,瞬态电流测试可以检测出CMOS数字电路中的某些故障,这些故障通常（例如开路故障）不能被传统的电压测试和稳态电流测试有效地检测出来。研究如何有效地压缩向量对测试集与通常的测试向量压缩一样,意义十分重要,但目前人们对此研究得较少。首先使用三种现有的游程编码方法对向量对测试集进行压缩,并比较它们的压缩结果。在此基础上．提出了一种更好的压缩方法。采用新方法对几个ISCAS标准电路的开路故障向量对测试集进行压缩,实验证明压缩效果比三种游程编码方法都要好。而且,新方法的解码代价非常小,适合压缩大型电路的开路故障测试集。     

基于渗透测试的网络安全漏洞实时侦测技术研究

传统网络安全漏洞侦测技术无法准确得到攻击注入点,和服务器交互频繁,导致侦测结果不可靠、效率低下。为此,提出一种新的基于渗透测试的网络安全漏洞实时侦测技术。设计了渗透测试下网络安全漏洞实时侦测系统,构建系统架构,在生成攻击图时,将网络当前节点漏洞看作单位编码,利用进化计算对不同漏洞属性权重进行调整,获取攻击图库。在设计攻击注入点分析模块时,利用广度优先爬取法,依据网页目录层次实现网络页面爬取;通过爬取过程获取网络全部页面攻击注入点,根据Bloom Filter对重复的URL进行去重处理。利用渗透测试实现攻击和分析模块设计,以此生成攻击图对注入点注入攻击;对攻击反馈进行研究,判断注入点是否存在网络安全漏洞。渗透测试时为了降低交互频率,通过探子请求技术完成探测,对是否进行进一步侦测进行判断。实验结果表明,所提技术侦测结果可靠,效率高。     

一种基于EAI模型的软件安全测试方法

研究了一种用于测试软件安全的基于EAI(Environment Application Interaction Model)模型的软件错误注入测试方法,提出了用包裹函数实现软件错误注入的安全测试方法及实现方法.对四个应用软件进行了实际测试,实验结果表明,该方法是有效的.     

一种基于CPN的协议测试序列生成方法

针对状态空间规模较大的协议,提出了一种基于着色Petri网CPN(ｃolored ｐetri ｎet)、面向属性的协议一致性测试序列生成方法。 首先, 构建被测协议规范的CPN模型, 即协议模型, 并将被测协议的若干功能属性采用CPN进行形式描述, 形成属性模型。 提出了属性模型到协议模型的状态投影算法、模型状态空间的路径匹配算法和搜索算法, 基于这些算法给出了一种完整的基于属性的测试序列生成方法。 该方法不但可以有效避免协议规模庞大所导致的状态爆炸问题, 而且还对测试中的PCO库所进行了特殊标识, 完成测试序列中可观察元素的自动提取处理, 使得处理后的测试序列可直接用于协议实际测试过程。 为有效验证所提测试序列生成方法的可行性, 开发了一套实现该方法的软件, 并应用于HMIPv6协议的实际测试过程中。实践表明, 这套软件可以对较为复杂的协议一致性测试过程提供强有力的支持。     

基于有限状态机的被动测试错误诊断

针对被动测试错误诊断算法只能推测出被测系统可能存在错误却无法准确定位错误的问题，提出了一种逐步定位系统实现错误的层次递进的方法．先利用测试序列的输入输出信息并结合错误模型生成初始诊断错误集合，再依据测试套上下文使用错误检测算法对该集合进行筛选，最后经连续观察或结合主动测试进行错误区分．实例验证结果表明，所提方法能够对绝大多数有单个实现错误的有限状态机模型进行错误定位．     

一种通信有限状态机的被动测试及其错误诊断

针对现有的被动测试方法无法解决嵌入式通信系统的错误检测问题，提出了一种被动测试错误检测方法．该方法在外部通道放置观察者，并使用了全局状态描述系统的当前可能状态，利用了观察到的输入输出信息，同时结合了模型转换推测出系统的状态变迁．基于该检测方法又设计出一种层次化的错误诊断算法，首先记录被动检测过程中系统经历的转换轨迹，用变异分析方法生成候选诊断，然后通过被动观察来降低错误集合的规模，最后使用区分序列和交叉判定进行错误定位．通过一个实际的H．245通信协议的实验表明，所提算法能够在有限观察步骤内检测出被测系统中的错误，并能有效定位检测错误，其回溯算法也可以显著缩短错误症状序列的长度．     

一种提高协议测试效率的新方法

针对使用传统的方法提高协议测试效率存在的问题，从测试序列测试顺序的角度，首次引入了测试序列动态重排序的方法，对不同的错误情况，提出三种动态排序算法．讨论了测试序列动态重排序对测试效率产生的影响．实验仿真验证了所提动态排序方法比传统的静态测试在测试效率上有较大改进．     

一种动态协议一致性测试方法

利用约束满足技术实现了一种新的动态协议一致性测试方法，解决了由于固定测试集的错误覆盖度、测试用例的相关性，以及实测结果的影响，导致实际测试中存在执行效率不高和实际测试范围可能被缩小的问题．     

降低软件变异测试复杂性的新方法

基于硬件测试技术中经常使用的故障控制及等价关系的理论,对软件变异测试提出一种新的简化决策条件故障的思想和技术,使得在变异测试中需要注入的故障数得以减少,从而简化软件变异测试过程,缩短了测试时间.由此也可有效降低软件测试复杂性,提高测试效率.实验结果证明了所提出的思想和方法的正确性和有效性.