基于分离逻辑的程序验证研究综述

自20世纪60年代以来,虽然有Floyd-Hoare逻辑的出现,但使用形式化工具对命令式程序的正确性和可靠性进行自动验证,一直被认为是极具挑战性、神圣不可及的工作.20世纪末,由于更多科研的投入,特别是微软、IBM等大型公司研发部门的大量人力、物力的投入,程序验证方面在21世纪初取得了不少进展,例如用于验证空客代码无运行时错误的ASTRéE工具、用于Windows设备驱动里关于过程调用的协议验证的SLAM工具.但这些工具并没有考虑动态创建的堆(heap):ASTRéE工具假设待验证代码没有动态创建的堆,也没有递归;SLAM假设待验证系统已经有了内存安全性.事实上,很多重要的程序,例如Linux内核、Apache、操作系统设备驱动程序等,都涉及到对动态创建堆的操作.如何对这类操作堆的程序(heap-manipulating programs)进行自动验证仍然是一个难题.2001年~2002年,分离逻辑(separation logic)提出后,其分离(separation)思想和相应的框(frame)规则使得局部推理(local reasoning)可以很好地应用到程序验证中.自2004年以来,基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展,取得了很多令人瞩目的成果,例如Space Invader/Abductor,Slayer,HIP/SLEEK,CSL等工作.着重对这方面的部分重要工作进行阐述.

基于文法分支覆盖的短句子生成算法

提出一种上下文无关文法的句子生成算法.对于给定文法,算法生成一个满足该文法分支覆盖准则的句子集.结合长度控制、冗余消除和句子集规模控制等策略,使得生成的句子较短、无冗余、句子集规模较小.考察了算法在基于文法的软件系统的测试数据生成方面的应用情况.实验结果表明,该算法生成的测试数据具有较强的程序揭错能力,并且能够帮助测试人员提高测试速度.

基于Rectified Adam和颜色不变性的对抗迁移攻击

深度神经网络在物体检测、图像分类、自然语言处理、语音识别等众多领域上得到广泛应用.然而,深度神经网络很容易受到对抗样本(即在原有样本上施加人眼无法察觉的微小扰动)的攻击,而且相同的扰动可以跨模型、甚至跨任务地欺骗多个分类器.对抗样本这种跨模型迁移特性,使得深度神经网络在实际生活的应用受到了很大限制.对抗样本对神经网络的威胁,激发了研究者对对抗攻击的研究兴趣.虽然研究者们已提出了不少对抗攻击方法,但是大多数这些方法(特别是黑盒攻击方法)的跨模型的攻击能力往往较差,尤其是对经过对抗训练、输入变换等的防御模型.为此,提出了一种提高对抗样本可迁移性的方法:RLI-CI-FGSM.RLI-CI-FGSM是一种基于迁移的攻击方法,在替代模型上,使用基于梯度的白盒攻击RLI-FGSM生成对抗样本,同时使用CIM扩充源模型,使RLI-FGSM能够同时攻击替代模型和扩充模型.具体而言,RLI-FGSM算法将Radam优化算法与迭代快速符号下降法相结合,并利用目标函数的二阶导信息来生成对抗样本,避免优化算法陷入较差的局部最优.基于深度神经网络具有一定的颜色变换不变性,CIM算法通过优化对颜色变换图像集合的扰动,针对防御模型生成更多可迁移的对被攻击的白盒模型不那么敏感的对抗样本.实验结果表明,该方法在一般网络和对抗网络模型上都取得了更高的成功率.

改进的流不敏感的类型限定词推断

类型限定词可以精化标准类型,提高类型系统的表达能力。流不敏感的类型限定词推断已被用于CQual架构,以提高C程序的质量。然而,类型转化会影响类型限定词推断的有效性。首先,展示了一种允许类型转化的程序语言和流不敏感的限定词推断系统;其次,提出了变量参与的限定词推断系统,引入了联合类型并给出约束求解算法;最后,证明了推断的正确性并展示了一些实例运行结果。

基于限界约束的安全相关性质的推理证明

安全相关的性质如访问控制等在复杂环境下有十分重要的作用。从程序验证方面来说,不仅考虑安全性和活性的验证,还要考虑一些安全策略的性质,如非干涉性,这些不能用一般的性质来描述的安全策略可以被看作"超安全性质"。限界约束可通用地表示不同程度的访问频次限制,是安全相关性质验证中有效的辅助方法之一,在无线传感器网络协议、嵌入式系统等重要领域的性质验证方面具有广泛的应用价值。主要研究网络安全策略中的安全相关性质的限界表达及基于该限界约束的验证规则。