Symbolic execution for software testing: three decades later
背景介紹
技術難點
路徑探索約束求解內存建模
關鍵目標
生成一組具體的測試用例,執行該路徑檢查是否存在各種錯誤,包括內存斷言沖突、未捕獲的異常、安全漏洞和內存損壞
符號執行的優點
比傳統的動態執行技術更強大,不僅能夠發現一般性的錯誤,還能夠對復雜程序進行推理從測試生成來說,能夠生成高覆蓋率的測試用例從BUG尋找來說,能夠提供具體的測試用例,方便確認和調試錯誤
符號執行的缺點
如果判斷條件是一個輸入符號,會產生路徑爆炸(限制搜索的時間、路徑的深度、循環迭代的次數以及路徑的數量)純靜態的符號執行,可能存在約束路徑不能由求解器高效求解,比如判斷函數的原函數實現咋不到
聯合執行
隨機產生輸入數據,得到響應的路徑約束,然后取反得到對立的路徑約束如此反復聯合執行,可能會帶來路徑丟失,原因一樣,路徑約束不能求解聯合執行,還需要區分實際狀態和符號狀態
面臨的挑戰
路徑選擇
使用啟發式函數對路徑進行探索,先探索最值得探索的路徑使用一些可靠的程序分析的技術減少路徑探索的復雜度 約束求解
不相關約束消除(取反路徑后面的約束)增量求解(在前面的基礎上) 內存建模
程序語句如何翻譯為符號化約束 符號化跳轉 - 聯合執行,探索實際路徑
- SMT求解器,效率低
- 使用靜態分析
并發執行
考慮動態符號執行
開源的符號執行工具
KLEE
KLEE結構圖
組成
解釋模塊 將被測程序翻譯成LLVM(類似于RISC-V的精簡指令集),LLVM實際上是一種匯編語言。通過在翻譯好的LLVM指令中,加入一些功能函數的調用,在程序執行時,KLEE可以控制指令的執行過程,保存程序執行過程中的所有狀態,包括內存信息、寄存器值以及程序計數器等。 符號表示模塊 將程序的輸入變量全部用符號表示, 程序對變量操作統統體現在符號表上。當程序走到分支時,KLEE會將現有的信息進行復制,采用(COW(copy on write)的方式),復制只是對原對象的標記,只在對象發生變化時,才復制該對象并反映出變化。 約束求解模塊 KLEE在使用符號執行時,會收集當前路徑的約束條件。KLEE會對這些約束進行求解,得到具體的測試用例,在分支語句中,也可以用用例進行判斷。 路徑選擇模塊 在路徑執行時,KLEE將會保存所有經過約束求解但尚未執行的可行路徑信息(state),在一條路徑完成之后,該state會被標記為完成,被標記過的路徑將不再被選擇執行。路徑的選擇,有兩種方法包括隨機選擇和基于覆蓋率優化算法。 錯誤檢測模塊 當程序遇到讀寫錯誤或者崩潰時,KLEE會根據約束條件,生成會導致該錯誤的測試用例,并終止此次執行。特別的當遇到除數為0時,KLEE會添加路徑約束條件除數非0,繼續執行。在遇到讀寫指令時,KLEE將變量地址和變量大小作為約束條件,檢測是否存在內存越界。
ANGR
項目框架
組成
CLE模塊(cle loads everything) 將可執行程序加載進內存空間,它可以從ELF/PE文件中識別文件頭提取架構、代碼段、數據段等信息,接著會繼續加載程序的依賴文件,如so或者dll文件。 archinfo模塊 保存針對不同架構的指令集,例如x86、arm、mips以及powerc等,提供專用的類,包含對應的CPU架構模型，包括寄存器、位寬、大小端等數據結構 pyVEX模塊 將機器碼轉換為開源二進制插樁工具Valgrind所使用的中間語言VEX,這是因為angr可以處理不同架構的程序,因此需要一個中間語言進行分析 SimEngine 對VEX程序進行解釋和執行,支持具體值執行和符號值執行，執行時支持自定義函數Hook和斷點，支持自定義路徑探索策略 Claripy 將符號執行中生成的路徑約束轉化成SMT公式，使用Z3進行求解 SimOS 用于模擬程序與系統環境交互，提供了許多模擬的libc函數和系統調用，用戶也可以自行編寫Hook函數進行模擬
總結
以上是生活随笔為你收集整理的[fuzz论文阅读] Symbolic execution for software testing: three decades later的全部內容，希望文章能夠幫你解決所遇到的問題。
如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。
