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的全部內容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網站內容還不錯，歡迎將生活随笔推薦給好友。