作者 | 王祺昌 華東師范大學軟件工程學院碩士研究生

蘇亭 華東師范大學軟件工程學院教授

版塊 | 鑒源論壇 · 觀模

引言：測試用例自動生成，簡稱測試生成（Test Generation），是指針對給定的被測對象，例如代碼單元、接口、系統等，使用相關算法生成測試用例集合的方法。其本質是測試用例設計自動化，無需開發者手動設計測試用例。測試生成可分為黑盒和白盒，前者在不考慮程序本身的情況下為程序生成測試用例，而后者分析程序的源代碼或二進制代碼以生成測試用例，基于符號執行的測試生成是一種典型的白盒測試生成方法。

01 什么是符號執行（symbolic execution）

符號執行（symbolic execution）是一種經典的程序分析技術，使用抽象的符號值（symbolic value）而不是精確的具體值（concrete value）作為程序輸入，以此將程序變量的值表示為這些輸入的符號表達式。在符號執行期間的任何一點，符號執行引擎可以獲取到達該點的路徑約束，并通過約束求解器（constraint solver）求解約束以得到可以到達該點的具體值。

下面的簡單代碼片段將給出一個例子，假設ERROR語句對應程序中的一個漏洞，我們使用符號執行判斷是否有達到該語句的可能。符號執行會在給定的時間內，生成一組輸入來盡可能多的探索所有的執行路徑，程序的輸入包括兩個變量 x 和 y，因此符號執行會將它們都綁定到對應的符號值α和β，最終程序中的每個點都對應一組α和β組成的約束。

圖 1 符號執行代碼示例

符號執行結束后生成的計算樹如圖 2 所示，樹中的每個節點代表程序中的一個條件語句，每個邊代表一組非條件語句的執行，每條路徑代表從程序開始到路徑終點的一條執行路徑，通過為每條路徑求解對應的路徑約束，就可以判斷該路徑是否可行，并為可行路徑生成對應的程序輸入。

ERROR 語句對應的路徑約束為（2*β==α ^ α<=β+10），求解該約束可得到一個可行解（α=4 ^ β=2），則(x =4, y=2)就是到達 ERROR 語句對應的程序輸入。

圖 2 程序對應的計算樹（computation tree）

02 符號執行的發展

符號執行的思想最早由 James C. King 在 1976 年發表的一篇論文[1]中提出，文中提出的“解析程序的路徑后，用符號模擬通過路徑并獲得輸出”的方法如今被稱為“經典符號執行”。

雖然符號執行技術最早在 70 年代就被提出，但未受到研究者的廣泛關注，直到 21 世紀才重新回到人們的視野中，這主要受兩個原因的限制。首先，符號執行在大型現實世界程序中的應用需要求解復雜而龐大的約束，而當時的約束求解器的求解能力限制了符號執行技術推廣，在過去十年中，涌現了了許多強大的約束求解器如 Z3 (de Moura and Bj?rner, 2008)[2], Yices (Dutertre and de Moura, 2006)[3], STP (Ganesh and Dill, 2007)[4]。其次，老一代計算機的計算能力有限，無法符號地執行大型程序，而今天的計算機比八十年代強大得多，這減少了符號執行應用于大型真實世界程序的障礙。

2006年，Cristian Cadar 設計了一種“先進行符號執行，后根據符號執行結果生成測試用例”的“執行生成測試”技術[5]，并隨后將其發展為應用在GNU/Linux 內核錯誤檢查中的 KLEE[6]。

2007年，Koushik Sen 提出將符號執行和實際執行結合的混合執行（Concolic Execution）[7]。

2009 年，Vitaly Chipounov 提出“選擇性符號執行”，通過選擇 “對程序設計者有意義”的執行分支進行符號執行測試來提高對大型程序應用符號執行測試的可行性。

如今符號執行已經被廣泛用于測試領域，其中最著名的用途是進行測試生成以提高代碼覆蓋率并發現程序錯誤，此外還被用于安全漏洞自動生成、負載測試、故障定位和回歸測試等。

03 符號執行進階

3.1 混合執行（Concolic Execution）

混合執行（Concolic Execution）已成為一種流行的符號執行方法，又稱為動態符號執行（Dynamic Symbolic Execution）或動態測試生成（Dynamic Test Generation） [8]。與經典符號執行不同，混合執行使用一個具體值作為輸入驅動程序運行，沿途收集路徑約束，當程序執行結束后通過對路徑約束上的不同分支取反來生成新路徑上的約束，交由約束求解器求解得到新的輸入，重復上述策略以覆蓋更多的路徑。

通過這種輸入迭代產生變種輸入的方法，理論上所有可行的路徑都可以被計算并分析。混合執行相較于經典符號執行的優勢在于每次執行都是基于具體值的而非模擬符號值的執行，從而顯著降低了符號執行的開銷，使得符號執行技術有能力處理更大規模的現實世界程序。

3.2 符號反向執行（Symbolic Backward Execution）

符號反向執行（SBE）是符號執行的一種變體[9]，它探索從程序中的特定目標點到程序的入口的路徑，因此其分析方向和傳統的正向符號執行相反。符號反向執行的主要目標是快速尋找可以到達程序中特定目標點（例如 assert 和 throw 語句）的測試用例，這對開發人員在對程序進行調試或回歸測試時非常有用。

04 符號執行的限制

符號執行理論上可以對程序可能的執行路徑進行詳盡的探索，也因此在處理現實世界的程序時遇到了一些挑戰：

(1) 路徑爆炸

大多數符號執行方法不適用于處理大型程序：隨著程序規模的擴大，程序中有意義的路徑數量成指數級增長。許多程序中還存在無限循環(infinite-loop)或遞歸調用，這大大增加了路徑條數，提高了符號執行的難度。

(2) 復雜約束

符號執行中的重要部分是對路徑約束的求解，但現實中存在一些復雜約束使得約束求解器難以求解（例如非線性算術運算、第三方庫函數等），這會顯示符號執行系統可以探索的路徑數量。

(3) 內存

符號執行引擎難以處理指針、數組等復雜對象，另外，由于符號執行根據內存地址分析變量及其變化，對于有內存地址別名的程序，符號執行引擎將難以區分不同別名，因此執行結果可能有偏差。

05 總結

符號執行作為一個經典的程序分析技術，在 21 世紀受到了研究者的廣泛重視，并為軟件測試提供了一個在白盒情況下精準和詳盡地測試程序的全新思路，近年來不斷出現新的符號執行技術和相關工具，被廣泛應用于測試生成、負載測試、故障定位以及回歸測試等場景。盡管取得了巨大進展，但符號執行仍然面臨現實世界大型程序中存在的許多挑戰，學術界和工業界也在不斷探索符號執行和其他技術相結合以提升執行性能的方式，例如將符號執行與模糊測試相結合以提升測試生成的精確性和可擴展性。

審核編輯：湯梓紅