基于符號執(zhí)行的測試生成

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

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

版塊 | 鑒源論壇 · 觀模

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

01 什么是符號執(zhí)行（symbolic execution）

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

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

圖 1 符號執(zhí)行代碼示例

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

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

圖 2 程序?qū)?yīng)的計算樹（computation tree）

02 符號執(zhí)行的發(fā)展

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

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

2006年，Cristian Cadar 設(shè)計了一種“先進行符號執(zhí)行，后根據(jù)符號執(zhí)行結(jié)果生成測試用例”的“執(zhí)行生成測試”技術(shù)[5]，并隨后將其發(fā)展為應(yīng)用在GNU/Linux 內(nèi)核錯誤檢查中的 KLEE[6]。

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

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

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

03 符號執(zhí)行進階

3.1 混合執(zhí)行（Concolic Execution）

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

通過這種輸入迭代產(chǎn)生變種輸入的方法，理論上所有可行的路徑都可以被計算并分析?；旌蠄?zhí)行相較于經(jīng)典符號執(zhí)行的優(yōu)勢在于每次執(zhí)行都是基于具體值的而非模擬符號值的執(zhí)行，從而顯著降低了符號執(zhí)行的開銷，使得符號執(zhí)行技術(shù)有能力處理更大規(guī)模的現(xiàn)實世界程序。

3.2 符號反向執(zhí)行（Symbolic Backward Execution）

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

04 符號執(zhí)行的限制

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

(1) 路徑爆炸

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

(2) 復雜約束

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

(3) 內(nèi)存

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

05 總結(jié)

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

審核編輯：湯梓紅