首页 | 本学科首页   官方微博 | 高级检索  
     

一种基于程序功能标签切片的制导符号执行分析方法
引用本文:甘水滔,王林章,谢向辉,秦晓军,周林,陈左宁.一种基于程序功能标签切片的制导符号执行分析方法[J].软件学报,2019,30(11):3259-3280.
作者姓名:甘水滔  王林章  谢向辉  秦晓军  周林  陈左宁
作者单位:数学工程与先进计算国家重点实验室, 江苏 无锡 214083,计算机软件新技术国家重点实验室(南京大学), 江苏 南京 210023,数学工程与先进计算国家重点实验室, 江苏 无锡 214083,数学工程与先进计算国家重点实验室, 江苏 无锡 214083,数学工程与先进计算国家重点实验室, 江苏 无锡 214083,数学工程与先进计算国家重点实验室, 江苏 无锡 214083
基金项目:国家自然科学基金(91318301,61170066,6147179)
摘    要:提出了一种基于程序功能标签切片的制导符号执行分析方法OPT-SSE.该方法从程序功能文档提取功能标签,利用程序控制流分析,建立各功能标签和程序基本块的映射关系,并根据功能标签在程序执行中的顺序关系生成功能标签执行流.针对给定的代码目标点,提取与之相关的功能执行流切片,根据预定义好的功能标签流制导规则进行符号执行分析,在路径分析过程中,及时裁剪无关的功能分支路径以提升制导效率.通过对不同的功能标签流进行分离制导符号执行分析,可避免一直执行某复杂循环体的情形,从而提高对目标程序的整体分支覆盖率和指令覆盖率.实验结果表明,通过对binutils、gzip、coreutils等10个不同软件中的20个应用工具上的分析,OPT-SSE与KLEE提供的主流搜索策略相比,代码目标制导速度平均提升到4.238倍,代码目标制导成功率平均提升了31%,程序指令覆盖率平均提升了8.95%,程序分支覆盖率平均提升了8.28%.

关 键 词:制导符号执行  分支覆盖率  指令覆盖率  搜索策略  程序切片
收稿时间:2016/1/14 0:00:00
修稿时间:2016/2/19 0:00:00

Guiding Symbolic Execution Analysis by Leveraging Program Function Label Slice
GAN Shui-Tao,WANG Lin-Zhang,XIE Xiang-Hui,QIN Xiao-Jun,ZHOU Lin and CHEN Zuo-Ning.Guiding Symbolic Execution Analysis by Leveraging Program Function Label Slice[J].Journal of Software,2019,30(11):3259-3280.
Authors:GAN Shui-Tao  WANG Lin-Zhang  XIE Xiang-Hui  QIN Xiao-Jun  ZHOU Lin and CHEN Zuo-Ning
Affiliation:State Key Laboratory of Mathematical Engineering and Advanced Computing, Wuxi 214083, China,State Key Laboratory for Novel Software Technology(Nanjing University), Nanjing 210023, China,State Key Laboratory of Mathematical Engineering and Advanced Computing, Wuxi 214083, China,State Key Laboratory of Mathematical Engineering and Advanced Computing, Wuxi 214083, China,State Key Laboratory of Mathematical Engineering and Advanced Computing, Wuxi 214083, China and State Key Laboratory of Mathematical Engineering and Advanced Computing, Wuxi 214083, China
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%.
Keywords:guided symbolic execution  branch coverage  instruction coverage  search strategy  program slice
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号