符號執行

符號執行（英語：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中，每個符號執行狀態都是一個獨立的虛擬機快照。這種方法的空間複雜度較高，對內存的消耗很大。