基于依赖条件重构的程序符号值分析方法

doi:10.3969/j.issn.0372-2112.2019.03.016

电子学报 ›› 2019, Vol. 47 ›› Issue (3): 630-635.DOI: 10.3969/j.issn.0372-2112.2019.03.016

基于依赖条件重构的程序符号值分析方法

郭曦¹, 王盼²

1. 华中农业大学信息学院, 湖北武汉 430070;
2. 武汉电力职业技术学院电力工程系, 湖北武汉 430079

收稿日期:2017-07-10 修回日期:2018-02-27 出版日期:2019-03-25
- 通讯作者:
- 郭曦
- 作者简介:
- 王盼女,1987年4月出生,河南济源人.博士、讲师.主要研究方向为电力电子变换、新能源等.E-mail:wangpan6712063@163.com
- 基金资助:
- 国家自然科学基金 (No.61502194）; 中央高校基本科研业务费专项基金 (No.2662018JC028）

Program Symbol Value Analysis Based on Dependent Condition Reconstruction

GUO Xi¹, WANG Pan²

1. College of Informatics, Huazhong Agriculture University, Wuhan, Hubei 430070, China;
2. Department of Power Engineering, Wuhan Electric Power Technical College, Wuhan, Hubei 430079, China

Received:2017-07-10 Revised:2018-02-27 Online:2019-03-25 Published:2019-03-25
- Supported by:
- National Natural Science Foundation of China (No.61502194); Fundamental Research Funds for the Central Universities (No.2662018JC028)

摘要/Abstract

摘要： 符号执行在路径分析、调试和验证等软件分析过程中发挥着重要的作用.但是随着程序规模的增大，有效的执行路径数量程指数级增长，符号执行技术往往难以有较好的分析效果.符号执行分析中的两个瓶颈问题是路径条件表达式的提取和约束求解.状态合并是目前解决状态爆炸的常用分析方法，但是这种抽象的分析方法往往会导致错误的路径信息.依据符号执行引擎采用的搜索策略，符号执行工具在符号变量状态合并中可能会产生不可解的路径条件.提出基于依赖条件重构的程序符号值分析方法，通过综合分析各路径的路径条件逻辑表达式，提取共享的变量符号值从而提高变量状态合并的效率，同时采用逆向关联分析方法产生依赖条件集合从而提高路径分析的精度.实验结果表明该方法相对于传统的状态合并分析方法有更高的执行效率及分析精度.

关键词: 程序分析, 符号执行, 关联依赖, 约束求解

Abstract: Symbolic execution is of vital importance for software engineering activities,such as path exploration,debugging and verification.However,symbolic execution techniques do not scale well for complicated realistic programs,because the number of feasible executions paths increases exponentially.Path condition expression extracting and constraint solving are the bottlenecks of symbolic execution.State merging is a common method to tackle the problem of state explosion,but this abstract procedure would be prone to incorrect path information.According to different searching strategy of symbolic engine,symbolic execution tools could generate unsolved path conditions during the process of symbolic variable state combination.A symbol value analysis based on dependent condition reconstruction method is proposed,which analysize the logic path conditions and extracts the common variable symbols to enhance the combination efficiency.Meanwhile,the backward analysis method is used to generate dependent condition set to improve the accuracy of path analysis.The experimental results demonstrate that it has better execution efficiency and accuracy compare to the tradition state combination methods.

Key words: program analysis, symbolic execution, related dependency, constrain solving

中图分类号:

TP311

郭曦, 王盼. 基于依赖条件重构的程序符号值分析方法[J]. 电子学报, 2019, 47(3): 630-635.

GUO Xi, WANG Pan . Program Symbol Value Analysis Based on Dependent Condition Reconstruction[J]. Acta Electronica Sinica, 2019, 47(3): 630-635.

参考文献

[1] KUZNETSOV V,KINDER J,BUCUR S,et al.Efficient state merging in symbolic excution[J].ACM SIGPLAN Notices,2012,47(6):193-204.
[2] GODEFROID P.Compositional dynamic test generation[A].Proceeding of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,2007.47-54.
[3] AVGERINOS T,REBERT A,CHA S K,et al.Enhancing symbolic execution with veritesting[A].Proceeding of the 36th International Conference on Software Engineering[C].New York:ACM,2014.1083-1094.
[4] GODEFROID P,NORI A V,RAJAMANI S K,et al.Compositional may-must program analysis:Unleashing the power of alternation[A].Proceeding of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,2010.43-56.
[5] TORLAK E,BODIK R.A lightweight symbolic virtual machine for solver-aided host languages[J].ACM SIGPLAN Notices,2014,49(6):530-541.
[6] VISSER W,REANU C S,NEK R.Test input generation for java containers using state matching[A].Proceeding of the 5th International Symposium on Software Testing and Analysis[C].New York:ACM,2006.37-48.
[7] BOONSTOPPEL P,CADAR C,ENGLER D.RWset:Attacking path explosion in constraint-based test generation[A].Proceeding of the 14th International Conference on TOOLS and Algorithms for the Construction and Analysis of Systems[C].Berlin:Springer,2008.351-366.
[8] SHARIR M,PNUELI A.Two Approaches to Interprocedural Dataflow Analysis[M].Englewood:Prentice-Hall,1981.189-234.
[9] REPS T,HORWITZ S,SAGIV M.Precise interprocedural dataflow analysis via graph reachability[A].Proceeding of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages[C].New York:ACM,1995.49-61.
[10] SEN K,NECULA G,GONG Liang,et al.MultiSE:Multi-path symbolic execution using value summaries[A].Proceeding of the 10th Joint Meeting on Foundations of Software Engineering[C].New York:ACM,2015.842-853.
[11] QI Dawei,NGUYEN H T,ROYCHOUDHURY A.Path exploration based on symbolic output[J].ACM Transaction on Software Engineering and Methodology,2011,22(4):278-288.
[12] 王伟光,曾庆凯,孙浩.面向危险操作的动态符号执行方法[J].软件学报,2016,27(5):1230-1245.WANG Wei-guang,ZENG Qing-kai,SUN Hao.Dynamic symbolic execution method oriented to critical operation[J].Journal of Software,2016,27(5):1230-1245.(in Chinese)
[13] 周艳红,王天成,李华伟,等.基于路径约束求解的多目标状态激励生成方法[J].计算机学报,2016,39(9):1829-1842.ZHOU Yan-hong,WANG Tian-cheng,LI Hua-wei,et al.Test generation for multiple target states using path constraint solving[J].Chinese Journal of Computers.2016,39(9):1829-1842.(in Chinese)
[14] 秦晓军,周林,陈左宁,等.基于懒符号执行的软件脆弱性路径求解算法[J].计算机学报,2015,38(11):2290-2300.QIN Xiao-jun,ZHOU Lin,CHEN Zuo-ning,et al.Software vulnerable trace's solving algorithm based on lazy symbolic execution[J].Chinese Journal of Computers,2015,38(11):2290-2300.(in Chinese)
[15] 王红阳,姜淑娟,王兴亚,鞠小林,张艳梅.基于子路径扩展的不可达路径检测方法[J].电子学报,2015,43(8):1555-1560.WANG Hong-yang,JIANG Shu-juan,WANG Xing-ya,JU Xiao-lin,ZHANG Yan-mei.An approach for detecting infeasible paths based on sub-path expansion[J].Acta Electronica Sinica,2015,43(8):1555-1560.(in Chinese)

基于依赖条件重构的程序符号值分析方法

Program Symbol Value Analysis Based on Dependent Condition Reconstruction

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 10

编辑推荐

Metrics

[1]	汪孙律, 杨秋松, 李明树. 一种针对格式文件的符号执行优化方法[J]. 电子学报, 2020, 48(12): 2417-2424.
[2]	杨超, 郭云飞, 扈红超, 刘文彦, 霍树民, 王亚文. 基于符号执行的软件缓存侧信道脆弱性检测技术[J]. 电子学报, 2019, 47(6): 1194-1200.
[3]	赵祖威, 冯世宁, 汤恩义, 陈鑫, 李宣东, 潘敏学, 赵晨. 一种符号执行制导的循环内界分析方法[J]. 电子学报, 2017, 45(11): 2582-2592.
[4]	徐超, 陈勇, 葛红美, 何炎祥. 基于符号执行的能耗错误检测方法[J]. 电子学报, 2016, 44(5): 1040-1050.
[5]	王红阳, 姜淑娟, 王兴亚, 鞠小林, 张艳梅. 基于子路径扩展的不可达路径检测方法[J]. 电子学报, 2015, 43(8): 1555-1560.
[6]	王志, 贾春福, 刘伟杰, 王晓初, 张海宁, 于晓旭, 陈喆. 一种抵抗符号执行的路径分支混淆技术[J]. 电子学报, 2015, 43(5): 870-878.
[7]	马森, 赵文, 习翔宇, 王栋伟. 基于值依赖分析的空指针解引用检测[J]. 电子学报, 2015, 43(4): 647-651.
[8]	万勇兵, 徐中伟, 梅萌. 一种符号化执行的实时系统一致性测试生成方法[J]. 电子学报, 2013, 41(11): 2276-2284.
[9]	曹春红;王利民;赵大哲. 基于离散元胞蚂蚁算法的几何约束求解技术研究[J]. 电子学报, 2011, 39(5): 1127-1130.
[10]	单锦辉;王戟;齐治昌. 面向路径的测试数据自动生成方法述评[J]. 电子学报, 2004, 32(1): 109-113.