神经符号执行：一种归纳式符号执行方法的可行性
编程语言
2018-07-03 v1
摘要
符号执行是一种强大的程序分析技术。然而，它在实际适用性方面存在诸多局限：路径爆炸问题妨碍可扩展性、需要特定语言的实现、无法处理复杂依赖关系，以及底层可满足性检查器所支持理论的表达能力有限。通常，感兴趣变量之间的关系无法直接或表示为纯符号约束。为此，我们提出一种新方法——神经符号执行（neuro-symbolic execution）——它将这种关系学习为神经网络的近似。其特点是一个能够求解混合约束的约束求解器，涉及符号表达式与神经网络表示。为此，我们将此类约束求解设想为结合 SMT 求解与基于梯度的优化的过程。我们展示了神经符号执行在构造缓冲区溢出漏洞利用中的效用。我们在 13/14 个具有困难约束、已知需要符号执行专门扩展的程序上报告了成功。此外，我们的技术在来自标准验证和不变量合成基准的 个程序中对给定的神经符号约束实现了 \% 的求解率。
引用
@article{arxiv.1807.00575,
title = {Neuro-Symbolic Execution: The Feasibility of an Inductive Approach to Symbolic Execution},
author = {Shiqi Shen and Soundarya Ramesh and Shweta Shinde and Abhik Roychoudhury and Prateek Saxena},
journal= {arXiv preprint arXiv:1807.00575},
year = {2018}
}