###
Journal of Software:2019.30(11):3259-3280

一种基于程序功能标签切片的制导符号执行分析方法
甘水滔,王林章,谢向辉,秦晓军,周林,陈左宁
(数学工程与先进计算国家重点实验室, 江苏 无锡 214083;计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023)
Guiding Symbolic Execution Analysis by Leveraging Program Function Label Slice
GAN Shui-Tao,WANG Lin-Zhang,XIE Xiang-Hui,QIN Xiao-Jun,ZHOU Lin,CHEN Zuo-Ning
(State Key Laboratory of Mathematical Engineering and Advanced Computing, Wuxi 214083, China;State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China)
Abstract
Chart / table
Reference
Similar Articles
Article :Browse 1368   Download 1165
Received:January 14, 2016    Revised:February 19, 2016
> 中文摘要: 提出了一种基于程序功能标签切片的制导符号执行分析方法OPT-SSE.该方法从程序功能文档提取功能标签,利用程序控制流分析,建立各功能标签和程序基本块的映射关系,并根据功能标签在程序执行中的顺序关系生成功能标签执行流.针对给定的代码目标点,提取与之相关的功能执行流切片,根据预定义好的功能标签流制导规则进行符号执行分析,在路径分析过程中,及时裁剪无关的功能分支路径以提升制导效率.通过对不同的功能标签流进行分离制导符号执行分析,可避免一直执行某复杂循环体的情形,从而提高对目标程序的整体分支覆盖率和指令覆盖率.实验结果表明,通过对binutils、gzip、coreutils等10个不同软件中的20个应用工具上的分析,OPT-SSE与KLEE提供的主流搜索策略相比,代码目标制导速度平均提升到4.238倍,代码目标制导成功率平均提升了31%,程序指令覆盖率平均提升了8.95%,程序分支覆盖率平均提升了8.28%.
Abstract:This paper introduces a novel approach called OPT-SSE to speed up and scale symbolic execution-guided symbolic execution method based on program function label slice. The OPT-SSE is constituted by two parts. One part is static analysis, which decomposes the whole program execution paths by different program function label slices through establishing the mapping between function tags and program CFG. The other part is specified function tags guided rule symbolic execution, which cuts unrelated branch path timely according to specified function tags flow when taking symbolic execution analysis. Through analyzing specified function label slice or different function label slices concurrently, OPT-SSE could avoid stuck in complex cycle, which is beneficial for speeding up goal-guided process and scaling the symbolic execution. OPT-SSE is evaluated on twenty applications from ten famous open softwares, like binutils, gzip, coreutils, and so on. Through comparison with KLEE, OPT-SSE speeded up goal-guided by 4.238 times, increased the goal-guided success rate about 31%, and increased instruction coverage about 8.95%, branch coverage about 8.28%.
文章编号:     中图分类号:TP311    文献标志码:
基金项目:国家自然科学基金(91318301,61170066,6147179) 国家自然科学基金(91318301,61170066,6147179)
Foundation items:National Natural Science Foundation of China (91318301, 61170066, 6147179)
Reference text:

甘水滔,王林章,谢向辉,秦晓军,周林,陈左宁.一种基于程序功能标签切片的制导符号执行分析方法.软件学报,2019,30(11):3259-3280

GAN Shui-Tao,WANG Lin-Zhang,XIE Xiang-Hui,QIN Xiao-Jun,ZHOU Lin,CHEN Zuo-Ning.Guiding Symbolic Execution Analysis by Leveraging Program Function Label Slice.Journal of Software,2019,30(11):3259-3280