[符號執行-入門1]軟件測試中的符號執行

最近在自學符號執行，所以，這篇經典文章(Symbolic Execution for Software Testing: Three Decades Later)[1]做爲入門必讀。

• 0. 定義
• 1. 經典的符號執行
• 2. 現代符號執行技術
  • 2-1. 混合執行測試(Concolic testing)
  • 2-2. 執行生成測試(Execution-Generated Testing, EGT)
  • 2-3. 動態符號執行中的不精確性(imprecision) vs.完整性(completeness)
• 3. 主要挑戰和解決方案
  • 3-1. 路徑爆炸(Path Explosion)
  • 3-2. 約束求解(Constraint Solving)
  • 3-3. 內存建模(Memory Modeling)
  • 3-4. 併發控制(Handling Concurrency)
• 4. MISC
• 5. Reference:

0. 定義

符號執行 （Symbolic Execution）是一種程序分析技術，它能夠經過分析程序來獲得讓特定代碼區域執行的輸入。顧名思義，使用符號執行分析一個程序時，該程序會使用符號值做爲輸入，而非通常執行程序時使用的具體值。在達到目標代碼時，分析器能夠獲得相應的路徑約束，而後經過約束求解器來獲得能夠觸發目標代碼的具體值。

軟件測試中的符號執行主要目標是[1]：

在給定的探索儘量多的、不一樣的程序路徑(program path)。對於每一條程序路徑，
1) 生成一個具體輸入的集合(主要能力)；
2) 檢查是否存在各類錯誤(errors，包含assertion violations, uncaught exceptions, security vulnerabilities, and memory corruption)。

從測試生成的角度，符號執行能夠生成高覆蓋率的測試用例。
從bug finding的角度，符號執行能夠提供一個具體的輸入用於觸發bug（過去經常用於調試bug）。

1. 經典的符號執行

符號執行的主要思想就是將輸入(input)用符號來表徵而不是具體值，同時將程序變量表徵成符號表達式。所以，程序的輸出就會被表徵成一個程序輸入的函數，即fun(input)。在軟件測試中，符號執行被用於生成執行路徑(execution path)的輸入。
執行路徑(execution path)：一個true和false的序列seq={p0,p1,...,pn}。其中，若是是一個條件語句，那麼pi=ture則表示這條條件語句取true，不然取false。
執行樹(execution tree)：一個程序的全部執行路徑則可表徵成一棵執行樹。
以下圖所示：

對應的執行樹：

3條不一樣的執行路徑構成了一棵執行樹。三組輸入{x=0,y=1},{x=2,y=1},{x=30,y=15}覆蓋了全部的執行路徑。所以，符號執行的目標就是在給定的時間內，生成一個輸入的集合使得全部的（或讓儘量多的）執行路徑依賴於由符號表徵的輸入。

符號狀態(symbolic state)：符號執行維護一個符號狀態，它是一個<變量，符號表達式(symbolic expressions)>的mapping。

符號路徑約束(symbolic path constraint)： a quantifier-free first-order formula over symbolic expressions.

符號執行後的結果以下圖所示：

當代碼中包含循環和遞歸時，若是終止條件是符號的話，那麼符號執行會產生無限數量的執行路徑。例以下圖所示，

這個時候，符號路徑要麼就是一串有限長度的ture後面跟着一個false（跳出循環），要麼就是無限長的true。如圖所示，

符號執行的主要缺點：若是符號路徑約束不可解（不能被solver解決）或者是不能被高效（時間效率）的解，則不能生成input。回到以前的例子（見圖 ~\ref{example-program}），若是把函數twice改爲(v*v)%50（非線性）：

假設採用的sovler不可解非線性約束，那麼，符號執行將失敗，即沒法生成input。

2. 現代符號執行技術

現代符號執行技術的特色是同時執行精確(Concrete)執行和符號(Symbolic)執行。

2-1. 混合執行測試(Concolic testing)

當給定若干個具體的輸入時，Concolic testing動態地執行符號執行。Concolic testing會同時維護兩個狀態：

1. 精確狀態(concrete state): maps all variables to their concrete values.
2. 符號狀態(symbolic state): only maps variables that have non-concrete values.

不一樣於傳統的符號執行技術，因爲Concolic testing須要維護程序執行時的整個精確狀態，所以它須要一個精確的初始值。舉例說明，仍是以前這個例子：

表明工具：

1. DART: Directed Automated Random Testing[2]
2. Concolic testing[3]

2-2. 執行生成測試(Execution-Generated Testing, EGT)

EGT在執行每一個操做以前，檢查每一個相關的值是精確的仍是已經符號化了的，而後動態地混合精確執行和符號執行。若是全部的相關值都是一個實際的值（即精確的，concrete），那麼，直接執行原始程序（即，操做，operation）。不然（至少一個值是符號化的），這個操做將會被符號執行。舉例說明，假設以前那個例子，第17行改爲y=10。那麼，在調用twice時，傳入的參數是concrete的，返回的也是一個concrete value，所以z也是一個concrete value。第七、8行中的z和y+10也會被轉換成concrete vaule。而後再進行符號執行。

表明工具：

1. EXE[4]
2. KLEE[5]

因而可知，不管是concolic testing仍是EGT，他們都是動態地mix use concrete and symbolic execution。所以，也被稱做「動態符號執行」。

2-3. 動態符號執行中的不精確性(imprecision) vs.完整性(completeness)

不精確性:代碼調用了第三方代碼庫（因爲種種緣由沒法進行代碼插裝），假設傳入的參數都是concrete value，那麼就像EGT中的同樣，能夠所有看成concrete execution。即便傳入的參數中包含符號，動態符號執行仍是能夠對符號設一個具體的值。Concolic和EGT有不一樣的解決方法，後面再介紹。除了調用外部代碼，對於難以處理的操做數（如浮點型）或是一些複雜的函數（solver沒法解決或須要耗費大量時間），使用concrete value能夠幫助符號執行環節這種impression。
完整性:動態符號執行經過concrete value能夠簡化約束，從而防止符號執行get stuck。可是這也會帶來一個新問題，就是因爲這種簡化，它可能會致使一些不完整性，即有時候沒法對全部的execution path都能生成input。可是，當遇到不支持的操做或外部調用時，這顯然優於簡單地停止執行。

3. 主要挑戰和解決方案

3-1. 路徑爆炸(Path Explosion)

描述:
首先，要知道，符號執行implicitly過濾兩種路徑：

1. 不依賴於符號輸入的路徑；
2. 對於當前的路徑約束，不可解的路徑。
   可是，儘管符號執行已經作了這些過濾，路徑爆炸依舊是符號執行的最大挑戰。

解決方案:

1. 利用啓發式搜索搜索最佳路徑
   目前，主要的啓發式搜索主要focus在對語句和分支達到高覆蓋率，同時他們也可被用於優化理想的準則。
   • 方法1：利用控制流圖來guideexporation。
   • 方法2：interleave 符號執行和隨機測試。
   • 方法3（more recently）：符號執行結合演化搜索(evolutionary search)。其中，fitness function用於drive the exploration of the input space。
2. 利用可靠的(sound)程序分析技術來減少路徑爆炸的複雜度
   • 方法1：靜態地合併路徑，而後再feed solver。儘管這個方法在不少場合都有效，可是他把複雜度轉移給了solver，從而致使了下一個challenge，即約束求解的複雜度。
   • 方法2： 在後續的計算中，記錄並重用low-level function的分析結果。
   • 方法3 ： 自動化剪枝

3-2. 約束求解(Constraint Solving)

描述:
約束求解是符號執行的技術瓶頸。所以，對於solver的優化（提升solver的求解能力）成了解決這個技術瓶頸的手段。

解決方案:

1. 去除不相關的約束
   通常來講，程序分支主要依賴於一小部分的程序變量。也就是說，程序分支依賴於一小部分來自於路徑條件(path condition)的約束。所以，一種有效的方法就是去掉那些與當前分支的輸出不相關的路徑條件。例如，現有路徑條件：(x+y>10)^(z>0)^(y<12)^(z-x=0)。假設咱們如今想生成知足(x+y>10)^(z>0)^¬(y<12)，其中咱們想創建對¬(y<12)（與y有關）的feasibility。那麼，(z>0)和(z-x=0)這兩個約束均可以去掉，由於與y不相關。
2. 遞增求解
   核心思想就是緩存已經求解過的約束，例如(x+y<10)^(x>5)=>{x=6,y=3}。對於新的約束，首先判斷這個新約束的搜索空間是緩存里約束的超集仍是子集。若是是新的約束的搜索空間是緩存的約束的子集，那麼，就把緩存中的約束去掉多餘的條件後繼續求解。若是是超集，那麼直接把解代入去驗證。

3-3. 內存建模(Memory Modeling)

描述:
程序語句轉化成符號約束的精度對符號執行的覆蓋率有很大的影響。例如，內存建模是用一個具體的數值去近似一個固定位數的整數變量可能會頗有效，可是另外一方面，它也會致使imprecision，好比丟失一些符號執行的路徑，或探索一些無用的解。另外一個例子就是指針，一些工具如DART[3]只能處理精確的指針。

解決方案:
precision和scalability是一個trade-off。須要考慮的因素有：

1. 代碼是high level的application code仍是low-level的system code。
2. 不一樣的約束求解器的實際效果。

3-4. 併發控制(Handling Concurrency)

描述:
不少現實世界中的程序是併發的，這也意味着他們不少都是不肯定的(non-deteminism)。儘管如此，符號執行已經被有效地運用在測試併發系統，分佈式系統。

4. MISC

1. 符號執行的論文，教程，視頻，工具

後續，我會記錄一些step by step使用部分符號執行工具的blog。

5. Reference:

[1]: Symbolic Execution for Software Testing: Three Decades Later
[2]: DART: Directed Automated Random Testing
[3]: CUTE: A concolic unit testing engine for C
[4]: EXE: Automatically generating inputs of death
[5]: KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs