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

Accurate Compiler and Optimization Independent Function Identification Using Program...

Derrick McKee (Purdue University), Nathan Burow (MIT Lincoln Laboratory), Mathias Payer (EPFL)

Read More

All things Binary

Dr. Sergey Bratus, DARPA PI and Research Associate Professor at Dartmouth College

Read More

Symbolic Path Tracing to Find Android Permission-Use Triggers

Kristopher Micinski (Haverford College), Thomas Gilray (University of Alabama, Birmingham), Daniel Votipka (University of Maryland), Michelle L. Mazurek (University of Maryland), Jeffrey S. Foster (Tufts University)

Read More

It Doesn’t Have to Be So Hard: Efficient Symbolic...

Vaibhav Sharma (University of Minnesota), Navid Emamdoost (University of Minnesota), Seonmo Kim (University of Minnesota), Stephen McCamant (University of Minnesota)

Read More