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

Efficient Normalized Reduction and Generation of Equivalent Multivariate Binary...

Arnau Gàmez-Montolio (City, University of London; Activision Research), Enric Florit (Universitat de Barcelona), Martin Brain (City, University of London), Jacob M. Howe (City, University of London)

Read More

Detecting Obfuscated Function Clones in Binaries using Machine Learning

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

Read More

Evaluating Disassembly Ground Truth Through Dynamic Tracing (abstract)

Lambang Akbar (National University of Singapore), Yuancheng Jiang (National University of Singapore), Roland H.C. Yap (National University of Singapore), Zhenkai Liang (National University of Singapore), Zhuohao Liu (National University of Singapore)

Read More

BAR2019 Keynote Talk

Dustin Fraze, Program Manager, DARPA I2O

Read More