周宽久，杨 广，赖晓晨，崔 凯，姚艳双

（大连理工大学 软件学院，辽宁 大连116620）

0 引 言

软件代码中的缺陷是导致软件故障和漏洞问题的主要原因［1］，国家自然科学基金委也设立可信软件重大研究计划专门解决软件可信性问题，通常的软件缺陷如缓冲区溢出、格式字符串、内存泄漏等无法通过安全子集检测出来，而又是影响软件可信性的主要原因，因此文章重点解决上述这些缺陷，从而达到提高软件可信性的目的。

对于软件代码漏洞缺陷检测的研究，国内外成果很多，Koushik Sen最早提出了concolic（一种白盒测试方法）单元测试的概念［2］，通过符号执行来计算程序的执行路径，研究如何赋初值的问题。Gulwani S提出一种基于有限回溯符号执行（symbolic execution）的缺陷自动验证方法，结合路径条件和缺陷触发条件进行缺陷自动验证［3］。Froihofer L等人则通过源码插桩方式得到程序动态运行的输出信息和日志，可以有效分离系统的业务逻辑与检测逻辑，增加程序动态分析的可靠性［4］。针对代码检测误报率过高的问题，肖庆，官云战等人提出了使用多项式时间复杂度的路径敏感算法实现对代码缺陷的静态检测，该方法通过控制流图实现属性状态条件的合并，判断不可达性，降低误报率［1］。近年来模型验证也成为代码诊断领域研究的热点，卞磊，刘超等人使用有穷状态机模型对过程内变量数据流异常进行检测，根据数据项的状态迁移判断过程内的数据流是否异常［5］。周宽久等人提出了一种基于XML中间模型的代码安全规范检测方法，使用GJB安全子集对代码安全进行分析［6］。……