基于符號(hào)執(zhí)行的測(cè)試生成

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

蘇亭 華東師范大學(xué)軟件工程學(xué)院教授

版塊 | 鑒源論壇 · 觀模

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

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

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

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

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

符號(hào)執(zhí)行結(jié)束后生成的計(jì)算樹(shù)如圖 2 所示，樹(shù)中的每個(gè)節(jié)點(diǎn)代表程序中的一個(gè)條件語(yǔ)句，每個(gè)邊代表一組非條件語(yǔ)句的執(zhí)行，每條路徑代表從程序開(kāi)始到路徑終點(diǎn)的一條執(zhí)行路徑，通過(guò)為每條路徑求解對(duì)應(yīng)的路徑約束，就可以判斷該路徑是否可行，并為可行路徑生成對(duì)應(yīng)的程序輸入。

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

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

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

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

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

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

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

2009 年，Vitaly Chipounov 提出“選擇性符號(hào)執(zhí)行”，通過(guò)選擇 “對(duì)程序設(shè)計(jì)者有意義”的執(zhí)行分支進(jìn)行符號(hào)執(zhí)行測(cè)試來(lái)提高對(duì)大型程序應(yīng)用符號(hào)執(zhí)行測(cè)試的可行性。

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

03 符號(hào)執(zhí)行進(jìn)階

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

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

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

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

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

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

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

(1) 路徑爆炸

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

(2) 復(fù)雜約束

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

(3) 內(nèi)存

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

05 總結(jié)

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

審核編輯：湯梓紅