Sheng-Han Wen (National Taiwan University), Wei-Loon Mow (National Taiwan University), Wei-Ning Chen (National Taiwan University), Chien-Yuan Wang (National Taiwan University), Hsu-Chun Hsiao (National Taiwan University)

Constraint solving creates a serious performance bottleneck in symbolic execution. Examining a plethora of SMT solvers with diverse capabilities, we address the following research questions: How can the performance of symbolic execution improve if it can pick a priori the best solver for a given path constraint? How can such a prediction oracle be practically implemented? In this work, we first define the solver selection problem in symbolic execution and its evaluation metrics, and perform a preliminary study to gauge potential performance improvement through solver selection. We then present the design and implementation of Path Constraint Classifier (PCC), a machine learning based meta-solver that aims to reduce overall constraint solving latency by dynamically selecting a solver per query. Using machine learning seems straightforward, yet surprisingly underexplored; one main technical challenge is how to avoid excessive overhead introduced by feature extraction. We address this challenge by taking advantage of the structural characteristics of symbolic execution. Our experiments confirm that the overall solver time can be reduced by 10.3% in the KLEE dataset and 46% in the benchmark dataset, while the solver prediction procedure only accounts for 2% to 10% of overall solving time.

View More Papers

Detecting Obfuscated Function Clones in Binaries using Machine Learning

Michael Pucher (University of Vienna), Christian Kudera (SBA Research), Georg Merzdovnik (SBA Research)

Read More

Towards Parallel Binary Code Analysis

Xiaozhu Meng (University of Wisconsin-Madison)

Read More

dAngr: Lifting Software Debugging to a Symbolic Level

Dairo de Ruck, Jef Jacobs, Jorn Lapon, Vincent Naessens (DistriNet, KU Leuven, 3001 Leuven, Belgium)

Read More

o-glassesX: Compiler Provenance Recovery with Attention Mechanism from a...

Yuhei Otsubo (National Police Agency, Tokyo, Japan), Akira Otsuka (Institute of information Security, Japan), Mamoru Mimura (National Defense Academy, Japan), Takeshi Sakaki (The University of Tokyo, Japan), Hiroshi Ukegawa (National Police Agency, Tokyo, Japan)

Read More