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

Monte Carlo Tree Search-based Path Exploration for Symbolic Execution

葉家郡(Jia-Jun Yeh)

指導教授 ： 黃世昆

國立交通大學/資訊學院/資訊科學與工程研究所/碩士(2017年)

摘要

符號執行(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.

並列關鍵字

Monte Carlo Tree Search ； Upper Confidence Bounds for Trees ； Symbolic Execution

參考文獻

[20] 陳盈伸. “符號執⾏之動態路徑修剪技術”. 英⽂. MA thesis. 臺灣⼤學, 2016, pp. 1– 49. doi: 10.6342/NTU201602958.

[1] David Silver et al. “Mastering the game of Go with deep neural networks and tree search”. In: Nature 529.7587 (2016), pp. 484–489.

[7] Sang Kil Cha et al. “Unleashing mayhem on binary code”. In: 2012 IEEE Symposium on Security and Privacy. IEEE. 2012, pp. 380–394.

[9] Leonardo de Moura and Nikolaj Bjørner. “Z3: An Efficient SMT Solver”. In: Tools and Algorithms for the Construction and Analysis of Systems: 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on 31 Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29- April 6, 2008. Proceedings. Ed. by C. R. Ramakrishnan and Jakob Rehof. Berlin, Heidelberg: Springer Berlin Heidelberg, 2008, pp. 337–340. isbn: 978-3-540-78800-3. doi: 10.1007/978-3-540-78800-3_24. url: http://dx.doi.org/10.1007/978- 3-540-78800-3_24.

[12] Yan Shoshitaishvili et al. “SoK: (State of) The Art of War: Offensive Techniques in Binary Analysis”. In: IEEE Symposium on Security and Privacy. 2016.