軟體除錯與符號執行整合互動

Abstract

由於軟體複雜度越來越高，大型軟體的程式規模已經超越人工測試的範圍。相較於傳統的測試與分析方法，符號執行(symbolic execution)能自動地產生符合條件的輸入資料，在一般情況下更能有效地分析與測試程式。因此符號執行的技術漸被廣泛應用。然而目前主要的符號執行系統(symbolic execution engine)在運用上缺乏互動機制，都必須預先撰寫腳本操控程式 (script)，指定找尋的路徑(path)或限制式(constraint)。無法停留在程式的特定執行點，藉以觀察程式、以適時調整符號執行的狀態。若要進行調整，必須重寫script、並重新執行，較缺乏彈性。 我們因此結合符號執行與除錯系統，在使用debugger進行動態分析(dynamic analysis)時，適時地使用符號執行來輔助使用者分析程式，大幅提升符號執行技術的實用性。我們經過評估，採用GDB除錯系統與Triton符號執行工具，透過python binding將兩者結合，實現軟體除錯與符號執行互動運用的概念。

As the software complexity is getting higher, the codebase of large-scale software is beyond the scope of manual testing. Compared to traditional software testing and analysis methods, symbolic execution is able to automatically generate the inputs that meet the constraints and test the program more efficiently. Therefore, symbolic execution has been widely applied in the testing and analysis of software. However, most of the symbolic execution engines lack interactive supports. We need to use the pre-written script to assign paths for exploration or constraints to be resolved. Users cannot stop the program at a specific execution stage, analyze the program, and adjust the symbolic execution state accordingly. It is impractical to rewrite the script, and restart the program for analysis and testing. We therefore combine software debugger with symbolic execution system. When the user launches the debugger to start dynamic analysis, they could use symbolic execution to aide analysis and largely improve the practicability. We have evaluated, through python binding, combining the gdb debug system and triton symbol execution tool, to achieve the interactive use of software debugging with symbolic execution.