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

• 学术论文 • 上一篇    下一篇

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

郭曦1, 王盼2   

  1. 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 Xi1, WANG Pan2   

  1. 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: 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

中图分类号: