摘要
符号执行在路径分析、调试和验证等软件分析过程中发挥着重要的作用.但是随着程序规模的增大,有效的执行路径数量程指数级增长,符号执行技术往往难以有较好的分析效果.符号执行分析中的两个瓶颈问题是路径条件表达式的提取和约束求解.状态合并是目前解决状态爆炸的常用分析方法,但是这种抽象的分析方法往往会导致错误的路径信息.依据符号执行引擎采用的搜索策略,符号执行工具在符号变量状态合并中可能会产生不可解的路径条件.提出基于依赖条件重构的程序符号值分析方法,通过综合分析各路径的路径条件逻辑表达式,提取共享的变量符号值从而提高变量状态合并的效率,同时采用逆向关联分析方法产生依赖条件集合从而提高路径分析的精度.实验结果表明该方法相对于传统的状态合并分析方法有更高的执行效率及分析精度.
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.
作者
郭曦
王盼
GUO Xi;WANG Pan(College of Informatics,Huazhong Agriculture University,Wuhan,Hubei 430070,China;Department of Power Engineering,Wuhan Electric Power Technical College,Wuhan,Hubei 430079,China)
出处
《电子学报》
EI
CAS
CSCD
北大核心
2019年第3期630-635,共6页
Acta Electronica Sinica
基金
国家自然科学基金(No.61502194)
中央高校基本科研业务费专项基金(No.2662018JC028)
关键词
程序分析
符号执行
关联依赖
约束求解
program analysis
symbolic execution
related dependency
constrain solving
