摘要
符号执行作为一种基本的程序分析技术,已被广泛应用于软件测试领域。研究表明,即使在现有的查询优化技术的支持下,约束求解也仍然是符号执行中最耗时的部分。猜测符号执行的思想是将多次约束求解合并成一次求解,从而减少约束求解消耗的时间。但是,猜测的成功率受猜测深度和路径搜索方向的影响,尤其是路径搜索的方向在较大程度上决定了整体猜测的成功率。因此,引导路径搜索向成功率高的方向进行,对提高猜测符号执行的整体效率至关重要。在猜测符号执行的路径搜索过程中引入蚁群算法,根据节点条件信息初次确定分支路径的权重,在多次迭代中根据分支路径的覆盖情况更新权重,通过权重决定路径搜索的方向。实验表明,该方法有效提升了猜测符号执行的效率。
Symbolic execution has been widely used in the field of software testing.The research shows that constraint solving is the most time-consuming part in symbolic execution,even though some optimization techniques are used.The speculative symbolic execution reduces the consuming time of constraint solved by making several continuous constraint solving merge into once.The success rate of every time guess is affected by the depth of conjecture and the direction of search,especially the direction of search.Therefore,how to guide the path search to conduct in the direction of success is very important to improve the efficiency of speculative symbolic execution.In this paper,ant colony algorithm was used to search the path.Firstly,according to the node condition,the weight of branch path was determined.Then,the weight of a branch was updated according to whether this branch is covered in every time guess.This paper chose the direction of search based on the weight of branch.The experimental results show that the proposed method can improve the efficiency of speculative symbol execution effectively.
作者
李航
臧洌
甘露
LI Hang;ZANG Lie;GAN Lu(School of Computer Science and Technology,Nanjing University of Aeronautics & Astronautic)
出处
《计算机科学》
CSCD
北大核心
2018年第6期145-150,共6页
Computer Science
关键词
蚁群算法
猜测符号执行
约束求解
路径搜索
Antcolony algorithm
Speculative symbolic execution
Constraint solving
Path search