Shiqi Shen (National University of Singapore), Shweta Shinde (National University of Singapore), Soundarya Ramesh (National University of Singapore), Abhik Roychoudhury (National University of Singapore), Prateek Saxena (National University of Singapore)
Symbolic execution is a powerful technique for
program analysis. However, it has many limitations in practical
applicability: the path explosion problem encumbers scalability,
the need for language-specific implementation, the inability to
handle complex dependencies, and the limited expressiveness of
theories supported by underlying satisfiability checkers. Often,
relationships between variables of interest are not expressible
directly as purely symbolic constraints. To this end, we present
a new approach—neuro-symbolic execution—which learns an
approximation of the relationship between program values of
interest, as a neural network. We develop a procedure for checking
satisfiability of mixed constraints, involving both symbolic
expressions and neural representations. We implement our new
approach in a tool called NeuEx as an extension of KLEE, a
state-of-the-art dynamic symbolic execution engine. NeuEx finds
33 exploits in a benchmark of 7 programs within 12 hours. This
is an improvement in the bug finding efficacy of 94% over vanilla
KLEE. We show that this new approach drives execution down
difficult paths on which KLEE and other DSE extensions get
stuck, eliminating limitations of purely SMT-based techniques.