oid first ... net 復雜度 sys 遇到 部分 testing

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

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。第7、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。

4-1. 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

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