作者投稿和查稿 主编审稿 专家审稿 编委审稿 远程编辑

计算机工程 ›› 2012, Vol. 38 ›› Issue (22): 24-27. doi: 10.3969/j.issn.1000-3428.2012.22.006

• 专栏 • 上一篇    下一篇

符号执行中的循环依赖分析方法

刘 杰,曹 琰,魏 强,彭建山   

  1. (国家数字交换系统工程技术研究中心,郑州 450002)
  • 收稿日期:2012-02-23 修回日期:2012-03-21 出版日期:2012-11-20 发布日期:2012-11-17
  • 作者简介:刘 杰(1983-),男,博士研究生、CCF会员,主研方向:软件安全分析;曹 琰,博士研究生;魏 强,副教授;彭建山,讲师
  • 基金资助:

    国家“863”计划基金资助项目(2008AA01Z420)

Loop Dependence Analysis Method in Symbolic Execution

LIU Jie, CAO Yan, WEI Qiang, PENG Jian-shan   

  1. (National Digital Switching System Engineering & Technological R&D Center, Zhengzhou 450002, China)
  • Received:2012-02-23 Revised:2012-03-21 Online:2012-11-20 Published:2012-11-17

摘要:

符号执行方法处理循环时存在路径爆炸的问题。为此,提出一种基于归纳变量的循环依赖分析方法。通过识别循环归纳变量及符号表达式,结合边界约束条件生成可达归纳变量分支的路径约束,并采用符号化映射方法分析嵌套循环归纳变量依赖问题,从而在不展开循环的情况下生成覆盖归纳变量分支的测试用例。对开源工具Libxml2进行实验,该方法能发现其中2个while循环所引发的数组访问越界错误。

关键词: 符号执行, 路径爆炸, 归纳变量, 循环依赖, 约束求解, 嵌套循环

Abstract:

Input-dependent loops can cause the problem of path explosion in symbolic execution, a method based on induction variable for analysis of loop dependence is proposed in this paper. By recognizing the loop induction variables and symbolic expressions, it is combined with the bound conditions to generate feasible path constraint for induction variable branches. Induction variable dependence of nested-loop is solved by symbolic affine analysis. It can generate test cases which can cover the branches of induction variables without loop unrolling. Test results show that by this method, two array access violations of the open source tools Libxml2 are found in while loops.

Key words: symbolic execution, path explosion, induction variable, loop dependence, constraint solving, nested loop

中图分类号: