基於蒙地卡羅樹搜尋法之符號執行路徑探索機制

Abstract

符號執行(symbolic execution)在程式測試與分析領域已被廣泛運用。由於符號執行會紀錄並模擬程式執行時的路徑，模擬次數會以指數級成長，可能耗盡所有運算資源，稱為路徑爆炸問題(path explosion problem)；我們因此在有限的資源內調整搜尋策略，優先計算較有價值的路徑。在本篇論文中，我們提出以蒙地卡羅搜尋樹為基礎的方法，為目前第一個將此演算法套用至符號執行的研究。我們評估方法的效能，比較與其他傳統策略如深度優先搜尋(DFS)、廣度優先搜尋(BFS)的效率。在實驗中，我們分別限制時間和空間資源使用量，以評估效能。在小規模測試中，我們的方法較傳統策略約有40%的效能成長。而大規模測試中，我們的方法更達到2.8倍的效能成長。

Symbolic execution is a widely used technique in program testing and analysis. When a program executes in symbolic traces, it emulates all possible paths, resulting in exponential growth of the number of states with the path explosion problem. We therefore propose a strategy within the limited resources to give priority to favorite paths. In this paper, we use the Monte Carlo tree search(MCTS) based strategy to resolve the problem and compare it with other methods such as depth-first search (DFS) and breadth-first search (BFS). We perform different scales of experiments based on constraints of time and space resource. For smaller test cases, we found MCTS performs averagely 1.4 times better in block discovery rate than BFS and DFS. In addition, for larger test cases, MCTS shows 2.8 times better in block discovery rate than DFS and BFS averagely.