1(华中农业大学信息学院计算机科学系 武汉 430070);2(武汉电力职业技术学院电力工程系 武汉 430079) (xguo@mail.hzau.edu.cn)
出版日期:
2018-10-01基金资助:
国家自然科学基金项目(61502194);中央高校基本科研业务费专项资金(2662018JC028)Variable Dependent Relation Analysis in Program State Condition Merging
Guo Xi1, Wang Pan21(Department of Computer Science, College of Informatics, Huazhong Agriculture University, Wuhan 430070);2(Department of Power Engineering, Wuhan Electric Power Technical College, Wuhan 430079)
Online:
2018-10-01摘要/Abstract
摘要: 程序分析的主要目标是对程序的性质进行研究,符号执行作为目前主流的分析方法在生成高效的测试用例集或提高路径覆盖率等方面发挥着重要的作用,其中路径条件表达式的提取以及约束求解是路径分析过程中的关键步骤.现有的路径分析方法普遍存在约束求解效率不高而导致的路径覆盖率较低的问题.由于符号执行引擎所采用的搜索策略不尽相同,在符号执行分析过程中存在状态合并的过程,该抽象过程可能导致产生不正确的测试用例.以提高路径分析效率为目标,提出一种高效的程序分析方法:首先对传统的符号执行树的表示方法进行改进,提取不同路径共享的符号表达式和路径约束条件以提高符号执行过程中状态合并的效率,然后采用隐式关联分析方法,产生逆向分析中的依赖条件集合,并给出基于依赖条件重构的算法以提高路径覆盖率.实验结果表明:相对于传统的状态合并以及符号执行方法,该方法有更为高效的状态合并效率以及更高的路径约束条件分析精度.
参考文献
相关文章 11
[1] | 谭坚, 罗巧玲, 王丽一, 胡夏晖, 范昊, 徐占. 基于SMT求解器的微处理器指令验证数据约束生成技术[J]. 计算机研究与发展, 2020, 57(12): 2694-2702. |
[2] | 黄桦烽,王嘉捷,杨轶,苏璞睿,聂楚江,辛伟. 有限资源条件下的软件漏洞自动挖掘与利用[J]. 计算机研究与发展, 2019, 56(11): 2299-2314. |
[3] | 刘经德,陈振邦,王戟. 基于求解开销预测的符号执行搜索策略研究[J]. 计算机研究与发展, 2016, 53(5): 1086-1094. |
[4] | 陈喆,王志,王晓初,贾春福. 基于代码移动的二进制程序控制流混淆方法[J]. 计算机研究与发展, 2015, 52(8): 1902-1909. |
[5] | 王 进, 黄志球, 唐佳俊, 陈 哲, 肖芳雄,. BPEL谓词约束建模及可行路径分析[J]. 计算机研究与发展, 2014, 51(4): 838-847. |
[6] | 陈冬火, 刘 全,. 基于符号执行和LTL公式重写的测试用例产生方法[J]. , 2013, 50(12): 2661-2675. |
[7] | 赵云山 宫云战 周 傲 王 前 周虹伯. 静态缺陷检测中的误报消除技术研究[J]. , 2012, 49(9): 1822-1831. |
[8] | 贾春福 王 志 刘 昕 刘昕海. 路径模糊:一种有效抵抗符号执行的二进制混淆技术[J]. , 2011, 48(11): 2111-2119. |
[9] | 严俊, 郭涛, 阮辉, 玄跻峰,. JUTA: 一个Java自动化单元测试工具[J]. , 2010, 47(10): 1840-1848. |
[10] | 徐贵红, 张 健,. 基于约束的主动规则终止性分析[J]. , 2006, 43(5): 894-900. |
[11] | 季晓慧, 张 健, . 一种求解混合约束问题的快速完备算法[J]. , 2006, 43(3): 551-556. |
PDF全文下载地址:
https://crad.ict.ac.cn/CN/article/downloadArticleFile.do?attachType=PDF&id=3800