基于深度学习的符号执行约束求解
软件工程
2020-03-19 v1
摘要
符号执行是一种强大的系统化软件分析技术，但受困于约束求解的高昂代价，而约束求解是影响符号执行有效性的关键支撑技术。诸如 Green 与 GreenTrie 的技术通过重用约束解来加速符号执行的约束求解；然而，这些重用技术需要约束间存在语法/语义等价或蕴含关系。本文引入 DeepSover，一种基于深度学习进行符号执行约束求解的新方法。我们的核心见解是利用一组约束解的集体知识训练深度神经网络，随后在符号执行过程中使用该网络对路径条件可满足性进行分类。实验评估表明 DeepSolver 在分类路径条件上高度准确，比最先进的约束求解与约束解重用技术更高效，并且能很好地支持符号执行任务。
引用
@article{arxiv.2003.08350,
title = {Constraint Solving with Deep Learning for Symbolic Execution},
author = {Junye Wen and Mujahid Khan and Meiru Che and Yan Yan and Guowei Yang},
journal= {arXiv preprint arXiv:2003.08350},
year = {2020}
}