符號執行

符號執行（英語：symbolic execution）是一種電腦科學領域的程式分析技術，通過採用抽象的符號代替精確值作為程式輸入變數，得出每個路徑抽象的輸出結果。這一技術在硬體、底層程式測試中有一定的應用，能夠有效的發現程式中的漏洞。

這一思想最初由IBM托馬斯·J·華森研究中心的詹姆斯·C.金（James C. King） 於1976年6月在論文Symbolic Execution and Program Testing中提出，文中「解析程式的路徑後，用符號類比通過路徑並獲得輸出」的方法如今被稱為「經典符號執行」。由於20世紀80年代的研究追求分析的完備性，而大型程式的路徑複雜，不可能完全遍歷，符號執行這一研究領域遇冷。21世紀後，該領域研究有了新的進展：2006年，克里斯蒂安·卡達爾（Cristian Cadar）在論文中設計了一種「先進行符號執行，後根據符號執行結果生成測試用例」的「執行生成測試」技術，並隨後將其發展為應用在GNU/Linux核心錯誤檢查中的KLEE；2007年，庫希克·森（Koushik Sen）在當年的軟體工程自動化（Automated Software Engineering）會議提出將符號執行和實際執行結合的「混合執行（Concolic testing）」方法；2009年，維塔利·奇波諾夫（Vitaly Chipounov）提出「選擇性符號執行」方法，通過選擇「對程式設計者有意義」的執行分支進行符號執行測試來提高對大型程式應用符號執行測試的可行性。

符號類比技術（symbolic simulation）則把類似的思想用於電路分析；符號計算（Symbolic computation）則用於數學表達式分析。

符號執行引擎

符號執行引擎是符號執行技術的實現產物，可以用於對程式進行符號執行。一個基本的符號執行引擎由下列部分組成：

1. 狀態資訊記憶體：儲存下列符號執行所需狀態資訊。
   1. $pc$：指向需要處理的下一條程式語句,其可以是賦值語句、條件分支語句或者是跳轉語句；
   2. $\pi$：指代路徑約束資訊,表示為執行到程式特定語句需要經過的條件分支，以及各分支處關於符號值$a_{i}$的表達式;
   3. $\sigma$：表示與程式變數相關的符號值集.
2. 語句執行器：執行每一條語句來取得該程式的控制流程。
3. 約束解算器（英語：constraint solver）：用於在一條路徑的符號執行結束後解算路徑約束與符號執行結果，為開發者提供一個可供實際執行（英語：concret execution）的值

實例

請看下列代碼：

int f() {
  y = read();
  z = y * 2;
  if(z == 12){
    fail();
  }else{
    printf("OK");
  }
}

實際執行時，該方法讀入一個值儲存於變數y，當y的值為6時，該方法呼叫fail()，反之列印OK。

在符號執行時，程式讀入一個符號值λ，並將 λ * 2 賦值給 z。當執行到 if 條件判斷語句，由於無法判斷 λ * 2 == 12是否為真，符號執行引擎將執行「為真」與「為假」兩種分支。執行時，引擎將判斷語句處的程式環境與路徑約束複製一份並應用於兩條分支。本例中， fail() 分支的路徑約束指的是判斷條件 λ * 2 == 12 ，而print("OK")分支的路徑約束為 λ * 2 != 12。路徑結束時，約束解算器計算並得出一個對此路徑有意義（即能夠完成該分支的）輸入變數實際值。該值可供幫助開發者復現錯誤時進行實際執行使用。本例中，fail()分支的一個約束結算結果是6。

局限性

路徑爆炸

大多數符號執行方法不適用於大型程式：隨著程式規模的擴大，程式中有意義的路徑成指數級擴大。有些程式中存在無盡迴圈或遞迴呼叫，這更大大增加了有意義路徑，提高了符號執行難度。 為解決此問題，馬健強（音譯，Kin-Keung Ma）等人提出使用啟發式路徑搜尋演算法提高代碼覆蓋率；馬特·斯塔特斯（Matt Staats）等人提出並列執行獨立路徑的方法來降低符號執行耗時； 庫茲涅佐夫等人則提出了合併相似分支的方法緩解路徑爆炸問題。

待測程式輸入變數的特點

由於利用路徑分析進行程式分析，對於輸入變數範圍大，但程式分支較少的程式，符號執行方法比對輸入變數進行分析的方法（如動態程式分析）具有較強優勢。但是對於輸入變數變化範圍小，程式分支多的程式，符號執行的效率較低。

主記憶體位址存在別名

由於符號執行根據主記憶體位址分析變數及其變化，對於有主記憶體位址別名的程式，符號執行引擎將難以區分不同別名，因此執行結果可能有偏差。需要使用分離邏輯進行處理。

陣列的處理

由於陣列是大量不同值（如主記憶體位址）的集合，符號執行引擎需要選擇將陣列作為一個單獨的完整變數處理還是將每一個陣列元素作為單獨的變數處理。由於引擎無法得知程式中每個陣列的意義，動態確定每個陣列的類型十分具有挑戰性。

存在執行環境互動

當某一程式（如下代碼所示）與超出符號執行引擎控制的執行環境有互動（如進行系統呼叫並取得系統呼叫返回資訊等）時，符號執行將難以完成：

int main()
{
  FILE *fp = fopen("doc.txt");
  ...
  if (condition) {
    fputs("some data", fp);
  } else {
    fputs("some other data", fp);
  }
  ...
  data = fgets(..., fp);
}

該程式將打開一個檔案，並根據條件將不同類型的資料寫入該檔案，然後回讀已寫入的資料。 從理論上講，符號執行引擎將在第5行產生兩個路徑並在第11行返回與在condition變數中的值一致的資料。然而檔案操作被實現為核心中的系統呼叫，符號執行工具無法控制其行為。 解決這一挑戰的主要方法是：

在符號執行過程中直接執行系統呼叫：這種方法的優點是實現起來很簡單；缺點是這種呼叫「並不是符號執行」，其返回內容是實際執行的真實值。

對執行環境建模： 引擎使用模型類比系統呼叫，其優點是，能夠得到正確的符號執行結果；缺點是需要實現和維護許多可能用到的系統呼叫模型。 KLEE、Cloud9和Otter 等工具通過實現檔案系統操作、通訊端、IPC等模型採用了這種方法。

建立整個執行環境的狀態分支：基於虛擬機器技術的符號執行工具通過建立整個VM狀態的分支來解決環境問題。比如S2E中，每個符號執行狀態都是一個獨立的虛擬機器快照。這種方法的空間複雜度較高，對主記憶體的消耗很大。