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.

View More Papers

Life after Speech Recognition: Fuzzing Semantic Misinterpretation for Voice...

Yangyong Zhang (Texas A&M University), Lei Xu (Texas A&M University), Abner Mendoza (Texas A&M University), Guangliang Yang (Texas A&M University), Phakpoom Chinprutthiwong (Texas A&M University), Guofei Gu (Texas A&M University)

Read More

Time Does Not Heal All Wounds: A Longitudinal Analysis...

Meng Luo (Stony Brook University), Pierre Laperdrix (Stony Brook University), Nima Honarmand (Stony Brook University), Nick Nikiforakis (Stony Brook University)

Read More

NAUTILUS: Fishing for Deep Bugs with Grammars

Cornelius Aschermann (Ruhr-Universität Bochum), Tommaso Frassetto (Technische Universität Darmstadt), Thorsten Holz (Ruhr-Universität Bochum), Patrick Jauernig (Technische Universität Darmstadt), Ahmad-Reza Sadeghi (Technische Universität Darmstadt), Daniel Teuchert (Ruhr-Universität Bochum)

Read More

Unveiling your keystrokes: A Cache-based Side-channel Attack on Graphics...

Daimeng Wang (University of California Riverside), Ajaya Neupane (University of California Riverside), Zhiyun Qian (University of California Riverside), Nael Abu-Ghazaleh (University of California Riverside), Srikanth V. Krishnamurthy (University of California Riverside), Edward J. M. Colbert (Virginia Tech), Paul Yu (U.S. Army Research Lab (ARL))

Read More