Survey of Constraint Solving Techniques Research Progress in Symbolic Execution

被引：0

作者：

Zou Q.-C. ^{[1
,2
]}

Wu R.-P. ^{[1
]}

Ma J.-X. ^{[1
]}

Wang X. ^{[1
]}

Xin W. ^{[1
]}

Hou C.-Y. ^{[3
]}

Li M.-C. ^{[1
]}

机构：

[1] China Information Technology Security Evaluation Center, Beijing

[2] 360 Security Research Labs, Beijing

[3] Beijing Central Security Evaluation Technology Co. Ltd., Beijing

来源：

Beijing Ligong Daxue Xuebao/Transaction of Beijing Institute of Technology | 2019年 / 39卷 / 09期

关键词：

Constraint solving; Performance optimization; Symbolic execution; Vulnerability discovery;

D O I：

10.15918/j.tbit1001-0645.2019.09.013

中图分类号：

学科分类号：

摘要：

In symbolic execution, constraint solving is mainly responsible for path reachability prediction and test input generation, but due to the path explosion problem and the limited power of the SMT solver, constraint solving occupy high overhead in symbolic execution, and this problem has become one of the bottlenecks in symbolic execution. This paper first introduces the basic concepts of symbolic execution, constraint solving, and analyzes the origin of the constraint solving problem. Second, this paper divides the optimization techniques in recent years into three stages: pre-solving, in-solving and post-solving. The related techniques include slicing, simplification, fast unsatisfiability check, multi-solver support, etc. Finally, the conclusions and prospects are made. It is proposed that the future work should focus on the improvements in respect of constraint reduction, constraint solutions reuse, parallel solving, solving configuration prediction, etc. © 2019, Editorial Department of Transaction of Beijing Institute of Technology. All right reserved.

引用

页码：957 / 966

页数：9

共 55 条

[1]

Barrett C., Sebastiani R., Seshia S., Et al., Satisfiability modulo theories, Handbook of Satisfiability, (2009)

[2]

Stump A., Barrett C.W., Dill D.L., CVC: A cooperating validity checker, International Conference on Computer Aided Verification, pp. 500-504, (2002)

[3]

De-Moura L., Bjorner N., Z3: an efficient SMT solver, International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337-340, (2008)

[4]

STP (simple theorem prover)

[5]

An SMT solver

[6]

MathSat

[7]

SMT-COMP: the satisfiability modulo theories competition

[8]

Boyer R.S., Elspas B., Levitt K.N., Select-a formal system for testing and debugging programs by symbolic execution, Acm Sigplan Notices, 10, 6, pp. 234-245, (1975)

[9]

Clarke L.A., A program testing system, Proceedings of the 1976 Annual Conference, pp. 488-491, (1976)

[10]

Howden W.E., Symbolic testing and the DISSECT symbolic evaluation system, IEEE Transactions on Software Engineering, SE-3, 4, pp. 266-278, (1977)

← 1 2 3 4 5 6 →