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

Vault: Fast Bootstrapping for the Algorand Cryptocurrency

Derek Leung (MIT CSAIL), Adam Suhl (MIT CSAIL), Yossi Gilad (MIT CSAIL), Nickolai Zeldovich (MIT CSAIL)

Read More

NoDoze: Combatting Threat Alert Fatigue with Automated Provenance Triage

Wajih Ul Hassan (NEC Laboratories America, Inc.; University of Illinois at Urbana–Champaign), Shengjian Guo (Virginia Tech), Ding Li (NEC Laboratories America, Inc.), Zhengzhang Chen (NEC Laboratories America, Inc.), Kangkook Jee (NEC Laboratories America, Inc.), Zhichun Li (NEC Laboratories America, Inc.), Adam Bates (University of Illinois at Urbana–Champaign)

Read More

Balancing Image Privacy and Usability with Thumbnail-Preserving Encryption

Kimia Tajik (Oregon State University), Akshith Gunasekaran (Oregon State University), Rhea Dutta (Cornell University), Brandon Ellis (Oregon State University), Rakesh B. Bobba (Oregon State University), Mike Rosulek (Oregon State University), Charles V. Wright (Portland State University), Wu-Chi Feng (Portland State University)

Read More

Private Continual Release of Real-Valued Data Streams

Victor Perrier (Data61, CSIRO and ISAE-SUPAERO), Hassan Jameel Asghar (Macquarie University and Data61, CSIRO), Dali Kaafar (Macquarie University and Data61, CSIRO)

Read More