Program Symbol Value Analysis Based on Dependent Condition Reconstruction

doi:10.3969/j.issn.0372-2112.2019.03.016

您当前的位置：

首页 >

文章列表页 >

Program Symbol Value Analysis Based on Dependent Condition Reconstruction

更新时间：2025-07-02

- Program Symbol Value Analysis Based on Dependent Condition Reconstruction
- Acta Electronica Sinica Vol. 47, Issue 3, Pages: 630-635(2019)
- 作者机构：
  
  1. 华中农业大学信息学院,湖北,武汉,430070
  2. 武汉电力职业技术学院电力工程系,湖北,武汉,430079
  3. 华中农业大学信息学院,湖北,武汉,430070
  4. 武汉电力职业技术学院电力工程系,湖北,武汉,430079
- 作者简介：
- 基金信息：
  
  National Natural Science Foundation of China (No.61502194);Fundamental Research Funds for the Central Universities (No.2662018JC028)
- DOI：10.3969/j.issn.0372-2112.2019.03.016
  CLC： TP311
- Published Online：25 March 2019，
  
  Published：2019
- 稿件说明：
移动端阅览
Program Symbol Value Analysis Based on Dependent Condition Reconstruction[J]. Acta Electronica Sinica, 2019, 47(3): 630-635.
DOI：

Program Symbol Value Analysis Based on Dependent Condition Reconstruction[J]. Acta Electronica Sinica, 2019, 47(3): 630-635. DOI： 10.3969/j.issn.0372-2112.2019.03.016.

摘要

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

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.

关键词

Keywords

references

Views

322

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Semantic Comparison Model for Binary Programs Based on Statistical Reasoning

Bayesian Program Analysis

Null Pointer Dereference Detection Based on Value Dependences Analysis

Branch Obfuscation to Combat Symbolic Execution

Related Author

WANG Pan

GUO Xi

XIONG Ying-fei

ZHANG Yi-fan

LI Tian-chi

CHEN Yi-fan

WU Yi-qian

WANG Guan-cheng

Related Institution

College of Informatics, Huazhong Agricultural University

Hubei Key Laboratory for High-Efficiency Utilization of Solar Energy and Operation Control of Energy Storage System, Hubei University of Technology

Key Laboratory of High Confidence Software Technologies （Peking University）， Ministry of Education

School of Computer Science， Peking University

⁰