概述

傳統符號執行是一種靜態分析技術，最初在1976年由King JC在ACM上提出。即通過使用抽象的符號代替具體值來模擬程式的執行，當遇到分支語句時，它會探索每一個分支, 將分支條件加入到相應的路徑約束中，若約束可解，則說明該路徑是可達的。符號執行的目的是在給定的時間內，儘可能的探索更多的路徑。根據執行的目的來分，主要有兩個：

從測試的角度來看，它可以模擬出各個路徑的輸入值，從而建立高覆蓋率的測試套件。這裡是靜態的分析程式得到測試需要的輸入，與動態執行程式的測試不同，動態執行程式的測試更多的是依賴完備的測試用例來提升測試的覆蓋率，達到發現問題的目的。

從缺陷查詢的角度來看，它為開發人員提供了觸發的缺陷的具體輸入，利用該輸入，程式可用於缺陷的確認或除錯。符號執行不僅限於查詢諸如緩衝區溢位之類的問題，而且可以通過根據缺陷發現的條件，生成複雜的斷言，來判斷缺陷發生的可能性。

符號執行的優勢是能夠以儘可能少的測試用例集達到高測試覆蓋率, 從而挖掘出複雜軟體程式的深層錯誤。然而, 在實際的軟體測試應用過程中, 不可避免地會遇到許多限制條件, 如路徑爆炸問題、約束求解困難集記憶體建模等問題, 這會導致符號執行難以在現實的軟體測試應用中達到理想的效果。

符號執行經過了傳統符號執行（我理解就是Static Symbolic Execution）→動態符號執行(dynamic symbolic execution,也叫Concolic Execution)→選擇性符號執行（Selective symbolic execution）的發展過程,動態符號執行包括混合測試 （Concolic Testing）和執行生成測試（Execution-Generated Testing(EGT)）兩種。

這裡是《符號執行研究綜述》中的觀點，實際中可能選擇性符號執行是比較新的一種符號執行方式，但不能說是一定優於動態符號執行的下一代技術。

static symbolic execution傳統符號執行

傳統符號執行的關鍵是使用符號值替代具體的值作為輸入，並將程式變數的值表示為符號輸入值的符號表達式。其結果是程式計算的輸出值被表示為符號輸入值的函式。

在遇到程式分支指令時, 程式的執行也相應地搜尋每個分支, 分支條件被加入到符號執行儲存的符號路徑約束 PC, PC表示當前路徑的約束條件。在收集了路徑約束條件之後, 使用約束求解器來驗證約束的可解性, 以確定該路徑是否可達。若該路徑約束可解, 則說明該路徑是可達的;反之, 則說明該路徑不可達, 結束對該路徑的分析。

函式 testme() 有 3 條執行路徑，組成右邊的執行樹。執行路徑(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）和符號路徑約束 PC（path constraint (or path condition)），其中 σ 表示變數到符號表達式的對映，PC 是符號表示的不含量詞的一階表示式。在符號執行的初始化階段，σ 被初始化為空對映，而 PC 被初始化為 true，並隨著符號執行的過程不斷變化。在對程式的某一路徑分支進行符號執行的終點，把 PC 輸入約束求解器（constraint solver）以獲得求解，生成實際的輸入值。如果程式把生成的具體值作為輸入執行，它將會和符號執行執行在同一路徑，即此時PC的公式所表示的路徑，並且以同一種方式結束。

例如上面的例子。

符號執行開始時，符號狀態 σ 為空，符號路徑約束 PC 為 true。

當我們遇到一個讀語句，形式為var=sym input()，即接收程式輸入，符號執行就會在符號狀態 σ 中加入一個對映 var->s，這裡s就是一個新的未約束的符號值。main()函式，16，17行會得到結果σ= {x ↦x0，y ↦ y0}，其中x0，y0是兩個初始不受約束的符號值；

當遇到一個賦值語句 v = e 時，符號執行就會在符號狀態 σ 中加入一個 v 到 σ(e) 的對映，於是程式執行完第 6 行後得到 σ = {x->x0, y->y0, z->2y0}。

當每次遇到條件語句 if(e) S1 else S2 時，PC 會被更新為 PC∧σ(e)，表示 then 分支，同時生成一個新的路徑約束 PC’，初始化為 PC∧¬σ(e)，表示 else 分支。

如果 PC 是可滿足的，那麼程式會走 then 分支（σ 和 PC），否則如果 PC’ 是可滿足的，那麼程式會走 else 分支（σ 和 PC’）。值得注意的是，符號執行不同於實際執行，其實兩條路都會走，分別維護它們的狀態。

如果 PC 和 PC’ 都不能滿足，那麼符號執行就在對應的路徑終止。

第 7 行建立了符號執行例項，路徑約束分別是 x0 = 2y0 和 x0 ≠ 2y0，在第 8 行又建立了兩個例項，分別是 (x0 = 2y0)∧(x0 > y0 + 10) 和 (x0 = 2y0)∧(x0 ≤ y0 + 10)。

如果符號執行遇到了 exit 語句或者 error，當前例項會終止，並利用約束求解器對當前路徑約束求出一個可滿足的值，這個值就構成了測試輸入：如果程式輸入了這些實際的值，就會在同樣的路徑結束。例如Figure2中三個綠色塊裡的值。

如果符號執行的程式碼包含迴圈或遞迴，且它們的終止條件是符號化的，那麼可能就會導致產生無數條路徑。如Figure3。這段程式碼就有無數條執行路徑，每條路徑的可能性有兩種：要麼是任意數量的true加上一個false結尾，要麼是無窮多數量的false。我們形式化地表示包含n個true條件和1個false條件的路徑，其符號化約束如下。其中每個 Ni 都是一個新的符號值，執行結束的符號狀態為 {N->Nn+1, sum->Σi∈[1,n]Ni}。在實踐中我們需要通過一些方法限制這樣的搜尋，例如timeout，限制路徑數量，迴圈迭代次數或探測深度。

經典的符號執行有一個關鍵的缺點，若符合執行路徑的符號路徑約束無法使用約束求解器進行有效的求解，則無法生成輸入。例如Figure2對應 twice 函式替換成Figure4. 那麼符號執行會得到路徑約束 x0 ≠ (y0y0)mod50 和 x0 = (y0y0)mod50。更嚴格一點，如果我們不知道 twice 的原始碼，符號執行將得到路徑約束 x0 ≠ twice(y0) 和 x0 = twice(y0)。在這兩種情況下，符號執行都不能生成輸入值。

Dynamic symbolic execution（Concolic Execution）

混合實際執行和符號執行，稱為concolic execution，是真正意義上的動態符號執行。

經典的符號執行，過度的依賴了符號執行的約束求解能力，限制了傳統符號執行的能力發揮。如果能加入具體值進行分析，將大大簡化分析過程，降低分析的難度和提升效率；但分析過程中，仍不可避免的還是需要將各種條件表示式，進行符號化抽象後變成約束條件參與執行。將程式語句轉換為符號約束的精度，對符號執行所達到的覆蓋率以及約束求解的可伸縮性會產生重大影響。所以如何做好混合具體(Concrete)執行和符號(Symbolic)執行的能力的平衡，就成為現代符號執行的關鍵點。

Concolic Testing

最早將實際執行和符號執行結合起來的是2005年發表的DART，全稱為“Directed Automated Random Testing”，以及2005年發表的CUTE，即“A concolic unit testing engine for C”。

Concolic執行維護一個實際狀態和一個符號化狀態：實際狀態將所有變數對映到實際值，符號狀態只對映那些有非實際值的變數。Concolic執行首先用一些給定的或者隨機的輸入來執行程式，收集執行過程中條件語句對輸入的符號化約束，然後使用約束求解器去推理輸入的變化，從而將下一次程式的執行導向另一條執行路徑。簡單地說來，就是在已有實際輸入得到的路徑上，對分支路徑條件進行取反，就可以讓執行走向另外一條路徑。這個過程會不斷地重複，加上系統化或啟發式的路徑選擇演算法，直到所有的路徑都被探索，或者使用者定義的覆蓋目標達到，或者時間開銷超過預計。

仍以figure2中例子為例。Concolic執行會先產生一些隨機輸入，例如{x=22, y=7}，然後同時實際地和符號化地執行程式。這個實際執行會走到第7行的else分支，符號化執行會在實際執行路徑生成路徑約束x ≠ 2y0（結束）。然後 Concolic 執行會將該路徑約束的連線詞取反，求解 x0 = 2y0 得到測試輸入 {x = 2, y = 1}，這個新輸入就會讓執行走向一條不同的路徑。concolic執行會在這個新的測試輸入上再同時進行實際的和符號化的執行，執行會取與此前路徑不同的分支，即第7行的then分支和第8行的else分支，這時產生的約束是 (x0 = 2y0)∧(x0 ≤ y0 + 10)（結束）。通過對將結合項 (x0 ≤ y0 + 10) 取反得到的約束 (x0 = 2y0)∧(x0 > y0 + 10) 進行求解，得到測試輸入 {x = 30, y = 15}，然後程式到達了 ERROR 語句。這樣程式的所有 3 條路徑就都探索完了，其使用的策略是深度優先搜尋。

Execution-Generated Testing(EGT)

     Cristian Cadar在2006年發表EXE，以及2008年發表EXE的改進版本KLEE，對上述concolic執行的方法做了進一步優化。其創新點主要是在實際狀態和符號狀態之間進行區分，稱之為執行生成的測試（Execution-Generated Testing），簡稱EGT。

EGT 在每次執行前會動態地檢查所涉及的值（比如語句、函式引數）是不是都是實際的值，如果是，則程式按照原樣執行（即直接把實際值帶入，然後像普通語句、函式一樣執行），否則，如果至少有一個值是符號值，程式會通過更新當前路徑的條件符號化地執行。例如上面的例子，把 17 行的 y = sym_input() 改成 y = 10，那麼第 6 行就會用實參10去呼叫 twice 函式，就像普通程式那樣執行。然後第 7 行將變成 if(20 == x)，因為這裡x是一個符號值，所以符號化執行。符號執行會通過新增約束 x = 20，走 then 分支，同時新增約束 x ≠ 20，走 else 分支。而在 then 分支上，第 8 行變成了 if(x > 20)，不會到達 ERROR。

concolic執行的出現，讓傳統靜態符號執行遇到的很多問題能夠得到解決——那些符號執行不好處理的部分、求解器無法求解的部分，用實際值替換就好了。使用實際值，可以讓因外部程式碼互動和約束求解超時造成的不精確大大降低，但付出的代價就是，會有丟失路徑的缺陷，犧牲了路徑探索的完全性。

selective symbolic execution選擇性符號執行

受路徑爆炸和約束求解問題的制約, 符號執行不適用於程式規模較大或邏輯複雜的情況, 並且對於與外部執行環境互動較多的程式尚無很好的解決方法。選擇性符號執行有助於解決這類問題, 也是具體執行和符號執行混合的一種分析技術, 依據特定的分析, 決定符號執行和具體執行的切換使用。

在選擇性符號執行中, 使用者可以指定一個完整系統中的任意部分進行符號執行分析, 可以是應用程式、庫檔案、系統核心和裝置驅動程式等。選擇性符號執行在符號執行和具體執行間轉換, 並透明地轉換符號狀態和具體狀態。選擇性符號執行極大地提高了符號執行在實際應用中對大型軟體分析測試的可用性, 且不再需要對這些環境進行模擬建模。

選擇性符號執行在指定區域內的符號化搜尋, 就是完全的符號執行, 在該區域之外均使用具體執行完成。選擇性符號執行的主要任務就是在分析前將大程式區分為具體執行區域和符號執行區域。

主要挑戰和解決方法

符號執行存在路徑爆炸（程式碼規模、複雜度）、約束求解（計算演算法）、記憶體模型（工具設計）等挑戰。

Path Explosion路徑爆炸

由於在每一個條件分支都會產生兩個不同約束，符號執行要探索的執行路徑依分支數指數增長。在時間和資源有限的情況下，應該對最相關的路徑進行探索。通過路徑選擇的方法緩解指數爆炸問題，主要有兩種方法：啟發式地優先探索最值得探索的路徑，並使用合理的程式分析技術來降低路徑探索的複雜性。

啟發式搜尋是一種路徑搜尋策略，大多數啟發式的主要目標在於獲得較高的語句和分支的覆蓋率，不過也有可能用於其他優化目的。一種有限的方法是使用靜態控制流圖來知道探索，儘量選擇與未覆蓋指令最接近的路徑。另一種啟發式方法是隨機探索，即在兩邊都可行的符號化分支處隨機選擇一邊。另一個方法是符號執行與進化搜尋相結合，其fitness function用來指導輸入空間的搜尋，其關鍵就在於fitness function的定義，例如利用從動態或靜態分析中得到的實際狀態資訊或者符號資訊來提升fitness function。

用程式分析和軟體驗證的思路去減少路徑探索的複雜性。一個簡單的方法是，通過靜態融合減少需要探索的路徑，具體說來就是使用select表示式直接傳遞給約束求解器，但實際上是將路徑選擇的複雜性傳遞給了求解器，對求解器提出了更高的要求。還有一種思路是重用，即通過快取等方式儲存函式摘要，可以將底層函式的計算結果重用到高階函式中，不需要重複計算，減小分析的複雜性。還有一種方法是剪枝冗餘路徑，RWset技術的關鍵思路就是，如果程式路徑與此前探索過的路徑在同樣符號約束的情況下到達相同的程式點，那麼這條路徑就會從該點繼續執行，所以可以被丟棄。

Constraint Solving約束求解

約束求解器優化。兩種優化方法：不相關約束消除（Irrelevant constraint elimination），增量求解（Incremental solving.）。

通常一個程式分支只依賴於一小部分的程式變數，因此一種有效的優化是從當前路徑條件中移除與識別當前分支不相關的約束。例如，當前路徑的條件是：(x + y > 10)∧(z > 0)∧(y < 12)∧(z - x = 0)，我們想通過求解 (x + y > 10)∧(z > 0)∧¬(y < 12)探索新的路徑，其中 ¬(y < 12) 是取反的條件分支，那麼我們就可以去掉對z的約束，因為對分支是不會有影響的。減小的約束集會給出x和y的新值，我們用此前執行的z值就可以生成新輸入了。如果更形式化地說，演算法會計算在取反條件所依賴的所有約束的傳遞閉包。

符號執行生成的約束集有一個重要的特徵，就是它們被表示為程式原始碼中的靜態分支的固定集合。所以，多個路徑可能會產生相似的約束集，所以可以使用相似的解決方案。通過重用以前相似請求得到的結果，可以提升約束求解的速度，這種方法被運用到了 CUTE 和 KLEE 中。在 KLEE 中，所有的請求結果都儲存在快取裡，該快取將約束集對映到實際的變數賦值。例如，在快取中有這樣一個對映：(x + y < 10)∧(x > 5) => {x = 6, y = 3}。利用這些對映，KLEE 可以迅速地解決一些相似的請求，例如請求 (x + y < 10)∧(x > 5)∧(y ≥ 0)，KLEE 可以迅速檢查得到 {x = 6, y = 3} 是可行的。

Memory Modeling記憶體建模

在訪問記憶體的時候，記憶體地址用來引用一個記憶體單元，當這個地址的引用來自於使用者輸入時，記憶體地址就成為了一個表示式。當符號化執行時，我們必須決定什麼時候將這個記憶體的引用進行實際化（看作實際值而非符號）。例如，一個memory model將int變數用某個實際值表示，可能會便於約束求解，但是會造成發現不了算術溢位。

別名問題，即地址別名導致兩個記憶體運算引用同一個地址，比較好的方法是進行別名分析，事先推理兩個引用是否指向相同的地址，但這個步驟要靜態分析完成。KLEE使用了別名分析和讓SMT考慮別名問題的混合方法。而DART和CUTE壓根沒解決這個問題

符號化跳轉也是一個問題，主要是switch這樣的語句，常用跳轉表實現，跳轉的目標是一個表示式而不是實際值。三種處理方法。1）使用concolic執行中的實際化策略，一旦跳轉目標在實際執行中被執行，就可以將符號執行轉向這個實際路徑，但缺陷是實際化導致很難探索完全的狀態空間，只能探索已知的跳轉目標。2）使用SMT求解器。當我們到達符號跳轉時，假設路徑謂詞為Π，跳轉到e，我們可以讓SMT求解器找到符合Π∧e的答案。但是這種方案效率低。3）使用靜態分析，推理整個程式，定位可能的跳轉目標。實際中，原始碼的間接跳轉分析主要是指標分析，而二進位制的跳轉分析，推理在跳轉目標表達式中哪些值可能被引用。例如，函式指標表，通常實現為，可能的跳轉目標表。

Handling Concurrency處理併發

大型程式通常是併發的，併發固有的非確定性，導致普通測試很困難。而動態符號執行適用於這類測試。

Symbolic execution for software testing: three decades later中舉了一些例子.

歷史發展和最新進展

符號執行最初提出是在70年代中期，靜態符合執行的原理。到了2005年左右開始重新流行，引入了一些新的技術讓符號執行更加實用。Concolic執行的提出讓符號執行真正成為可實用的程式分析技術，並且大量用於軟體測試、逆向工程等領域。

2005年作用湧現出很多工作，如DART、CUTE、EGT/EXE、CREST等等。真正值得關注和細讀的，應該是2008年Cristian Cadar開發的KLEE。KLEE可以是原始碼符號執行的經典作品，開源的，後來的許多優秀的符號執行工具都是建立在KLEE的基礎上。

基於二進位制的符號執行工具有2009年EPFL的George Candea團隊開發的S2E最為著名，其開創了選擇符號執行，S2E有開源的一個版本。2012年CMU的David Brumley團隊提出的Mayhem則採用了混合offline和online的執行方式。2008年UC Berkeldy的Dawn Song團隊提出的BitBlaze二進位制分析平臺中的Rudder模組使用了online的執行方式。

angr，是一個基於Python實現的二進位制分析平臺，完全開源且還在不斷更新，其中也實現了多種不同的符號執行策略。

在優化技術上， 2014年David Brumley團隊提出的路徑融合方法， Veritesting，是比較重要的工作之一，angr中也實現了這種符號執行方式（在靜態符號執行和動態符號執行間平衡，降低開銷）。2015年Stanford的Dawson Engler（Cristian Cadar的老師）團隊提出的Under-Constrained Symbolic Execution。

近年流行的符號執行與fuzzing技術相結合以提升挖掘漏洞效率，其實早在DART和2012年微軟的SAGE工作中就已經有用到這種思想，但這兩年真正火起來是2016年UCSB的Shellphish團隊發表的Driller論文，符號輔助的fuzzing（symbolic-assisted fuzzing），也非常值得一看。

參考文獻

[1] Schwartz E J, Avgerinos T, Brumley D. All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask) [C]// Security & Privacy. DBLP, 2010:317-331.

[2] Cadar C, Sen K. Symbolic execution for software testing: three decades later[M]. ACM, 2013.

[3] C. Cadar, D. Dunbar, and D. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI’08), volume 8, pages 209–224, 2008.

[4] R. S. Boyer, B. Elspas, and K. N. Levitt. SELECT – a formal system for testing and debugging programs by symbolic execution. SIGPLAN Not., 10:234–245, 1975.

[5] P. Godefroid, N. Klarlund, and K. Sen. DART: Directed Automated Random Testing. In PLDI’05, June 2005.

[6] K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. In ESEC/FSE’05, Sep 2005.

[7] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler. EXE: Automatically Generating Inputs of Death. In Proceedings of the 13th ACM Conference on Computer and Communications Security, pages 322–335, 2006.

[8] J. Burnim and K.Sen,“Heuristics for scalable dynamic test generation,” in Proc. 23rd IEEE/ACM Int. Conf. Autom. Software Engin., 2008, pp. 443–446.

[9] V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea. Selective Symbolic Execution. In Proceedings of the 5th Workshop on Hot Topics in System Dependability, 2009.

[10] S. K. Cha, T. Avgerinos, A. Rebert, and D. Brumley. Unleashing Mayhem on Binary Code. In Proceedings of the IEEE Symposium on Security and Privacy, pages 380–394, 2012.

[11] Song D, Brumley D, Yin H, et al. BitBlaze: A New Approach to Computer Security via Binary Analysis[C]// Information Systems Security, International Conference, Iciss 2008, Hyderabad, India, December 16-20, 2008. Proceedings. DBLP, 2008:1-25.

[12] Yan S, Wang R, Salls C, et al. SOK: (State of) The Art of War: Offensive Techniques in Binary Analysis[C]// Security and Privacy. IEEE, 2016:138-157.

[13] T. Avgerinos, A. Rebert, S. K. Cha, and D. Brumley. Enhancing Symbolic Execution with Veritesting. pages 1083–1094, 2014.

[14] D. a. Ramos and D. Engler. Under-Constrained Symbolic Execution: Correctness Checking for Real Code. In Proceedings of the 24th USENIX Security Symposium, pages 49–64, 2015.

[15] P. Godefroid, M. Y. Levin, and D. Molnar. SAGE: Whitebox Fuzzing for Security Testing. ACM Queue, 10(1):20, 2012.

[16] N. Stephens, J. Grosen, C. Salls, A. Dutcher, R. Wang, J. Corbetta, Y. Shoshitaishvili, C. Kruegel, and G. Vigna. Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In Proceedings of the Network and Distributed System Security Symposium, 2016.

[17] 葉志斌,嚴波. 符號執行研究綜述[J]. 電腦科學, 2018, 45(6A): 28-35.

[18] Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, Irene Finocchi: A Survey of Symbolic Execution Techniques. ACM Comput. Surv. 51(3): 50:1-50:39 (2018) 2017

參考部落格：

https://zhuanlan.zhihu.com/p/26927127

https://www.bookstack.cn/read/CTF-All-In-One/doc-8.9_symbolic_execution.md

https://zhuanlan.zhihu.com/p/282771772

https://blog.csdn.net/A951860555/article/details/119102789