论文标题
通过深度学习象征性执行的约束解决
Constraint Solving with Deep Learning for Symbolic Execution
论文作者
论文摘要
符号执行是一种强大的系统软件分析技术，但遭受了约束解决的高成本，这是影响符号执行有效性的关键支持技术。诸如绿色和Greentrie重用解决方案之类的技术以加快象征性执行的约束解决方案；但是，这些重用技术需要约束之间的句法/语义等效性或含义关系。本文介绍了DeepSover，这是一种新颖的方法，可以通过深入学习象征性执行的深度学习来解决。我们的关键见解是利用一组约束解决方案的集体知识来培训深层神经网络，然后将其用于对路径条件进行分类，以使其在符号执行过程中的满意度。实验评估表明，DeepSolver在分类路径条件上非常准确，比最新的约束解决方案和约束解决方案重用技术更有效，并且可以很好地支持符号执行任务。
Symbolic execution is a powerful systematic software analysis technique, but suffers from the high cost of constraint solving, which is the key supporting technology that affects the effectiveness of symbolic execution. Techniques like Green and GreenTrie reuse constraint solutions to speed up constraint solving for symbolic execution; however, these reuse techniques require syntactic/semantic equivalence or implication relationship between constraints. This paper introduces DeepSover, a novel approach to constraint solving with deep learning for symbolic execution. Our key insight is to utilize the collective knowledge of a set of constraint solutions to train a deep neural network, which is then used to classify path conditions for their satisfiability during symbolic execution. Experimental evaluation shows DeepSolver is highly accurate in classifying path conditions, is more efficient than state-of-the-art constraint solving and constraint solution reuse techniques, and can well support symbolic execution tasks.
