基於機器學習的求解器選擇增進符號執行效率

Abstract

本論文提出了一個符號執行引擎中的新元件：路經約束條件分類器 (Path Constraint Classfier)，這個元件主要透過對符號執行(Symbolic Execution) 中的路徑約束條件選擇最適當的求解器 (Constraint Solver) 以增進符號執行在約束條件求解上的效率。 在以往的符號執行中，通常一個符號執行引擎只會使用固定的一個求解器來進行求解，但根據我們初步的研究，不同的路徑約束條件都有著不同的特性，而當今熱門的求解器在不同的問題上也都有著不同的求解能力，若我們在對路徑約束條件求解時，可以先選擇一個最適合這個路徑約束條件的求解器，那符號執行的效率將可大大的提升。因此，本論文主要專注在這一點，實作了一個支援路徑約束條件分類的系統雛形，透過從符號執行引擎蒐集到的路徑約束條件，嘗試對其進行特徵抽取 (feature extraction)，並使用基於深度神經網路 (Deep Neural Network) 的機器學習模型進行求解器預測。 在我們的系統雛型中，我們提出了約束路徑特徵快取 (Constraint Feature Cache) 的優化方法，使得預測求解器上的額外時間花費可以大幅度降低。除此之外，我們還提出了邏輯選擇 (logic selection) 以及備援求解器 (backup solver) 兩個優化技巧，藉此提升我們的系統在約束路徑求解的能力。

Symbolic execution is a widely applied automated program analysis technique for test case generation and vulnerability discovery. Symbolic execution systematically explores possible program execution paths, represents each path as a set of constraints, and sends such constraints to an SMT solver for satisfilability check and input generation. Despite being a key enabler of symbolic execution, contraint solving can take up to 99% of total time [26] and thus becomes a serious performance bottleneck. Observing a plethora of SMT solvers with diverse capabilities, we seek to explore the following research questions: How much performance can symbolic execution gain if it can pick a priori the best solver for a given path contraint? How can such a prediction oracle be practically implemented? In this work, we first formally define the solver selection problem and its evaluation metrics, and perform a preliminary study to confirm that an performance improvement through solver selection is possible. 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. The idea of using machine learning seems straightforward yet surprisingly less explored, and we identify one main technical challenge being how to avoid excessive overhead introduced by machine learning, including feature extraction. We address this challenge by taking advantage of structural characteristics of symbolic execution, and our experiment confirms that by sacrificing a small amount of time on solver prediction procedure, more performance benefit can be obtained. Also, our solution can be seamlessly integrated with other optimization techniques (e.g., constraint simplification, query reduction, and improved solvers) to further improve the scalability of constraint solving in symbolic execution.