基于動(dòng)態(tài)分析的軟件不變量綜合技術(shù)*

王 博 , 盧思睿 , 姜佳君 , 熊英飛

1(北京大學(xué) 信息科學(xué)技術(shù)學(xué)院 計(jì)算機(jī)科學(xué)技術(shù)系 軟件研究所,北京 100871)2(高可信軟件技術(shù)教育部重點(diǎn)實(shí)驗(yàn)室(北京大學(xué)),北京 100871)

軟件不變量(software invariant,以下簡(jiǎn)稱為不變量)是軟件運(yùn)行時(shí)在程序某位置必須保持的屬性(property).不變量可以有多種表現(xiàn)形式,例如前條件(pre-condition)與后條件(post-condition)、循環(huán)不變量(loop invariant)、斷言(assertion)、在面向?qū)ο笳Z言中描述對(duì)象屬性的類不變量(class invariant)以及描述對(duì)象之間關(guān)系的結(jié)構(gòu)不變量(structural invariant)等等.

不變量被廣泛應(yīng)用在程序驗(yàn)證、程序理解、程序優(yōu)化、程序維護(hù)、程序缺陷定位以及程序缺陷修復(fù)等領(lǐng)域.一般而言,不變量可以被編碼為邏輯表達(dá)式,從而使用數(shù)理邏輯手段進(jìn)行演算.例如在程序驗(yàn)證中,不變量可以視為規(guī)約(specification),通過把程序的語義轉(zhuǎn)化為邏輯表達(dá)式,可以使用霍爾邏輯進(jìn)行演算來驗(yàn)證程序是否滿足規(guī)約.由于不變量是軟件屬性的高度抽象,人工構(gòu)造不變量非常繁瑣復(fù)雜,因此開發(fā)人員一般采用軟件分析(program analysis)的方法從軟件中自動(dòng)地綜合(synthesize)不變量.

軟件分析技術(shù)主要包括靜態(tài)分析(static analysis)和動(dòng)態(tài)分析(dynamic analysis).靜態(tài)分析不需要運(yùn)行程序,僅根據(jù)程序自身的源碼、文檔或者可執(zhí)行文件等等進(jìn)行分析.為了分析得到不變量,靜態(tài)分析在程序所有可能執(zhí)行的路徑(path)和狀態(tài)(state)上進(jìn)行推理,可以得到可靠的(sound)分析結(jié)果.然而,由于靜態(tài)分析過于復(fù)雜,在實(shí)際中只能應(yīng)用在小規(guī)模軟件上,而且一般只能得到形式較為簡(jiǎn)單的不變量.動(dòng)態(tài)分析則根據(jù)程序的執(zhí)行蹤跡(trace)來分析得到不變量.給定一組輸入(例如軟件的單元測(cè)試)運(yùn)行程序,動(dòng)態(tài)分析根據(jù)程序某位置運(yùn)行時(shí)狀態(tài)歸納分析結(jié)果.由于動(dòng)態(tài)方法只執(zhí)行全部可能的輸入的一部分,并且只覆蓋了一部分路徑,因此動(dòng)態(tài)分析的結(jié)果不保證可靠性與完備性,例如可能遺漏了某些不變量或者生成了錯(cuò)誤的不變量.相比于靜態(tài)分析,動(dòng)態(tài)分析一般效率(efficiency)較高,有更好的可延展性(scalability),而且可以生成形式更復(fù)雜的不變量.

早在20 世紀(jì)70 年代,軟件驗(yàn)證領(lǐng)域就開始了對(duì)不變量的研究.早期不變量相關(guān)研究主要是基于靜態(tài)分析方法,例如使用抽象解釋[1,2]分析不變量.2000 年左右,研究者們才開始研究基于動(dòng)態(tài)技術(shù)來分析不變量.其中,里程碑式的研究工作是Ernst 等人在1999 年提出的Daikon[3].之后,研究人員逐漸開展基于動(dòng)態(tài)分析的不變量綜合研究,并且取得了一系列成果.本文的目標(biāo)是分析、梳理這20 余年內(nèi)基于動(dòng)態(tài)分析的不變量分析的相關(guān)研究工作,以供研究人員快速了解該領(lǐng)域.有關(guān)基于純靜態(tài)分析的不變量分析方法不在本文討論范圍之內(nèi).

為了對(duì)該研究問題的進(jìn)展進(jìn)行系統(tǒng)地分析和比較,我們首先按以下步驟收集并篩選1999 年以來的相關(guān)研究文獻(xiàn).

(1) 使用谷歌學(xué)術(shù)搜索引擎以及ACM,IEEE,Springer,Elsevier 和CNKI 等論文數(shù)據(jù)庫;

(2) 檢索關(guān)鍵字包括在英文引擎中的“program invariant”和“software invariant”以及在中文引擎中的“不變量”和“不變式”等;

(3) 檢索時(shí)間為1999 年至今的全部文獻(xiàn);

(4) 基于前述步驟檢索到的論文,通過人工篩選移除無關(guān)論文.之后,瀏覽文獻(xiàn)并移除與動(dòng)態(tài)分析技術(shù)無關(guān)論文.在此文獻(xiàn)列表上,總結(jié)出該領(lǐng)域的活躍研究者,進(jìn)一步在研究者的論文列表中檢查是否有遺漏的工作.在選取過程中,主要傾向選取軟件形式化、軟件工程、系統(tǒng)軟件以及程序設(shè)計(jì)語言等相關(guān)領(lǐng)域的會(huì)議和期刊.

我們最終選取了90 篇論文,其中絕大多數(shù)是所涉及領(lǐng)域的高質(zhì)量會(huì)議和期刊,例如POPL 會(huì)議(2 篇)、PLDI會(huì)議(10 篇)、OOPSLA 會(huì)議(1 篇)、SOSP 會(huì)議(1 篇)、CAV 會(huì)議(2 篇)、ICSE 會(huì)議(14 篇)、ESEC/FSE 會(huì)議(5篇)、ASE 會(huì)議(8 篇)、ISSTA 會(huì)議(7 篇)、ESOP 會(huì)議(1 篇)、TACAS 會(huì)議(1 篇)、SAS 會(huì)議(2 篇)、FM 會(huì)議(1篇)、ISSRE 會(huì)議(1 篇)、TSE 期刊(6 篇)、TOSEM 期刊(2 篇)、軟件學(xué)報(bào)(2 篇).

圖1 統(tǒng)計(jì)了2001 年～2019 年的與動(dòng)態(tài)不變量分析技術(shù)的發(fā)表文章數(shù),從中可以看到該領(lǐng)域的研究趨勢(shì).自從1999 年以來,每年都有高質(zhì)量文章發(fā)表,說明相關(guān)研究依然十分活躍.該領(lǐng)域的研究獲得了一些重要獎(jiǎng)項(xiàng),包括ICSE 會(huì)議2009 年[4]和2012 年[5]的SIGSOFT 杰出論文獎(jiǎng),PLDI 會(huì)議2018 年[6]和2019 年[7]的杰出論文獎(jiǎng).

國外已有一些與不變量分析技術(shù)相關(guān)的英文綜述論文,與已有的綜述[8-10]相比,我們的工作有以下不同.

· 首先,我們總結(jié)出基于動(dòng)態(tài)分析的不變量綜合技術(shù)的研究框架.現(xiàn)有的綜述主要以軟件驗(yàn)證領(lǐng)域的視角來梳理文獻(xiàn).我們希望在建立統(tǒng)一的研究框架之后,可以打破軟件形式化、系統(tǒng)軟件、軟件工程、程序設(shè)計(jì)語言等不同領(lǐng)域之間的壁壘,更系統(tǒng)地分析和比較研究成果;

· 其次,本文重點(diǎn)對(duì)動(dòng)態(tài)分析相關(guān)的不變量綜合技術(shù)進(jìn)行綜述,對(duì)于不變量的種類并不限制.相比Furia 等人的綜述[8],我們不僅分析了循環(huán)不變量的相關(guān)工作,還總結(jié)了結(jié)構(gòu)不變量等其他種類的不變量;

· 再次,我們?cè)谖墨I(xiàn)選取與分類上使用了新的視角.我們按照生成不變量的方法將所綜述的文獻(xiàn)劃分為基于模板窮舉的方法、基于數(shù)值計(jì)算的方法、基于統(tǒng)計(jì)學(xué)習(xí)的方法和基于符號(hào)執(zhí)行的方法這4 個(gè)類別.在此基礎(chǔ)上,我們嘗試總結(jié)出動(dòng)態(tài)不變量綜合技術(shù)發(fā)展的不同階段,以方便研究人員掌握該領(lǐng)域的發(fā)展脈絡(luò)并預(yù)測(cè)發(fā)展趨勢(shì).另外,我們分析并總結(jié)了不變量在軟件維護(hù)、軟件測(cè)試和軟件調(diào)試等相關(guān)領(lǐng)域的廣泛應(yīng)用;

· 最后,在上述綜述之后,該領(lǐng)域又出現(xiàn)一些新的進(jìn)展.研究者們不但提出一些新的不變量動(dòng)態(tài)綜合方法,還把該技術(shù)應(yīng)用在新問題和新場(chǎng)景上,例如最近兩年不變量被應(yīng)用在信息物理系統(tǒng)錯(cuò)誤檢測(cè)[11,12]和神經(jīng)網(wǎng)絡(luò)模型驗(yàn)證[7,13]等領(lǐng)域.我們補(bǔ)充了相關(guān)的最新研究成果.

Fig.1 Publication numbers in different years圖1 在不同年份發(fā)表的文章數(shù)

本文貢獻(xiàn)可以總結(jié)如下.

(1) 系統(tǒng)地分析了基于動(dòng)態(tài)分析的不變量綜合技術(shù).通過梳理與該領(lǐng)域相關(guān)的90 篇國內(nèi)外高水平論文,提出了“學(xué)習(xí)者-預(yù)言模型”研究框架概括基于動(dòng)態(tài)分析的不變量綜合技術(shù);

(2) 在該研究框架下,我們對(duì)于收集到的方法根據(jù)其技術(shù)特點(diǎn)進(jìn)行分類,并分析得到該領(lǐng)域的演進(jìn)趨勢(shì);

(3) 系統(tǒng)地總結(jié)了基于動(dòng)態(tài)分析的不變量綜合技術(shù)的相關(guān)應(yīng)用;

(4) 總結(jié)了該領(lǐng)域的經(jīng)常使用的數(shù)據(jù)集和開源工具.

本文第1 節(jié)介紹本領(lǐng)域的基礎(chǔ),包括不變量的概念與形式,提出了“學(xué)習(xí)者-預(yù)言”研究框架.第2 節(jié)對(duì)已有的基于動(dòng)態(tài)分析的不變量綜合方法進(jìn)行梳理分析,并分析技術(shù)演進(jìn)趨勢(shì).第3 節(jié)總結(jié)動(dòng)態(tài)分析綜合不變量的相關(guān)應(yīng)用.第4 節(jié)總結(jié)常用的測(cè)試程序以及重要的開源工具.最后,第5 節(jié)總結(jié)全文并展望未來研究方向.

1 基于動(dòng)態(tài)分析綜合不變量基礎(chǔ)

1.1 不變量的概念與形式

不變量的字面是表達(dá)“不會(huì)改變的量”或“常量”的含義.在計(jì)算機(jī)程序中,不變量是指在程序某個(gè)片段在所有執(zhí)行過程中需要保持為真的邏輯斷言.根據(jù)程序的位置不同,不變量約定的名稱也會(huì)隨之改變.例如:在循環(huán)初始位置和結(jié)束位置都被保持的屬性,一般被成為循環(huán)不變量;在面向?qū)ο笳Z言中,描述對(duì)象方法(method)或者域(field)的屬性的,一般被稱為類不變量.另外,當(dāng)不變量所描述的對(duì)象為數(shù)據(jù)結(jié)構(gòu)實(shí)例(instance)之間的關(guān)系時(shí),被稱為結(jié)構(gòu)不變量(例如二叉樹中一組左、右孩子節(jié)點(diǎn)的雙親節(jié)點(diǎn)必須相同).

以下給出不變量的形式化定義.

定義1(不變量).在命令語言中,對(duì)于任意的可終止程序P,c是P中的命令集合.在關(guān)于P的任意輸入上,執(zhí)行到c中命令之前時(shí),程序的狀態(tài)始終滿足的邏輯表達(dá)式I,則稱I是該位置上的不變量.

根據(jù)定義1,我們可以描述不同類型的不變量.例如:當(dāng)c僅包含一條命令,在其執(zhí)行之前必須滿足的邏輯表達(dá)式I為c的斷言(assert);若c僅包含循環(huán)的第1 條命令以及循環(huán)之后的第1 條命令,在這兩個(gè)命令執(zhí)行前必須滿足的邏輯表達(dá)式I成為循環(huán)不變量.

在邏輯上,不變量必須保證是正確的,這就要求生成不變量的算法必須是可靠的.然而在程序分析中,尤其是動(dòng)態(tài)分析中,可靠性難以保證.因此,該領(lǐng)域的研究者提出各種方法來生成最可能正確的不變量.

1.2 基于動(dòng)態(tài)分析的不變量綜合技術(shù)研究框架

本文重點(diǎn)綜述基于動(dòng)態(tài)分析的不變量綜合技術(shù),其目標(biāo)是在動(dòng)態(tài)分析的基礎(chǔ)上歸納得到不變量.圖2 總結(jié)了典型的基于動(dòng)態(tài)分析的不變量綜合技術(shù)的研究框架.

Fig.2 Overview of general dynamic invariant synthesis framework圖2 基于動(dòng)態(tài)分析的不變量綜合方法研究框架概覽

受到預(yù)言指導(dǎo)下的歸納綜合(oracle guided inductive synthesis)技術(shù)[14]的啟發(fā),我們提出基于動(dòng)態(tài)分析的不變量綜合方法的研究框架,如圖2 上半部所示.該框架可以大體分為兩個(gè)模塊,即基于歸納的學(xué)習(xí)者(inductive learner,后文簡(jiǎn)稱為學(xué)習(xí)者)模塊以及預(yù)言(oracle)模塊.預(yù)言模塊也可以被稱為教師(teacher).其中,學(xué)習(xí)者的任務(wù)是綜合生成不變量,而預(yù)言的任務(wù)是判斷學(xué)習(xí)者產(chǎn)生的不變量是否正確以及為學(xué)習(xí)者提供不變量綜合用的輔助信息.學(xué)習(xí)者和預(yù)言之間存在交互,交互方式是學(xué)習(xí)者向預(yù)言提出請(qǐng)求(request),請(qǐng)求的內(nèi)容可以是驗(yàn)證其生成不變量的正確性、程序符號(hào)執(zhí)行的結(jié)果、正例、反例等.預(yù)言負(fù)責(zé)回應(yīng)(response)相應(yīng)的結(jié)果.一般而言,學(xué)習(xí)者不掌握程序內(nèi)部細(xì)節(jié),視其為黑盒.學(xué)習(xí)者主要通過預(yù)言返回的數(shù)據(jù)樣例等信息歸納產(chǎn)生不變量.預(yù)言掌握豐富的程序內(nèi)部信息,以便能夠回應(yīng)學(xué)習(xí)者的請(qǐng)求.二者經(jīng)過有限次的交互后,得到最終的不變量集合.基于此,我們將該研究框架稱為“學(xué)習(xí)者-預(yù)言”模型.

預(yù)言模塊把程序視為白盒,除了掌握程序代碼、程序規(guī)約(specification)、程序?qū)傩?property)等信息之外,還能產(chǎn)生正例(example)和反例(counter-example).值得注意的是:程序規(guī)約既可以是程序的完全規(guī)約,也可以是測(cè)試等形式的不完全規(guī)約.為了響應(yīng)學(xué)習(xí)者的請(qǐng)求,預(yù)言可以執(zhí)行多種操作.例如:學(xué)習(xí)者請(qǐng)求驗(yàn)證猜想的不變量是否正確時(shí),預(yù)言可以使用測(cè)試執(zhí)行程序驗(yàn)證或者通過靜態(tài)分析驗(yàn)證;學(xué)習(xí)者請(qǐng)求提供程序的符號(hào)執(zhí)行結(jié)果時(shí),預(yù)言可以進(jìn)行動(dòng)態(tài)或靜態(tài)符號(hào)執(zhí)行,返回程序中變量的符號(hào)表示以及路徑約束;學(xué)習(xí)者請(qǐng)求反例時(shí),預(yù)言通過靜態(tài)分析和約束求解器得到反例并返回.

學(xué)習(xí)者是不變量綜合技術(shù)的核心,也是該領(lǐng)域一直以來的研究重點(diǎn).我們根據(jù)所依賴預(yù)言提供數(shù)據(jù)的種類以及學(xué)習(xí)者所采用的歸納方法,大致將其分為4 類,即基于模板窮舉的方法、基于數(shù)值計(jì)算的方法、基于統(tǒng)計(jì)學(xué)習(xí)的方法以及基于符號(hào)執(zhí)行的方法.

本文提出相關(guān)方法的一種劃分,可以看出,這幾種分類有著明顯的遞進(jìn)關(guān)系.大致的趨勢(shì)是生成不變量形式越來越復(fù)雜,方法的步驟從單次到循環(huán)迭代,依賴預(yù)言提供的信息越來越多.值得注意的是:如果某幾種方法之間有交叉重疊之處,我們將依據(jù)一個(gè)方法的主要?jiǎng)?chuàng)新之處來將其歸類.

通過上述不變量的綜合過程,我們總結(jié)對(duì)于生成不變量的質(zhì)量的影響因素以及對(duì)不變量綜合技術(shù)的評(píng)價(jià)指標(biāo),如圖2 下半部所示.

影響生成的不變量質(zhì)量的因素主要包括學(xué)習(xí)者的歸納能力、時(shí)間/內(nèi)存等約束以及預(yù)言提供的信息等.學(xué)習(xí)者的歸納能力越強(qiáng),得到的不變量形式越復(fù)雜、越精確.由于“學(xué)習(xí)者-預(yù)言”模型可能需要多次迭代,時(shí)間/內(nèi)存等約束會(huì)影響最終的生成結(jié)果,例如在達(dá)到最優(yōu)解之前因?yàn)槌瑫r(shí)停止,會(huì)導(dǎo)致產(chǎn)生次優(yōu)解.另外,一般而言,預(yù)言提供的信息越多,對(duì)學(xué)習(xí)者的幫助就越大,最終得到的不變量集合質(zhì)量越高.

對(duì)于不變量綜合方法,我們可以從效率(effciency)、表現(xiàn)力(expressiveness)、精確度(precision)和效用性(utility)這4 個(gè)方面對(duì)其進(jìn)行評(píng)價(jià).

· 效率是單位時(shí)間內(nèi)某方法生成的不變量數(shù)目.對(duì)于動(dòng)態(tài)分析而言,效率越高的方法可延展性越好.一些不變量綜合方法依賴于插裝、動(dòng)態(tài)符號(hào)執(zhí)行等代價(jià)較高的動(dòng)態(tài)技術(shù),其運(yùn)行代價(jià)限制了它們?cè)诖笠?guī)模程序上的應(yīng)用.因此,高效率的方法具有更高的實(shí)用價(jià)值;

· 表現(xiàn)力是某方法能夠生成不變量的種類.一般形式越復(fù)雜的不變量越難生成,例如二元不變量難于一元不變量,高階多項(xiàng)式形式的不變量難于線性形式的不變量.復(fù)雜不變量在現(xiàn)實(shí)世界中大量存在,生成方法更有表現(xiàn)力意味著其能生成更復(fù)雜的不變量,從而更好地刻畫軟件屬性.值得注意的是:表現(xiàn)力雖然從某種程度上可以反映召回率(recall),即發(fā)現(xiàn)的不變量占理論上所有存在的不變量的比例,但是二者并不相同.在現(xiàn)有相關(guān)論文中,評(píng)價(jià)方法的表現(xiàn)力往往依賴于不變量的復(fù)雜程度,即通過能夠生成其他方法理論上無法生成的形式的不變量證明其優(yōu)勢(shì),而不是簡(jiǎn)單比較挖掘到的不變量的數(shù)目;

· 精確度是指所生成的不變量中正確的不變量的比例.動(dòng)態(tài)分析方法一般不保證結(jié)果的正確性,對(duì)于產(chǎn)生的假陽性(false positive)不變量,需要較高的代價(jià)去過濾.因此,高精確度的方法更容易部署為全自動(dòng)方法,具有更好的實(shí)用性;

· 效用性是指所生成的不變量是否滿足應(yīng)用需求的比例.雖然方法的精確度十分重要,但是如果不滿足應(yīng)用的需求,生成大量正確而無用的不變量,也會(huì)影響任務(wù)的完成.例如在軟件驗(yàn)證任務(wù)中,不變量過多會(huì)導(dǎo)致程序的驗(yàn)證耗時(shí)過長(zhǎng),甚至因超時(shí)導(dǎo)致任務(wù)失敗.因此在實(shí)際應(yīng)用中,我們需要精簡(jiǎn)而正確的不變量集合.效用性與應(yīng)用類型高度相關(guān).例如,動(dòng)態(tài)監(jiān)測(cè)非法內(nèi)存訪問時(shí),與內(nèi)存邊界有關(guān)的不變量有更高的效用性.

2 基于動(dòng)態(tài)分析的不變量綜合技術(shù)

本節(jié)主要在第1 節(jié)中提到的“學(xué)習(xí)者-預(yù)言”框架下討論基于動(dòng)態(tài)分析的不變量綜合技術(shù).首先,從學(xué)習(xí)者的視角來看,根據(jù)學(xué)習(xí)者的歸納得到不變量的方法,我們將當(dāng)前的基于動(dòng)態(tài)分析的不變量綜合技術(shù)大致分為4 類:基于模板窮舉的方法(例如Daikon[3,15,16]和DIDUCE[17])、基于數(shù)值計(jì)算的方法(例如DIG[5,18],NumInv[19]和SLING[20])、基于機(jī)器學(xué)習(xí)的方法(例如ICE[21],PIE[22]和DORDER[23])以及基于符號(hào)執(zhí)行的方法(例如DySy[24]和KRYSTAL[25]).本節(jié)依次介紹4 個(gè)分類.針對(duì)每個(gè)分類,我們主要介紹該分類整體的技術(shù)特點(diǎn),該分類下已有的重要方法,并簡(jiǎn)要概括該類方法的優(yōu)缺點(diǎn)及其適用場(chǎng)景;其次,對(duì)預(yù)言來說,驗(yàn)證學(xué)習(xí)者提出的不變量正確性是其核心任務(wù),因此,我們以預(yù)言驗(yàn)證不變量的方式將已有方法進(jìn)行簡(jiǎn)要?dú)w類分析;最后,我們做出小結(jié),分析本領(lǐng)域研究的現(xiàn)狀與發(fā)展趨勢(shì).

2.1 基于模板窮舉的不變量綜合技術(shù)

在基于模板窮舉的方法中,學(xué)習(xí)者在程序上選擇需要生成不變量的位置,根據(jù)預(yù)先設(shè)計(jì)的謂詞模板,與當(dāng)前位置的變量嘗試所有可能的組合之后得到猜想不變量集合,根據(jù)預(yù)言提供該位置程序正確執(zhí)行的狀態(tài)集過濾掉被違反的不變量.預(yù)言一般需要執(zhí)行測(cè)試集來收集正確的程序狀態(tài)返回給學(xué)習(xí)者,并根據(jù)測(cè)試等部分規(guī)約對(duì)猜想不變量進(jìn)行驗(yàn)證.學(xué)習(xí)者與預(yù)言之間存在一次或者多次交互,最終將不變量集合返回.

最早在1998 年,Vaziri 等人檢測(cè)動(dòng)態(tài)運(yùn)行中兩個(gè)變量是否保持=,＜,＞,≤或≥等比較關(guān)系.該工作可視為基于模板的動(dòng)態(tài)不變量分析的早期探索[26].

1999 年,Ernst 等人提出并實(shí)現(xiàn)了Daikon[3],并在2001 年將其擴(kuò)展為期刊論文[15].Daikon 是本領(lǐng)域的里程碑,同時(shí)也是應(yīng)用最廣泛的不變量分析工具.Daikon 的學(xué)習(xí)者是基于模板窮舉來生成不變量.具體來說,在程序員指定的程序位置和變量上,學(xué)習(xí)者根據(jù)模板窮舉填入變量,得到猜想的不變量集合.之后,學(xué)習(xí)者將變量提交給預(yù)言驗(yàn)證,預(yù)言通過運(yùn)行測(cè)試,過濾測(cè)試中被違反的不變量,返回最終的不變量集合.例如,有變量a,b和不變量模板x=0,窮舉后得到不變量是a=0 和b=0 提交給預(yù)言.預(yù)言運(yùn)行所有測(cè)試后,發(fā)現(xiàn)該位置存在a≠0 的情況,則a=0 被刪除,最終輸出不變量b=0.學(xué)習(xí)者的模板可以大致分為一元操作、二元操作、標(biāo)量的三元操作以及列表變量相關(guān)的模板.表1 列出了Daikon 的所有模板.相比之前的早期探索,Daikon 大幅擴(kuò)充了模板的數(shù)量和表現(xiàn)力,增加了多元表達(dá)式以及自動(dòng)添加了求和等重要的臨時(shí)變量,可用于挖掘更多的列表元素的不變量.Daikon 支持二元比較關(guān)系、三元以內(nèi)的線性關(guān)系等等,同時(shí)允許用戶添加自定義模板.

Table 1 Templates of Daikon表1 Daikon 的模板

Daikon 可以在程序的任意位置收集不變量,在收集位置上被觀測(cè)的變量在執(zhí)行時(shí)的值的集合稱為一個(gè)樣本(sample).若設(shè)被分析程序中需要收集的位置數(shù)為P,對(duì)于某個(gè)收集不變量的位置,其所有可能的不變量數(shù)為I,在該位置上報(bào)告的不變量數(shù)為RI,且樣本數(shù)為L(zhǎng),則Daikon 的空間復(fù)雜度為

時(shí)間復(fù)雜度在最差情況下為

由于實(shí)際執(zhí)行中大多數(shù)情況下候選不變量的值是False,會(huì)很快被過濾,因此一般情況下的時(shí)間復(fù)雜度是

由上述3 個(gè)公式可知:Daikon 分析的代價(jià)很高,特別是I是關(guān)于變量個(gè)數(shù)的高階多項(xiàng)式.例如:若在當(dāng)前位置有3 個(gè)變量,僅僅模板ax+by+cz=d就會(huì)產(chǎn)生152 個(gè)可能的不變量[27].Daikon 的空間復(fù)雜度和時(shí)間復(fù)雜度隨著程序規(guī)模的增大呈指數(shù)級(jí)增長(zhǎng),導(dǎo)致將其很難擴(kuò)展在較大規(guī)模的程序上.

在Daikon 類似的方法中,學(xué)習(xí)者算法的復(fù)雜度導(dǎo)致其在復(fù)雜模板上代價(jià)很高,而主要依賴于簡(jiǎn)單的模板又導(dǎo)致其表現(xiàn)力不足.另外,Daikon 的預(yù)言采用單元測(cè)試驗(yàn)證不變量的正確性,預(yù)言的驗(yàn)證能力十分依賴于測(cè)試集的質(zhì)量[16].為了克服這些缺點(diǎn),隨后,研究人員從學(xué)習(xí)者和預(yù)言兩方面對(duì)Daikon 的生成方法進(jìn)行優(yōu)化.

為了提升Daikon 的學(xué)習(xí)者效率,Perkins 和Ernst 等人分析了Daikon 算法,發(fā)現(xiàn)其簡(jiǎn)單增量算法中存在多處冗余[27]:首先,當(dāng)變量x和變量y滿足不變量x=y時(shí),對(duì)于其他任意的Daikon 模板f,都滿足f(x)=f(y);其次,若某變量x滿足恒等于常數(shù)a,即有不變量x=a,則會(huì)產(chǎn)生很多冗余不變量,例如,x=0 必然可得x≥0;再次,面向?qū)ο笳Z言中的變量存在層次,生成的不變量可以同時(shí)影響多個(gè)位置,例如,面向?qū)ο笾心硞€(gè)公共方法返回處的不變量既是該方法的后條件,又是對(duì)象不變量;最后,不變量之間存在蘊(yùn)含關(guān)系,例如x＞y蘊(yùn)含x≥y.針對(duì)這4 個(gè)方面的冗余,作者們提出使用增量算法進(jìn)行削減.另外,為了盡快過濾錯(cuò)誤的不變量,他們引入了5 輪次(pass)分析,即:在早期的輪次中分析簡(jiǎn)單的不變量,后面的輪次中分析復(fù)雜的不變量.通過上述加速方法,大幅提升了Daikon 的效率.

在Daikon 等方法中,預(yù)言的驗(yàn)證能力高度依賴于測(cè)試集的質(zhì)量,初始測(cè)試集的大小和覆蓋率等指標(biāo)直接影響方法的精確度.為了緩解這一問題,張令明等人提出了基于反饋的動(dòng)態(tài)不變量生成方法iDiscovery[28],在預(yù)言中引入測(cè)試自動(dòng)生成方法:首先,使用Daikon 生成不變量;然后,將不變量作為斷言插裝回原程序;隨后,使用符號(hào)執(zhí)行在插裝后的程序上生成測(cè)試,將新測(cè)試加入原測(cè)試集中;最后,使用加強(qiáng)后的測(cè)試運(yùn)行Daikon.迭代上述過程,直至達(dá)到不動(dòng)點(diǎn).實(shí)驗(yàn)證明了在Daikon 生成的不變量中,該方法可以過濾很多其中的錯(cuò)誤不變量,并且能發(fā)現(xiàn)新的不變量.值得注意的是,該方法是基于模板窮舉的方法和基于符號(hào)執(zhí)行的方法的結(jié)合,詳見第2.4 節(jié).

Daikon 對(duì)結(jié)構(gòu)不變量的支持非常有限,僅能分析簡(jiǎn)單的數(shù)據(jù)結(jié)構(gòu).因此,Malik 等人提出針對(duì)復(fù)雜數(shù)據(jù)結(jié)構(gòu)的動(dòng)態(tài)不變量提取算法Deryaft[29].通過將程序的堆(heap)建模為圖,其中,圖的節(jié)點(diǎn)代表內(nèi)存對(duì)象,圖的邊標(biāo)記為域,之后在圖上分析其性質(zhì).Deryaft 把性質(zhì)設(shè)計(jì)為模板,然后在圖上迭代驗(yàn)證性質(zhì)是否成立.其所設(shè)計(jì)的模板主要有可達(dá)性(如無環(huán)性)、數(shù)據(jù)結(jié)構(gòu)中描述大小的屬性是否與遍歷所得的節(jié)點(diǎn)數(shù)相等、樹中不同節(jié)點(diǎn)到根節(jié)點(diǎn)的距離等等.實(shí)驗(yàn)表明:對(duì)于結(jié)構(gòu)不變量,Deryaft 的表現(xiàn)力和效用性優(yōu)于Daikon.

另外,與Daikon 在同一時(shí)期,由Hangal 等人在2002 年提出的DIDUCE 也是影響力較大的工作[17].與Daikon相比,DIDUCE 的優(yōu)勢(shì)在于:(1) 它是一種全自動(dòng)的方法,不必像Daikon 一樣需要人工指定分析的位置和變量;(2) DIDUCE 通過削減分析的狀態(tài),可以延展到較大規(guī)模程序上;(3) 對(duì)程序輸入要求不高,甚至可以使用無測(cè)試預(yù)言(test orcale)的隨機(jī)生成的測(cè)試.DIDUCE 只分析全局變量上的不變量,縮小了分析的范圍.DIDUCE 通過將狀態(tài)映射為整數(shù)上的位(bit),從而將每個(gè)插裝位置的不變法分析運(yùn)算約減為幾個(gè)邏輯位運(yùn)算,在運(yùn)行中未改動(dòng)過的位即是不變量.DIDUCE 擁有動(dòng)態(tài)檢查錯(cuò)誤的能力,在實(shí)驗(yàn)中,它可以發(fā)現(xiàn)長(zhǎng)時(shí)間運(yùn)行后進(jìn)入的非法狀態(tài).在預(yù)言中,與Daikon 使用測(cè)試作為規(guī)約不同,DIDUCE 使用程序一部分正常運(yùn)行作為驗(yàn)證手段.

之后,Fei 等人提出了針對(duì)動(dòng)態(tài)監(jiān)控的加速技術(shù)Artemis[30],并應(yīng)用在C 語言版本的DIDUCE 的方法上,提升了該方法的效率.

Hangal 等人將Daikon 的方法移植在硬件驗(yàn)證上,針對(duì)硬件設(shè)計(jì)了新的模板并實(shí)現(xiàn)了工具IODINE[31].基于動(dòng)態(tài)分析的不變量一定程度上可以代替人工提取的規(guī)范,從而減輕硬件工程師的負(fù)擔(dān).

在Daikon 的啟發(fā)下,Boshernitsan 等人提出了方法Agitator,并將其實(shí)現(xiàn)為商業(yè)工具[32].Agitator 采用的模板包括等式(如x=y),區(qū)間(如a≤x≤b),非空(x≠null)以及從源代碼中收集的屬性,并將動(dòng)態(tài)挖掘出的不變量報(bào)告給開發(fā)者,輔助他們提升軟件的測(cè)試集質(zhì)量.

上述方法的不變量模板主要是基于命題邏輯的形式,即一階邏輯(first-order logic).后來,研究者也嘗試探索使用更復(fù)雜的邏輯的模板,例如二階邏輯(second-order logic)和時(shí)序邏輯(temporal logic).

Li 等人使用二階約束加強(qiáng)Daikon 的一階命題邏輯不變量,提出方法Meta-Inv[33].二階不變量又稱元不變量(meta invariant),是命題邏輯不變量之間蘊(yùn)含的不變關(guān)系.二階不變量甚至可以在一階不變量未知的情況下推導(dǎo).作者提出了若干二階不變量模板.例如在數(shù)據(jù)結(jié)構(gòu)棧中,top 方法入口處的不變量集是pop 方法入口處的不變量集的子集,即可得二階不變量:“top 方法的前條件蘊(yùn)含pop 方法的前條件”.作者設(shè)計(jì)了5 個(gè)二階不變量的模板,用于描述對(duì)于不同方法的入口和出口處的不變量集合之間的關(guān)系.在Daikon 的基礎(chǔ)上,該方法預(yù)言也使用測(cè)試驗(yàn)證不變量.二階不變量可以加強(qiáng)一階不變量的推理,另外還可以擴(kuò)展到大規(guī)模軟件上并且有較高的精確度.

Beschastnikh 等人提出Synoptic 方法,根據(jù)系統(tǒng)的運(yùn)行日志自動(dòng)建模,構(gòu)造出系統(tǒng)的有限狀態(tài)自動(dòng)機(jī)[34,35].Synoptic 在日志中挖掘事件的時(shí)間序列關(guān)系,在時(shí)間不變量(temporal invariant)模板的約束下探測(cè)模型空間.Synoptic 使用了3 種時(shí)間不變量來描述事件發(fā)生的順序關(guān)系,包括事件B永遠(yuǎn)發(fā)生在事件A之后、事件B永遠(yuǎn)不發(fā)生在事件A之后、事件A永遠(yuǎn)在事件B之前.

隨后,Beschastnikh 等人提出InvariMint 方法改進(jìn)Synoptic 方法[36].InvariMint 明確地指定了最終的模型中屬性的類型,并且將屬性挖掘和屬性規(guī)約兩個(gè)機(jī)制獨(dú)立出來,降低耦合.

Beschastnikh 等人提出Perfume 方法[37,38],在Synoptic 方法提出的模型迭代使用基于反例的抽象精化算法不斷改進(jìn)模型,直至模型滿足所有的屬性.

Beschastnikh 等人提出CSight 方法[39].CSight 為并行程序進(jìn)行日志分析,挖掘日志中的時(shí)間不變量,推理出系統(tǒng)的有限狀態(tài)自動(dòng)機(jī).開發(fā)者可以使用得到的簡(jiǎn)潔精確的自動(dòng)機(jī)理解系統(tǒng)的行為或發(fā)現(xiàn)缺陷.

Lemieux 等人提出了線性時(shí)間規(guī)約挖掘方法Texada[40],該方法允許用戶自定義任意的線性時(shí)間規(guī)約模板,同時(shí)挖掘用戶支持的且在置信區(qū)間內(nèi)的規(guī)約.

基于模板窮舉的方法簡(jiǎn)單直觀,不依賴于符號(hào)執(zhí)行、約束求解和統(tǒng)計(jì)學(xué)習(xí)等其他復(fù)雜技術(shù),而且有Daikon等成熟的工具體系支持.正如第3 節(jié)介紹的相關(guān)應(yīng)用中,該類技術(shù)的應(yīng)用范圍最廣,部分成果也被應(yīng)用于工業(yè)界.該類方法的缺點(diǎn)是其效果高度依賴于模板.模板形式的單調(diào)會(huì)限制不變量的表現(xiàn)力,但是豐富而語義多有重疊的模板又會(huì)降低效用性.因此,該類方法需要用戶根據(jù)應(yīng)用特點(diǎn)選擇合適的模板.另外,該類方法對(duì)測(cè)試集的質(zhì)量需求較高,不但需要測(cè)試有較高的代碼覆蓋率,也需要測(cè)試輸入有足夠的多樣性.

2.2 基于數(shù)值計(jì)算的不變量綜合技術(shù)

根據(jù)第2.1 節(jié)中對(duì)Daikon[3,15,16]復(fù)雜度的分析,隨著模板所需變量數(shù)以及合法變量數(shù)的增多,候選不變量的數(shù)量呈指數(shù)級(jí)增長(zhǎng).受限于模板與變量結(jié)合生成的巨大空間,基于模板窮舉的技術(shù)只適合探索較為簡(jiǎn)單的線性關(guān)系,對(duì)不變量表現(xiàn)力有較大限制.例如,Daikon 無法生成三元不等關(guān)系的不變量、非線性多項(xiàng)式的不變量、四元或四元以上的相等關(guān)系以及嵌套數(shù)組關(guān)系.為了探索更復(fù)雜的不變量,研究者結(jié)合數(shù)值計(jì)算方法生成不變量.在該類方法中,學(xué)習(xí)者將模板參數(shù)化,使用方程組求解方法和多面體近似方法計(jì)算不變量,并滿足覆蓋預(yù)言提供的狀態(tài)集合.在該類方法中,預(yù)言通過程序的正確運(yùn)行的狀態(tài)集驗(yàn)證學(xué)習(xí)者猜想的不變量.此外,在部分方法中,預(yù)言還可以根據(jù)學(xué)習(xí)者猜想得到的錯(cuò)誤不變量使用SMT 求解得到反例反饋給學(xué)習(xí)者,幫助其在下一輪迭代中產(chǎn)生更好的不變量.

在2012 年,Nguyen 等人首次將數(shù)值計(jì)算方法應(yīng)用在動(dòng)態(tài)不變量生成方法上[5].受到靜態(tài)分析方法中抽象解釋等方法的啟發(fā),他們使用的數(shù)值計(jì)算方法主要包括方程組求解和多面體(polyhedra)技術(shù),分別用于處理多元相等關(guān)系、多元不等關(guān)系.最后,使用SMT 求解技術(shù)刪除冗余的不變量.具體來說,對(duì)于多元相等關(guān)系,學(xué)習(xí)者根據(jù)當(dāng)前變量生成多元多次的等式模板.學(xué)習(xí)者向預(yù)言請(qǐng)求一組正例,將正例中變量的值帶入等式,即得到關(guān)于系數(shù)的一次方程組.根據(jù)線性代數(shù)方法求解該方程,就得到了等式不變量中的系數(shù).例如,當(dāng)前位置存在變量a和b,并且需要得到最高項(xiàng)為二次的等式關(guān)系,學(xué)習(xí)者會(huì)產(chǎn)生等式方程:

然后,學(xué)習(xí)者向預(yù)言請(qǐng)求多組正確運(yùn)行中(a,b)的具體值帶入上述等式,就可得到關(guān)于等式不變量系數(shù)c1～c6的一個(gè)方程組.若該方程組存在唯一解,使用線性代數(shù)方法求解該方程組后就可得到不變量的系數(shù).用類似的方法,將不等關(guān)系轉(zhuǎn)化為給定一組點(diǎn),求一個(gè)可以覆蓋它們的凸多面體問題.最后,由于不變量之間可能存在蘊(yùn)含關(guān)系,通過SMT 求解器判斷不變量之間是否滿足蘊(yùn)含關(guān)系,從而過濾冗余的不變量.對(duì)于數(shù)組不變量,通過將未知數(shù)用數(shù)組的元素和索引表示,可以將上述計(jì)算方法用于數(shù)組上不變量的生成.雖然該方法的精確度和效用性不高,但是相比基于模板窮舉的方法,其表現(xiàn)力大幅增強(qiáng).

之后,Nguyen 等人繼續(xù)將上面的方法進(jìn)一步擴(kuò)展為DIG 方法[18]:首先,對(duì)于不等關(guān)系,DIG 添加了使用幾何推理的方法,用下八面體等形狀代替多面體,用于得到下近似的結(jié)果;其次,將八面體不等式用于數(shù)組邊界元素上;最后,作者理論分析了所涉及算法的復(fù)雜度.

之前相關(guān)工作中的不變量都是命題的合取形式,Nguyen 等人首次提出生成析取(disjunctive)不變量的動(dòng)態(tài)分析方法,提升了方法的表現(xiàn)力[41].析取不變量可以用于表現(xiàn)程序分支,是一種十分重要的不變量.例如在程序if(p)a=1; elsea=2;中,析取不變量(p∧a=1)∨(?p∧a=2)可以表現(xiàn)分支的性質(zhì).然而,傳統(tǒng)的動(dòng)態(tài)不變量綜合方法主要針對(duì)合取(conjunctive)、多項(xiàng)式以及凸多面體的不變量,并不適合生成析取不變量.生成析取不變量需要借助非凸多面體,而DIG 等方法使用的加法和乘法僅能描述凸多面體.因此,作者使用了最大加(max-plus)關(guān)系代替加法和乘法來描述非凸多面體.同時(shí),針對(duì)當(dāng)且僅當(dāng)(if-and-only-if)結(jié)構(gòu),作者使用雙最小加(dual min-plus)約束來描述.為了加速計(jì)算,作者提出了上述兩個(gè)算法的弱化版本,使其復(fù)雜度降至多項(xiàng)式時(shí)間.最后,作者引入靜態(tài)分析過濾不變量,使用迭代并行的k推導(dǎo)算法.

研究者注意到:在不變量的過濾階段,SMT 求解技術(shù)可以提升過濾非法不變量并產(chǎn)生反例.于是,研究者引入了“猜想-檢測(cè)”技術(shù),將生成和驗(yàn)證兩個(gè)步驟統(tǒng)一了起來.

2013 年,Sharma1 等人提出了基于“猜想-檢測(cè)”的循環(huán)不變量生成技術(shù)[42].學(xué)習(xí)者負(fù)責(zé)“猜想”,使用類似DIG的算法動(dòng)態(tài)推導(dǎo)等式不變量,提交給預(yù)言.預(yù)言負(fù)責(zé)“檢測(cè)”,使用SMT 過濾不滿足的不變量,并生成反例返回給“猜想”部分,輔助其生成不變量.“猜想-檢測(cè)”可視為是一種基于反例引導(dǎo)的方法.算法重復(fù)這兩個(gè)步驟,直至發(fā)現(xiàn)滿意的循環(huán)不變量.

Nguyen 等人提出了在符號(hào)執(zhí)行基礎(chǔ)上的基于反例引導(dǎo)的不變量生成技術(shù)NumInv(又稱DIG2)[19].首先,NumInv 使用DIG[18]得到一組不變量.對(duì)于程序位置L上的不變量p,將原程序轉(zhuǎn)換為if (?p)L.在轉(zhuǎn)換后的程序上運(yùn)行符號(hào)執(zhí)行.如果符號(hào)執(zhí)行中,L是可達(dá)的位置,則p必定不是不變量.對(duì)符號(hào)執(zhí)行的環(huán)境求解后可得反例,用于指導(dǎo)DIG 的不變量生成.若符號(hào)執(zhí)行中L不可達(dá),則認(rèn)為p是正確的不變量.在預(yù)言的驗(yàn)證部分中,NumInv 使用的符號(hào)執(zhí)行引擎是KLEE,依賴于SMT 求解器.相比于“猜想-檢測(cè)”[42]方法,NumInv 可以處理不等關(guān)系的不變量,表現(xiàn)力得到增強(qiáng).該方法在基于數(shù)值計(jì)算的方法基礎(chǔ)上結(jié)合了符號(hào)執(zhí)行技術(shù).

Nguyen 等人繼續(xù)改進(jìn)NumInv[19]的方法,提出了方法SymInfer(又稱DIG3)[43].首先,在學(xué)習(xí)者中設(shè)定初始的符號(hào)執(zhí)行最大分支數(shù),在被測(cè)程序上運(yùn)行符號(hào)執(zhí)行,收集各個(gè)路徑的抽象的符號(hào)狀態(tài).然后,SymInfer 將抽象狀態(tài)實(shí)例化得到具體狀態(tài),進(jìn)入推理階段運(yùn)行DIG 得到候選不變量集合.最后,學(xué)習(xí)者把不變量提交給預(yù)言,預(yù)言使用SAT 求解器判斷所有符號(hào)狀態(tài)是否能推導(dǎo)出某個(gè)不變量,如果推導(dǎo)可滿足,就認(rèn)為是合法的不變量;否則,就求解生成反例,用于返回給學(xué)習(xí)者,用于下一輪推導(dǎo)過程中指導(dǎo)DIG.學(xué)習(xí)者和預(yù)言之間不斷交互,直到得到了穩(wěn)定的結(jié)果后終止.與NumInv 相比,SymInfer 不是將符號(hào)執(zhí)行當(dāng)做黑盒使用,而是深入符號(hào)執(zhí)行引擎內(nèi)部,使用實(shí)際的符號(hào)狀態(tài).在驗(yàn)證中,SymInfer 得到的不變量精確度更高,證明該方法的有效性.值得注意的是:NumInv/DIG2 和SymInfer/DIG3 也可視為是基于符號(hào)執(zhí)行的方法.二者都建立在DIG 的基礎(chǔ)上,并且DIG,DIG2 和DIG3是同一個(gè)團(tuán)隊(duì)的連貫研究.為不破壞其完整性,本文將上述三者放在本類別下介紹.

Le 等人提出了SLING,用于在動(dòng)態(tài)分析的基礎(chǔ)上提取復(fù)雜數(shù)據(jù)結(jié)構(gòu)中的結(jié)構(gòu)不變量[20].SLING 使用分離邏輯(separation logic)[44]對(duì)堆內(nèi)存建模推理,最終輸出的不變量也是用分離邏輯的公式描述的.對(duì)于某個(gè)數(shù)據(jù)結(jié)構(gòu),如列表或樹等,SLING 需要設(shè)計(jì)基于分離邏輯的謂詞.然后記錄程序在某位置蹤跡,得到程序某位置上的堆和棧內(nèi)存對(duì)象變量.根據(jù)變量和謂詞生成候選不變量集合.最后,使用SMT 模型檢查過濾不可滿足的不變量.

基于數(shù)值計(jì)算的不變量綜合技術(shù)是目前表現(xiàn)力最強(qiáng)的一類方法,可以生成多種復(fù)雜的不變量,例如多元多次等式不變量和析取不變量.通過把固定的模板參數(shù)化,極大地?cái)U(kuò)展了可探索的不變量空間,同時(shí)也導(dǎo)致不變量空間爆炸式增長(zhǎng).由于面臨更巨大的搜索空間,該類方法的精確度和效用性低于其他方法.該類方法對(duì)測(cè)試集的質(zhì)量需求非常高,例如DIG 方法使用方程組求解等式不變量時(shí),如果不提供使之恰好有唯一解的數(shù)據(jù),就無法解出相應(yīng)不變量.

2.3 基于統(tǒng)計(jì)學(xué)習(xí)的不變量綜合技術(shù)

之前所述的方法不論是使用模板窮舉還是使用數(shù)值計(jì)算方法,核心都是使用確定、可解釋的算法.近年來,隨著統(tǒng)計(jì)機(jī)器學(xué)習(xí)技術(shù)受到了廣泛關(guān)注,研究者嘗試將統(tǒng)計(jì)學(xué)習(xí)技術(shù)應(yīng)用在基于動(dòng)態(tài)分析的不變量綜合技術(shù)中.該類別方法一般稱預(yù)言模塊為教師.預(yù)言可以通過靜態(tài)分析的手段驗(yàn)證學(xué)習(xí)者提出的不變量假設(shè),同時(shí)給學(xué)習(xí)者提供正例和反例.學(xué)習(xí)者使用統(tǒng)計(jì)學(xué)習(xí)方法,例如決策樹(decision tree)和支持向量機(jī)(support vector machine)等算法提出不變量假設(shè)給預(yù)言.當(dāng)?shù)玫阶罱K的不變量集合或達(dá)到時(shí)間/內(nèi)存約束后,返回結(jié)果.

Sankaranarayanan 等人使用決策樹來生成保證程序正確運(yùn)行的前條件[45].該方法根據(jù)程序的輸入變量用啟發(fā)式規(guī)則產(chǎn)生一組命題.根據(jù)這組命題構(gòu)造出一個(gè)SAT 滿足的命題公式,該公式的真值用于表示是否滿足某性質(zhì)(例如是否觸發(fā)緩沖區(qū)溢出).同時(shí),根據(jù)各個(gè)命題的賦值,可以生成具體的測(cè)試輸入.運(yùn)行具體輸入可得到該公式的真值(例如該輸入觸發(fā)了緩沖區(qū)溢出).之后,以命題賦值及公式的真值為訓(xùn)練集,使用決策樹算法從中學(xué)習(xí)出命題組成的前條件.

Garg 等人提出了基于學(xué)習(xí)的數(shù)值不變量生成技術(shù)ICE[21].ICE 分為學(xué)習(xí)者和教師兩個(gè)模塊.學(xué)習(xí)者不掌握程序及其規(guī)約的任何信息,通過運(yùn)行蹤跡中的具體值來綜合出不變量假設(shè).作者將這樣的不變量生成器稱為黑盒(block-box)方法.教師掌握程序信息和規(guī)約,可以為學(xué)習(xí)者提供訓(xùn)練數(shù)據(jù),也可以對(duì)學(xué)習(xí)者返回的不變量假設(shè)進(jìn)行驗(yàn)證,當(dāng)教師拒絕不變量假設(shè)時(shí),會(huì)報(bào)告提供新的反例.教師和學(xué)習(xí)者僅通過具體的數(shù)據(jù)溝通,這樣切分的好處是可以讓學(xué)習(xí)者應(yīng)用機(jī)器學(xué)習(xí)技術(shù).作者發(fā)現(xiàn):僅使用正例和反例用于訓(xùn)練產(chǎn)生的不變量歸納性(inductive)不強(qiáng),如果把數(shù)據(jù)之間的推導(dǎo)關(guān)系作為訓(xùn)練數(shù)據(jù)的一部分,則可以減輕過擬合現(xiàn)象.ICE 會(huì)根據(jù)預(yù)定義的數(shù)值關(guān)系原子命題模板(僅包括x+y＜a或x≠y等簡(jiǎn)單形式)綜合出復(fù)雜的不變量.

隨后,Garg 為ICE 的學(xué)習(xí)者設(shè)計(jì)更復(fù)雜的學(xué)習(xí)算法[46].作者提出了針對(duì)邏輯蘊(yùn)含的決策樹算法.同時(shí),理論證明該算法的收斂性,以及如果存在不變量,則該學(xué)習(xí)算法必然能在有限次迭代中發(fā)現(xiàn).

Padhi 等人發(fā)現(xiàn):ICE 等方法所用的原子命題需要事先用給定的模板定義,限制了不變量的搜索空間.當(dāng)這些方法生成的命題無法區(qū)分正確輸入和錯(cuò)誤輸入時(shí),就不能產(chǎn)生正確的不變量.他們提出PIE 方法,不再需要提供命題模板,而是用基于搜索的程序綜合來生成[22].

Ezudheen 等人發(fā)現(xiàn),ICE 生成的不變量并不適合用于程序驗(yàn)證,因?yàn)槌绦蝌?yàn)證需要霍爾子句(Horn clause)進(jìn)行程序推理.作者提出了HORN-ICE 方法,將ICE 的思想應(yīng)用于生成霍爾子句形式的不變量上[47].霍爾約束是非線性的不變量,為了解決這一挑戰(zhàn),作者提出了基于決策樹的學(xué)習(xí)算法來從樣本中學(xué)習(xí).作者從理論上證明了:如果存在不變量,該算法可以在多項(xiàng)式時(shí)間內(nèi)找到.隨后,Neider 等人在HORN-ICE 的基礎(chǔ)上提出了SORCAR方法[48].SORCAR 的學(xué)習(xí)者在每次交互中,盡量挑選與所驗(yàn)證屬性最相關(guān)的謂詞來生成不變量.

Gehr 等人提出了新的基于機(jī)器學(xué)習(xí)的黑盒方法提取交換性規(guī)范(commutativity specification)[49].交換性規(guī)范是指兩個(gè)操作可以交換順序,在多線程程序驗(yàn)證中十分重要.作者收集數(shù)據(jù)時(shí)采用類型感知采樣技術(shù),得到足夠多樣性而且冗余少的數(shù)據(jù)集.該高質(zhì)量數(shù)據(jù)集可用于過濾冗余的謂詞.最后使用謂詞生成公式覆蓋當(dāng)前的樣例集合,以得到最終的不變量.

Zhu 等人提出了自動(dòng)生成形狀規(guī)約的方法DORDER[23].給定一個(gè)數(shù)據(jù)結(jié)構(gòu)的定義和執(zhí)行蹤跡,DORDER 可以在自動(dòng)生成描述形狀和順序的謂詞.首先,DORDER 對(duì)數(shù)據(jù)結(jié)構(gòu)使用隨機(jī)測(cè)試技術(shù)產(chǎn)生一組”輸入-輸出對(duì)”(input-output pair);然后,DORDER 自動(dòng)地分析數(shù)據(jù)結(jié)構(gòu),得到一組原子命題;最后,使用機(jī)器學(xué)習(xí)算法根據(jù)蹤跡學(xué)習(xí)原子命題.

Zhu 等人提出了數(shù)據(jù)驅(qū)動(dòng)的受約束的霍爾子句(constrained Horn clause)求解方法LinearArbitrary[6],該方法能使用任意的原子謂詞來任意地組合成受約束的霍爾子句.該方法由反例制導(dǎo)的抽象精化驗(yàn)證(counterexample guided abstraction refinement)部分來采樣有代表性的正例和反例,并提供給機(jī)器學(xué)習(xí)工具鏈.機(jī)器學(xué)習(xí)工具鏈由兩層模型組成,用于歸納得到不變量.該方法的驗(yàn)證模塊也使用到了基于數(shù)值計(jì)算方法的多面體求解方法.

Brockschmidt 等人認(rèn)為,動(dòng)態(tài)分析下生成不變量是搜索出程序已經(jīng)運(yùn)行的狀態(tài)的上近似(over approximate)公式,從某種角度就是統(tǒng)計(jì)學(xué)習(xí)問題.他們提出了技術(shù)Locust 用于學(xué)習(xí)結(jié)構(gòu)不變量[50],用于描述堆對(duì)象的形狀(shape).Locust 定義了一套分離邏輯公式的文法來描述不變量空間.給定一個(gè)初始文法節(jié)點(diǎn),Locust 根據(jù)當(dāng)前狀態(tài)在機(jī)器學(xué)習(xí)模型的指導(dǎo)下展開非終結(jié)節(jié)點(diǎn),直至生成一個(gè)合法的公式.

近年來,不變量也與新場(chǎng)景和新問題結(jié)合起來.信息物理系統(tǒng)是軟件與傳感器等硬件結(jié)合的系統(tǒng),在與現(xiàn)實(shí)世界的交互過程中需要構(gòu)建復(fù)雜的模型,因此往往難以靠人力進(jìn)行精確地分析和驗(yàn)證.信息物理系統(tǒng)在使用中會(huì)產(chǎn)生大量數(shù)據(jù),Chen 等人利用機(jī)器學(xué)習(xí)方法學(xué)習(xí)其中的不變量[11,12].作者使用了監(jiān)督模型,即收集正常運(yùn)行以及非法運(yùn)行狀態(tài)下的數(shù)據(jù),使用支持向量機(jī)算法訓(xùn)練出分類器,用于描述系統(tǒng)變量之間的不變關(guān)系.作者使用了變異測(cè)試來產(chǎn)生非法運(yùn)行的數(shù)據(jù).

基于統(tǒng)計(jì)學(xué)習(xí)的方法一般采用形式較為簡(jiǎn)單的不變量模板,表現(xiàn)力受到限制.有的綜合方法依賴于較為復(fù)雜的學(xué)習(xí)算法,結(jié)果會(huì)有不確定性,也影響了綜合方法的精確度和效用性.同時(shí),類似神經(jīng)網(wǎng)絡(luò)等模型可解釋性較低,難以對(duì)生成的不變量給出形式化證明.理論上,該類方法可以實(shí)現(xiàn)跨項(xiàng)目的不變量預(yù)測(cè),但是可遷移性仍需實(shí)驗(yàn)驗(yàn)證.該類方法效率較高,適用于需要快速產(chǎn)生不變量的場(chǎng)景.

2.4 基于符號(hào)執(zhí)行的不變量綜合技術(shù)

上述的3 類方法的學(xué)習(xí)者主要依靠程序執(zhí)行蹤跡和反例分析得到不變量,而忽視了許多代碼文本自身的信息.在此類方法中,學(xué)習(xí)者除了請(qǐng)求具體執(zhí)行的數(shù)據(jù),也會(huì)請(qǐng)求程序符號(hào)執(zhí)行(symbolic execution)的結(jié)果,即變量的符號(hào)表示和路徑約束.除了能得到程序的語義信息,也可以根據(jù)需要將符號(hào)執(zhí)行的約束進(jìn)行求解,預(yù)言既可以根據(jù)約束的可滿足性來驗(yàn)證不變量,也可以產(chǎn)生具體測(cè)試輸入來增強(qiáng)已有測(cè)試.

在2008 年,Csallner 等人最早將符號(hào)執(zhí)行應(yīng)用在動(dòng)態(tài)不變量生成技術(shù)上,提出了方法DySy[24].學(xué)習(xí)者向預(yù)言請(qǐng)求軟件的運(yùn)行狀態(tài)時(shí),除了在測(cè)試上運(yùn)行的具體執(zhí)行的狀態(tài),也會(huì)請(qǐng)求符號(hào)執(zhí)行的狀態(tài).預(yù)言部分在使用測(cè)試進(jìn)行具體執(zhí)行的同時(shí)進(jìn)行符號(hào)執(zhí)行.當(dāng)遇到分支時(shí),符號(hào)執(zhí)行使用具體程序的執(zhí)行流而非像傳統(tǒng)符號(hào)執(zhí)行探索其他路徑.當(dāng)具體執(zhí)行結(jié)束時(shí),符號(hào)執(zhí)行中保存的就是該具體執(zhí)行的路徑條件和變量的符號(hào)表示,即獲得了本次執(zhí)行的前條件/后條件,由預(yù)言將其返回給學(xué)習(xí)者.學(xué)習(xí)者將所有測(cè)試的前條件/后條件合并后,即可得該程序的不變量.與Daikon 相比,Dysy 生成的無關(guān)不變量更少,提升了方法的精確度和效用性.

同一時(shí)期,Kannan 等人提出KRYSTAL 技術(shù),基于符號(hào)執(zhí)行提取結(jié)構(gòu)不變量[25].KRYSTAL 技術(shù)提出了一種新的符號(hào)執(zhí)行的變體:普遍符號(hào)執(zhí)行.該變體不會(huì)映射賦值運(yùn)算中的左值,例如程序x=1;y=x+1;中左值y的符號(hào)表示是x+1 而非傳統(tǒng)符號(hào)執(zhí)行中的2.KRYSTAL 首先通過普遍符號(hào)執(zhí)行收集程序的路徑條件和變量的符號(hào)表示,使用二者生成局部謂詞.由局部謂詞生成局部不變量的模板.在這一組模板上執(zhí)行傳統(tǒng)的動(dòng)態(tài)不變量分析.在實(shí)驗(yàn)中,KRYSTAL 生成了很多之前方法無法生成的高質(zhì)量的結(jié)構(gòu)不變量,提升了方法的表現(xiàn)力和效用性.

符號(hào)執(zhí)行的核心思想是將程序中的具體值抽象為符號(hào)值,并在符號(hào)值上運(yùn)行程序.符號(hào)執(zhí)行可以探索程序中的路徑,并且可以產(chǎn)生覆蓋某條已探索路徑的具體輸入.符號(hào)狀態(tài)可以通過約束求解技術(shù)得到具體狀態(tài),如前文所述NumInv/DIG2[19]和SymInfer/DIG3[43]就在基于數(shù)值計(jì)算的方法基礎(chǔ)上輔助符號(hào)執(zhí)行技術(shù).另外,符號(hào)執(zhí)行的一個(gè)典型應(yīng)用是自動(dòng)生成測(cè)試.如前文所述,iDiscovery[28]使用符號(hào)執(zhí)行生成高覆蓋率的測(cè)試提供給Daikon,以生成質(zhì)量更高的不變量集合.

基于符號(hào)執(zhí)行的不變量綜合技術(shù)的使用前提是目標(biāo)程序必須支持符號(hào)執(zhí)行,該類別方法的優(yōu)勢(shì)和劣勢(shì)都可以追溯至符號(hào)執(zhí)行技術(shù)自身的優(yōu)缺點(diǎn).符號(hào)執(zhí)行的優(yōu)勢(shì)是能夠獲得程序的語義信息,使得學(xué)習(xí)者能在掌握代碼信息的情況下歸納綜合不變量.同時(shí),這類方法對(duì)原始測(cè)試的質(zhì)量需求也不高,因?yàn)榭梢愿鶕?jù)符號(hào)執(zhí)行求解出高覆蓋率的具體測(cè)試輸入來補(bǔ)全當(dāng)前測(cè)試.相對(duì)而言,該類方法生成的不變量精確度較高.然而,符號(hào)執(zhí)行也面臨許多挑戰(zhàn),例如路徑爆炸、內(nèi)存建模、約束求解以及對(duì)浮點(diǎn)數(shù)和并發(fā)等功能支持不足等.這就需要目標(biāo)程序滿足一系列要求,例如程序所需的第三方庫都已被建模以支持符號(hào)執(zhí)行;程序僅有串行執(zhí)行模式;程序沒有浮點(diǎn)計(jì)算,沒有過于復(fù)雜的內(nèi)存對(duì)象和復(fù)雜的循環(huán)結(jié)構(gòu)等.該類方法適用于規(guī)模較小、結(jié)構(gòu)簡(jiǎn)單或者測(cè)試不充足的程序,適合對(duì)不變量的精確度要求較高的場(chǎng)景.

2.5 預(yù)言的驗(yàn)證方法

在前4 節(jié)中,我們主要介紹學(xué)習(xí)者綜合不變量的過程中采用的不同歸納方法.在“學(xué)習(xí)者-預(yù)言”的研究框架內(nèi),預(yù)言主要承擔(dān)不變量正確性驗(yàn)證、提供正例/反例、實(shí)施符號(hào)執(zhí)行和實(shí)施具體執(zhí)行等.在預(yù)言的多個(gè)功能中,驗(yàn)證學(xué)習(xí)者提出的不變量的正確性是最重要的,因此我們主要介紹預(yù)言中不同的驗(yàn)證手段.其他預(yù)言相關(guān)問題,例如運(yùn)行程序方式等詳見前述方法細(xì)節(jié),不在此進(jìn)行討論.在本節(jié)中,我們主要介紹預(yù)言中不同的驗(yàn)證方法,并舉例介紹典型技術(shù).預(yù)言主要使用的驗(yàn)證手段有測(cè)試、程序一段時(shí)間內(nèi)的正常運(yùn)行、靜態(tài)分析等.

· 測(cè)試是軟件的部分規(guī)約,軟件單元測(cè)試的運(yùn)行狀態(tài)可以視為正確的狀態(tài).因此,預(yù)言常用測(cè)試來檢測(cè)學(xué)習(xí)者提出的不變量猜想.如果不變量違反了測(cè)試中出現(xiàn)的狀態(tài),預(yù)言則拒絕該不變量.使用測(cè)試驗(yàn)證不變量正確性的代表的技術(shù)有Daikon 及其衍生的相關(guān)方法、DIG、DySy、KRYSTAL 等;

· 操作系統(tǒng)和網(wǎng)絡(luò)服務(wù)器等軟件等需要長(zhǎng)時(shí)間運(yùn)行,在這些程序中,可以將程序一段時(shí)間內(nèi)的正常運(yùn)行視為正確的狀態(tài).在這些運(yùn)行上歸納出的不變量,可以用于檢測(cè)后續(xù)運(yùn)行的狀態(tài).代表技術(shù)有DIDUCE以及其衍生方法、信息物理系統(tǒng)中異常檢測(cè)等;

· 在有的方法中,預(yù)言掌握程序的完全規(guī)約和屬性等信息,可以使用靜態(tài)分析手段驗(yàn)證不變量的正確性.另外,預(yù)言還可以通過約束求解給出違反當(dāng)前規(guī)約的反例,反饋給學(xué)習(xí)者輔助下一輪的不變量生成.使用靜態(tài)分析的代表方法有ICE 及其衍生方法、DORDER、Locust 等.

2.6 小 結(jié)

本節(jié)嘗試總結(jié)該領(lǐng)域大體的研究現(xiàn)狀、發(fā)展脈絡(luò)以及領(lǐng)域分布等情況.表2 對(duì)主要的研究方法進(jìn)行總結(jié),包括方法名稱、相關(guān)論文、發(fā)表的會(huì)議/期刊名稱、發(fā)表年份、方法類型以及生成的不變量類型.該表按照方法的年份排序,方便讀者發(fā)現(xiàn)并分析研究趨勢(shì).

從現(xiàn)有方法出現(xiàn)的時(shí)間來看,依次出現(xiàn)的是基于模板窮舉的方法、基于符號(hào)執(zhí)行的方法、基于統(tǒng)計(jì)學(xué)習(xí)的方法以及基于數(shù)值計(jì)算的的方法.基于模板窮舉的方法最直觀簡(jiǎn)單,因此出現(xiàn)得最早.該類方法的相關(guān)研究主要集中出現(xiàn)在2000 年～2010 年之間.Daikon 不但是該類方法的開創(chuàng)者,也是使用動(dòng)態(tài)分析綜合不變量的先驅(qū)工作.基于符號(hào)執(zhí)行的的方法隨后出現(xiàn),由于符號(hào)執(zhí)行的自身限制,導(dǎo)致該類方法論文數(shù)量?jī)H有2 篇.基于統(tǒng)計(jì)學(xué)習(xí)的方法雖然最早出現(xiàn)在2008 年,但是該類方法在2014 年ICE 出現(xiàn)之后才涌現(xiàn)該領(lǐng)域代表性的研究工作,即使用“學(xué)習(xí)者-教師”模型,為學(xué)習(xí)者提供反例指導(dǎo)不變量的生成.基于數(shù)值計(jì)算的方法出現(xiàn)于2012 年,并且近幾年依然有該類方法的論文出現(xiàn).相比于之前的方法,該類方法不再拘泥于固定模板,而開始使用參數(shù)化的模板,能夠生成的不變量的表現(xiàn)力大幅增強(qiáng).我們可以分析出:根據(jù)出現(xiàn)時(shí)間的先后順序,基于動(dòng)態(tài)分析的不變量綜合技術(shù)整體上經(jīng)歷了方法從簡(jiǎn)單到復(fù)雜,依賴信息從少到多的演化趨勢(shì).

從現(xiàn)有方法生成的不變量類別來看,最多的是多項(xiàng)式不變量,其次是時(shí)間不變量和結(jié)構(gòu)不變量,其他形式的不變量只作為個(gè)例出現(xiàn).我們認(rèn)為,出現(xiàn)該現(xiàn)象主要有3 個(gè)原因:(1) 軟件驗(yàn)證技術(shù)對(duì)這3 種類型的不變量需求較多;(2) 這3 種類型的不變量相對(duì)其他類型的不變量更容易生成和驗(yàn)證;(3) 整體的研究活躍,相關(guān)的實(shí)驗(yàn)對(duì)象和開源工具較多.

從研究的領(lǐng)域分布來看,當(dāng)前已有方法主要來自于軟件工程、程序設(shè)計(jì)語言以及驗(yàn)證領(lǐng)域.其中,基于模板窮舉、基于數(shù)值計(jì)算和基于符號(hào)執(zhí)行的方法主要發(fā)表在軟件工程領(lǐng)域的會(huì)議和期刊上,例如ICSE,ASE,TSE 等.基于統(tǒng)計(jì)學(xué)習(xí)的方法則主要發(fā)表在程序設(shè)計(jì)語言和驗(yàn)證領(lǐng)域的會(huì)議和期刊上,例如PLDI,OOPSLA,CAV 等.在查閱文獻(xiàn)的過程中,我們發(fā)現(xiàn)不同領(lǐng)域之間的一些術(shù)語也存在差異,例如預(yù)言模塊在不同領(lǐng)域中稱呼不同,在驗(yàn)證領(lǐng)域的文章中多被稱為“教師”(teacher),而在軟件工程領(lǐng)域的文章中沒有統(tǒng)一的稱呼,多用諸如“測(cè)試預(yù)言”或”規(guī)約”等具體描述.而且文章中介紹相關(guān)工作的部分也多是介紹自身領(lǐng)域,較少涉及其他領(lǐng)域的相關(guān)工作.說明不同領(lǐng)域的研究團(tuán)隊(duì)之間的合作與交流需要加強(qiáng).

Table 2 Summary of dynamic analysis based program invariant synthesis approaches表2 基于動(dòng)態(tài)分析的不變量綜合方法總結(jié)

3 基于動(dòng)態(tài)分析綜合的不變量的相關(guān)應(yīng)用

不變量作為程序規(guī)約的一種形式,可以在軟件開發(fā)的各個(gè)階段發(fā)揮出關(guān)鍵作用.不變量在程序的設(shè)計(jì)、編碼、測(cè)試、驗(yàn)證、優(yōu)化和維護(hù)中都扮演著關(guān)鍵角色.例如,本領(lǐng)域的先驅(qū)Daikon 中提出了一些可能的應(yīng)用,例如增強(qiáng)文檔、輔助調(diào)試和缺陷修復(fù)、增強(qiáng)測(cè)試、輔助靜態(tài)驗(yàn)證[3,15,16]等等.近年來,隨著物理信息系統(tǒng)和深度神經(jīng)網(wǎng)絡(luò)等新領(lǐng)域研究的展開,也有研究者使用動(dòng)態(tài)分析產(chǎn)生的不變量在新場(chǎng)景下保證軟件的質(zhì)量.本節(jié)介紹基于動(dòng)態(tài)分析提取的不變量的主要相關(guān)應(yīng)用.

3.1 動(dòng)態(tài)錯(cuò)誤檢測(cè)

基于動(dòng)態(tài)分析綜合的不變量需要運(yùn)行程序獲得執(zhí)行蹤跡,這使得該技術(shù)能夠很好地與其他軟件動(dòng)態(tài)分析技術(shù)結(jié)合起來.一般而言,動(dòng)態(tài)監(jiān)測(cè)錯(cuò)誤方法可以分為直接驗(yàn)證模型以及“訓(xùn)練-驗(yàn)證”模型.直接驗(yàn)證模型是指運(yùn)行時(shí)指定不變量模板,可以直接用于驗(yàn)證運(yùn)行時(shí)狀態(tài).“訓(xùn)練-驗(yàn)證”模型是指先在一部分運(yùn)行數(shù)據(jù)上綜合得到不變量(訓(xùn)練階段),之后用于監(jiān)測(cè)后續(xù)的執(zhí)行(驗(yàn)證階段).為了提高不變量的質(zhì)量,訓(xùn)練階段可以使用單元測(cè)試或者有代表性的正常運(yùn)行數(shù)據(jù).

(1) 直接驗(yàn)證模型.

直接驗(yàn)證模型的代表有殺菌劑(sanitizer)技術(shù).最初,殺菌劑技術(shù)用于動(dòng)態(tài)監(jiān)測(cè)內(nèi)存對(duì)象的邊界溢出(bounds overflow)等錯(cuò)誤,目前也支持指針雙重釋放、浮點(diǎn)數(shù)精度不合要求、整數(shù)溢出等未定義行為、多線程錯(cuò)誤以及類型錯(cuò)誤等.以內(nèi)存對(duì)象溢出錯(cuò)誤檢測(cè)為例,其大致思路是使用指針訪問內(nèi)存時(shí),為了保證是合法的訪問,指針ptr必須滿足不變量(ptr≥base)∧(ptr＜base+size).其中,base是目標(biāo)內(nèi)存對(duì)象的基址,size是該內(nèi)存對(duì)象分配時(shí)的大小.該不變量意味著指針訪問必須在內(nèi)存對(duì)象的界內(nèi),從而杜絕上溢出(overflow)和下溢出(underflow)漏洞.在程序分配內(nèi)存時(shí),殺菌劑會(huì)給每個(gè)內(nèi)存對(duì)象動(dòng)態(tài)記錄base和size,即填充模板得到不變量.當(dāng)觸發(fā)非法訪問時(shí),殺菌劑會(huì)拋出警告或直接終止程序.代表性殺菌劑技術(shù)有AddressSanitizer[51],LowFat[52,53]和EffectiveSan[54]等.尤其是AddressSanitizer 等殺菌劑被集成在Clang 編輯器中,發(fā)現(xiàn)了現(xiàn)有軟件中大量的安全漏洞.

(2) “訓(xùn)練-驗(yàn)證”模型.

“訓(xùn)練-驗(yàn)證”模型的代表有Daikon[3,15,16]以及DIDUCE[17].以Daikon 為代表的相關(guān)技術(shù)使用單元測(cè)試訓(xùn)練[24,28,31-33],即在單元測(cè)試的運(yùn)行蹤跡上收集不變量.而以DIDUCE 為代表的相關(guān)技術(shù)會(huì)首先運(yùn)行一段時(shí)間程序,在這個(gè)過程中收集不變量,并將其用于監(jiān)視之后的運(yùn)行狀態(tài).二者適用于不同的場(chǎng)景,前者適用于測(cè)試比較充分的軟件,如庫(library)等;后者適用于運(yùn)行數(shù)據(jù)量龐大或者需要長(zhǎng)時(shí)間運(yùn)行的軟件,如信息物理系統(tǒng).接下來,我們介紹一些代表性應(yīng)用.

Wang 等人將Daikon 應(yīng)用在并發(fā)程序(concurrent program)上[55].相比于傳統(tǒng)的串行程序,并發(fā)程序線程之間的交互非常復(fù)雜,難以分析.作者將不變量和調(diào)用圖結(jié)合起來,用于監(jiān)測(cè)并發(fā)程序中的缺陷.Baliga 等人將Daikon應(yīng)用在內(nèi)核“后門”的監(jiān)測(cè)上,提出了方法Gibraltar[56,57].Gibraltar 在訓(xùn)練階段得到內(nèi)核數(shù)據(jù)結(jié)構(gòu)的不變量,其中包括內(nèi)核中控制和非控制相關(guān)數(shù)據(jù)結(jié)構(gòu).在之后的運(yùn)行中,如果不變量被違反,則認(rèn)為發(fā)現(xiàn)了后門.如第2.4 節(jié)中所述,Chen 等人利用“訓(xùn)練-驗(yàn)證”模型在物理信息系統(tǒng)上生成不變量,用于監(jiān)視制水機(jī)的工作狀態(tài)[11,12].馬駿馳等人使用基于模板的動(dòng)態(tài)不變量分析技術(shù)監(jiān)測(cè)高輻射空間環(huán)境下軟件系統(tǒng)的軟錯(cuò)誤[58].Lorenzoli 等人使用不變量監(jiān)視系統(tǒng)狀態(tài),并在執(zhí)行進(jìn)入錯(cuò)誤狀態(tài)時(shí)嘗試修復(fù)[59].

3.2 調(diào)試和缺陷定位

在調(diào)試和缺陷定位中,被違反的不變量可以幫助開發(fā)者縮小可疑的代碼和輸入的查找范圍,分析出錯(cuò)原因,從而輔助程序員更好的理解、定位和修復(fù)缺陷.早在2002 年,Raz 等人就將Daikon 用于檢測(cè)輸入數(shù)據(jù)的一致性上[60].隨后,不變量分析技術(shù)也被用于自動(dòng)缺陷定位技術(shù)上.

在統(tǒng)計(jì)調(diào)試(statistical debugging)中,通過猜想程序運(yùn)行時(shí)在某處需要滿足的不變量,通過統(tǒng)計(jì)謂詞違反情況來自動(dòng)定位缺陷[61].該方法與基于頻譜的定位技術(shù)互補(bǔ)[62].謝濤等人通過比較軟件不同版本之間變量值的差異來定位缺陷[63].Liblit 等人利用統(tǒng)計(jì)方法判斷出導(dǎo)致程序出錯(cuò)的不變量[64].Brun 等人利用機(jī)器學(xué)習(xí)方法挑選出最可能揭示缺陷的不變量[65].Groce 等人使用Daikon 幫助開發(fā)者理解多個(gè)版本中的同一個(gè)缺陷[66].

3.3 程序驗(yàn)證

在軟件驗(yàn)證中,需要耗費(fèi)大量人力為程序添加注解.開發(fā)者普遍認(rèn)為,添加注解的代價(jià)大于其收益,因此在開發(fā)實(shí)踐中不愿采用驗(yàn)證技術(shù).基于此,研究者發(fā)現(xiàn),基于動(dòng)態(tài)分析綜合的不變量可以輔助開發(fā)者實(shí)施驗(yàn)證技術(shù).基于動(dòng)態(tài)分析技術(shù)綜合得到的不變量是根據(jù)程序執(zhí)行的數(shù)據(jù)樣例歸納得到的,在不掌握代碼信息的情況下,很難保證分析結(jié)果的正確性.但基于動(dòng)態(tài)分析的不變量較為高效、精確并且不需要復(fù)雜的人工操作,依然被應(yīng)用在程序驗(yàn)證上.另外,由于動(dòng)態(tài)分析和靜態(tài)分析技術(shù)的互補(bǔ)性,也有研究者將二者結(jié)合起來克服各自的缺點(diǎn).

Nimmer 等人探索了將動(dòng)態(tài)分析和靜態(tài)分析結(jié)合起來解決生成程序形式化規(guī)約的問題[67].通過Daikon 生成不保證正確性的不變量,然后使用靜態(tài)分析進(jìn)行驗(yàn)證.靜態(tài)分析可以保證結(jié)果正確.作者發(fā)現(xiàn):即便在小測(cè)試集上,動(dòng)態(tài)分析得到的不變量的質(zhì)量也足夠靜態(tài)分析使用.同時(shí),作者也證實(shí)了Daikon 方法的有效性,相比靜態(tài)分析,Daikon 生成的不變量的準(zhǔn)確度和召回率都在90%以上.

動(dòng)態(tài)分析工具和靜態(tài)分析工具都可以輔助開發(fā)者添加注解.Nimmer 進(jìn)行實(shí)證研究對(duì)比二者在輔助用戶添加注解的作用[68].作者選用的靜態(tài)分析工具Houdini 和動(dòng)態(tài)分析工具Daikon,使用二者生成程序?qū)傩蕴峁┙o用戶.實(shí)驗(yàn)證明,二者都起到了積極作用而且效果互補(bǔ).其中,Daikon 能讓用戶發(fā)現(xiàn)更有表現(xiàn)力的不變量,同時(shí)動(dòng)態(tài)不變量的不正確性造成的阻礙很小.新手程序員認(rèn)為,Daikon 提供的信息更有幫助.

Polikarpova 等人在實(shí)證研究中對(duì)比了Daikon 動(dòng)態(tài)挖掘出的合約(contract)與人工定義的合約[69],發(fā)現(xiàn)基于動(dòng)態(tài)分析生成的不變量可以用于增強(qiáng)人工添加的合約,但是并不能產(chǎn)生全部的人工合約.相比于人工合約,Daikon 生成了大約5 倍數(shù)量的合約,但是只覆蓋了其中的60%,而且大約1/3 的合約是無關(guān)的或者是錯(cuò)誤的.作者還發(fā)現(xiàn),代碼的一些度量指標(biāo)與Daikon 生成不變量的質(zhì)量相關(guān),例如行數(shù)和類的繼承深度等.

合約規(guī)范(contract specification)是軟件驗(yàn)證和調(diào)試的重要手段.Schiller 等人通過實(shí)證研究調(diào)查程序員實(shí)際開發(fā)中合約規(guī)范的使用情況和效果[70].作者發(fā)現(xiàn):動(dòng)態(tài)不變量可以使程序員更好的理解程序的合約,并實(shí)現(xiàn)了工具Celeriac 用于將動(dòng)態(tài)不變量自動(dòng)植入合約.

Schiller 等人提出了VeriWeb 方法[71],使用Daikon 降低人工添加規(guī)約的代價(jià).在實(shí)證研究中,探索時(shí)間和資金代價(jià)與開發(fā)者添加的規(guī)約數(shù)量的關(guān)系,從實(shí)際的經(jīng)濟(jì)角度來審視軟件驗(yàn)證的可行性.

由于神經(jīng)網(wǎng)絡(luò)等機(jī)器學(xué)習(xí)模型結(jié)構(gòu)復(fù)雜、可解釋性較低,難以應(yīng)用傳統(tǒng)方法進(jìn)行驗(yàn)證.有研究者使用不變量分析技術(shù)對(duì)其輔助驗(yàn)證.Gopinat 等人使用凸面體不變量自動(dòng)推理深度神經(jīng)網(wǎng)絡(luò)的形式化屬性[13].通過神經(jīng)網(wǎng)絡(luò)模型的輸入和輸出建立前條件/后條件推理關(guān)系.同時(shí),作者也研究了輸入和網(wǎng)絡(luò)內(nèi)部層的推理關(guān)系.Zhu 等人使用不變量指導(dǎo)程序綜合方法生成可驗(yàn)證的程序來輔助強(qiáng)化學(xué)習(xí)模型的驗(yàn)證[7].

如前文所述,動(dòng)態(tài)分析挖掘的不變量在時(shí)序邏輯驗(yàn)證中也有重要應(yīng)用[36-39,40,72].通過生成系統(tǒng)中的有限狀態(tài)自動(dòng)機(jī)來判斷事件之間存在的時(shí)序邏輯,從而驗(yàn)證程序的模型.

3.4 軟件測(cè)試

軟件測(cè)試是與動(dòng)態(tài)不變量分析緊密結(jié)合的技術(shù),測(cè)試可以指導(dǎo)不變量的生成,不變量反過來也可以給測(cè)試反饋.研究者將不變量分析技術(shù)應(yīng)用于測(cè)試生成、測(cè)試選擇、變異測(cè)試等領(lǐng)域.

測(cè)試選擇的目的是選取測(cè)試集中最有效的子集來運(yùn)行,從而減小測(cè)試代價(jià).傳統(tǒng)上,研究者一般使用代碼覆蓋率度量測(cè)試的有效性,即:通過分析代碼的文本結(jié)構(gòu)有多少被執(zhí)行過來判斷測(cè)試質(zhì)量,覆蓋越高的測(cè)試被認(rèn)為質(zhì)量越好.Harder 等人提出使用語義覆蓋情況來選擇[73],即檢查一個(gè)測(cè)試覆蓋多少軟件不變量.作者通過該語義評(píng)價(jià)標(biāo)準(zhǔn)選擇更有效的測(cè)試集.謝濤等人使用該指標(biāo)選擇測(cè)試[74].類似地,Pacheco 等人使用不變量過濾無效的測(cè)試,并預(yù)測(cè)測(cè)試的結(jié)果[75].

軟件剖析(profiling)技術(shù)有助于幫助開發(fā)者指定測(cè)試計(jì)劃.Elbaum 等人對(duì)軟件剖析策略進(jìn)行了實(shí)證研究[76].作者制定了多個(gè)評(píng)價(jià)指標(biāo),包括代碼覆蓋率、錯(cuò)誤檢測(cè)能力以及Daikon 輸出不變量的質(zhì)量等.

Gupta 等人發(fā)現(xiàn),覆蓋率良好的測(cè)試不一定在生成不變量上表現(xiàn)良好.因此,他們提出了不變量覆蓋標(biāo)準(zhǔn),并使用該標(biāo)準(zhǔn)指導(dǎo)測(cè)試生成,最終證實(shí)了可以生成更精確的不變量[77].

根據(jù)測(cè)試的執(zhí)行狀態(tài)歸納得到的不變量可以用于測(cè)試生成.Yuan 等人使用Daikon 在初始測(cè)試集上得到的不變量用于生成軟件的集成測(cè)試[78].謝濤等人根據(jù)不變量的抽象操作用于指導(dǎo)自動(dòng)生成單元測(cè)試[79].在d’Amorim 等人的單元測(cè)試自動(dòng)生成技術(shù)的實(shí)證研究中,Daikon 的不變量是生成指導(dǎo)之一[80].Csallner 等人使用Daikon 生成的不變量與靜態(tài)分析結(jié)合用于指導(dǎo)測(cè)試生成[81].

變異測(cè)試是衡量測(cè)試集質(zhì)量的技術(shù),通過植入大量已知的人造缺陷來判斷測(cè)試的查錯(cuò)能力.然而,變異是否與原程序語義等價(jià)是不可判定問題,需要復(fù)雜的人工驗(yàn)證去排除.Schuler 等人認(rèn)為,違反了程序不變量的變異更容易違反原程序的語義.若此類變異沒有被測(cè)試檢測(cè)出來,則更值得人工驗(yàn)證是否是等價(jià)變異[82].

AJAX 技術(shù)是Web 2.0 技術(shù)的重要組成部分,AJAX 通過客戶端與服務(wù)端的復(fù)雜異步交互來支持在客戶端動(dòng)態(tài)修改網(wǎng)頁的DOM 樹.這也使得傳統(tǒng)的網(wǎng)絡(luò)應(yīng)用測(cè)試方法不適用于AJAX.Ali 等人利用動(dòng)態(tài)提取的狀態(tài)不變量使AJAX 的測(cè)試自動(dòng)化[4].

3.5 軟件維護(hù)

當(dāng)軟件交付使用后,需要軟件維護(hù)來修復(fù)缺陷和修正需求.不變量作為規(guī)約的一種形式,可以在該過程中起到重要作用.在Daikon 的最初論文中,作者就提出不變量可以應(yīng)用在軟件維護(hù)中,例如提升文檔質(zhì)量、輔助軟件修復(fù)等方面[15,16,83].

McCamant 使用不變量分析技術(shù)預(yù)測(cè)組件升級(jí)可能引入的缺陷[84].通過Daikon 生成系統(tǒng)舊的組件的操作抽象,將其用于檢查更新的組件.

Perkins 等人提出了ClearView 方法,使用不變量指導(dǎo)軟件自動(dòng)修復(fù)[85].ClearView 在程序的正確執(zhí)行中學(xué)習(xí)得到不變量,當(dāng)監(jiān)測(cè)到缺陷發(fā)生時(shí),查看被違反的不變量.之后,ClearView 生成滿足不變量的候選補(bǔ)丁,再觀察打補(bǔ)丁之后的程序的后續(xù)運(yùn)行,留下最有可能正確的補(bǔ)丁.

也有研究者使用基于動(dòng)態(tài)分析的不變量用于可靠性計(jì)算.Ding 等人使用Daikon 挖掘的不變量計(jì)算在線運(yùn)行軟件的可靠性[86].周遠(yuǎn)等人提出計(jì)算可靠性的方法是:在Daikon 提取的不變量中提取出失效數(shù)據(jù),再提供給可靠性計(jì)算模型Nelson 得到最終結(jié)果[87].

Wei 等人使用合約在給定的錯(cuò)誤執(zhí)行上自動(dòng)修復(fù)程序[88,89].作者使用前條件/后條件作為合約,用于發(fā)現(xiàn)缺陷并嘗試修復(fù).

4 常用實(shí)驗(yàn)對(duì)象與重要開源工具總結(jié)

本節(jié)總結(jié)第2 節(jié)中不變量綜合方法常用的基準(zhǔn)實(shí)驗(yàn)對(duì)象(benchmark test subject)以及重要的開源工具,以方便讀者檢索.

4.1 常用實(shí)驗(yàn)對(duì)象

為了有效地評(píng)估不變量綜合方法,需要合適的程序作為實(shí)驗(yàn)對(duì)象.一般而言,為了增強(qiáng)實(shí)驗(yàn)的可信度,實(shí)驗(yàn)對(duì)象程序一般需要具備以下特征:(1) 程序需要有多樣性(不能只考慮某一種類型的程序);(2) 實(shí)驗(yàn)程序集需要有一定規(guī)模(包括程序總數(shù)以及每個(gè)程序的規(guī)模);(3) 程序需要是實(shí)際的算法或項(xiàng)目(而非作者定制的程序);(4) 程序需要提供足夠的預(yù)言(包括高質(zhì)量的測(cè)試、規(guī)約、屬性描述等).

本節(jié)對(duì)第2 節(jié)中常用的實(shí)驗(yàn)對(duì)象進(jìn)行總結(jié),結(jié)果見表3,該表總結(jié)了程序集名稱、使用的編程語言、首次使用的時(shí)間、常見的用于生成的不變量類型以及使用的不變量綜合方法的名稱.其中,常見不變量類型是指該數(shù)據(jù)集被用于生成該類別的不變量,數(shù)值代表等式以及不等式等不變量類型,結(jié)構(gòu)代表結(jié)構(gòu)不變量,霍爾代表霍爾子句不變量.

Table 3 Summary of frequently used experiment subject programs表3 常用實(shí)驗(yàn)對(duì)象總結(jié)

SIR/Simens 程序集包含C,Java 等多種編程語言的程序,被廣泛應(yīng)用于軟件測(cè)試等相關(guān)研究中.該程序集的應(yīng)用類型比較廣泛,同時(shí)也有較大規(guī)模的程序.其中,tcas 是經(jīng)常被使用的程序.SIR 程序集中每個(gè)程序都擁有大量的測(cè)試用例和一些植入了缺陷的版本.

標(biāo)準(zhǔn)數(shù)據(jù)結(jié)構(gòu)包括常用基礎(chǔ)數(shù)據(jù)結(jié)構(gòu),例如無環(huán)列表、有環(huán)列表、有序列表、二分查找樹、AVL 樹、堆、棧等.常見的標(biāo)準(zhǔn)數(shù)據(jù)結(jié)構(gòu)程序包括C 語言中的glibc 和Java 語言中JDK 對(duì)應(yīng)的包.標(biāo)準(zhǔn)數(shù)據(jù)結(jié)構(gòu)常用于驗(yàn)證結(jié)構(gòu)不變量的綜合技術(shù).

NLA(nonlinear arithmetic)包括27 個(gè)C 語言程序.該程序集的程序規(guī)模較小,每個(gè)程序在20 行左右.該程序集涉及復(fù)雜數(shù)學(xué)運(yùn)算,包含非線性不變量.

AES(advanced encryption standard)包含27 個(gè)Ada 程序.該數(shù)據(jù)集包含多種不同類型的不變量,總計(jì)有868行代碼以及25 個(gè)函數(shù).

SV-COMP 是依托TACAS 會(huì)議舉行的軟件驗(yàn)證比賽.在2019 年的TACAS 會(huì)議上進(jìn)行了第8 屆比賽,并將在2020 年舉行第9 屆.以2017 年的比賽為例,其中包含超過8 900 個(gè)驗(yàn)證任務(wù),每個(gè)任務(wù)提供了C 語言程序以及相應(yīng)的規(guī)約.任務(wù)類型包括溢出、內(nèi)存安全以及并發(fā)安全等問題的驗(yàn)證.

GRASShopper 是一個(gè)驗(yàn)證工具,它提供了基準(zhǔn)程序集.該數(shù)據(jù)集是其自定義的編程語言.

VCDryad 是軟件驗(yàn)證中常用的基準(zhǔn)程序集,其中包含153 個(gè)堆內(nèi)存操作相關(guān)的C 語言程序.

從表3 中我們可以發(fā)現(xiàn):針對(duì)不同類型的不變量綜合方法之間采用的數(shù)據(jù)集之間存在一些交集,例如標(biāo)準(zhǔn)數(shù)據(jù)結(jié)構(gòu)被用于生成數(shù)值不變量和結(jié)構(gòu)不變量的實(shí)驗(yàn)中;而在相同類型的不變量綜合方法間,數(shù)據(jù)集存在很大的多樣性,目前還沒有一個(gè)較為公認(rèn)的基準(zhǔn)程序集.同時(shí),我們可以發(fā)現(xiàn)實(shí)驗(yàn)對(duì)象大多來自庫、算法以及數(shù)據(jù)結(jié)構(gòu)的實(shí)現(xiàn),這從側(cè)面反映了當(dāng)前方法可延展性普遍較低,應(yīng)用在大規(guī)模軟件項(xiàng)目上依然存在困難.

4.2 重要開源工具

不變量綜合工具是重要的基礎(chǔ)軟件框架,支持著驗(yàn)證、測(cè)試以及維護(hù)等多個(gè)研究方向,因此一直以來備受研究者的重視.本節(jié)總結(jié)前文中出現(xiàn)的重要的開源不變量綜合工具,見表4.該表展示了工具的名稱、相關(guān)文獻(xiàn)、論文發(fā)表時(shí)間、最新版本發(fā)布時(shí)間、支持的語言和工具的網(wǎng)站.為方便讀者查閱,該表按照工具的發(fā)表時(shí)間排序.其中,參考文獻(xiàn)可以檢索工作采用的不變量生成算法,發(fā)表時(shí)間是該工具最早提出的年份,最新版本發(fā)布時(shí)間可以展示工具的更新和維護(hù)情況,同時(shí)可供讀者根據(jù)時(shí)間選擇對(duì)應(yīng)版本的工具鏈.支持語言可以方便讀者選擇合適的工具.表中工具的下載地址收集于2019 年11 月.

Table 4 Summary of tools for dynamic analysis based program invariant synthesis表4 基于動(dòng)態(tài)分析的不變量綜合工具總結(jié)

5 總結(jié)與展望

不變量分析與動(dòng)態(tài)分析是結(jié)合了軟件驗(yàn)證、系統(tǒng)軟件、軟件工程和程序設(shè)計(jì)語言多個(gè)學(xué)科的重要研究領(lǐng)域,本文討論二者結(jié)合下的基于動(dòng)態(tài)分析的不變量綜合方法.自Daikon 以來,該領(lǐng)域得到研究者們的持續(xù)關(guān)注,新的研究進(jìn)展不斷涌現(xiàn).學(xué)術(shù)界的一些研究成果也已經(jīng)在工業(yè)界落地,廣泛應(yīng)用在驗(yàn)證相關(guān)的商業(yè)工具上,例如IODINE[31]和Agitar[32]等.本文提出該領(lǐng)域的研究框架,即“學(xué)習(xí)者-預(yù)言”模型,并按學(xué)習(xí)者產(chǎn)生不變量的方式將其分類.正如前文所述,本文根據(jù)學(xué)習(xí)者和預(yù)言的交互方式、學(xué)習(xí)者內(nèi)部算法以及預(yù)言提供信息的不同,不變量綜合方法大致可以分為4 類:基于模板窮舉的方法、基于數(shù)值計(jì)算的方法、基于統(tǒng)計(jì)學(xué)習(xí)的方法、基于符號(hào)執(zhí)行的方法等.我們嘗試梳理方法之間異同以及該領(lǐng)域整體上的演化進(jìn)程.之后,本文討論了動(dòng)態(tài)分析生成的不變量在軟件錯(cuò)誤檢測(cè)、軟件調(diào)試、缺陷定位、軟件驗(yàn)證和軟件測(cè)試等領(lǐng)域上的相關(guān)應(yīng)用.最后,本文總結(jié)本領(lǐng)域的重要實(shí)驗(yàn)對(duì)象程序集以及工具.

經(jīng)歷20 余年的發(fā)展,基于動(dòng)態(tài)分析的不變量綜合方法已經(jīng)初步構(gòu)建出一個(gè)研究體系,同時(shí)也存在一些有待研究的問題.下面我們討論該領(lǐng)域還存在如下值得進(jìn)一步研究的問題.

(1) 結(jié)合更多靜態(tài)分析方法

本文主要討論動(dòng)態(tài)分析基礎(chǔ)上的相關(guān)研究.然而,動(dòng)態(tài)分析與靜態(tài)分析有各自的優(yōu)勢(shì),也有各自的短板,二者的結(jié)合可以良好地彌補(bǔ)對(duì)方的缺點(diǎn).另外,不變量分析作為軟件靜態(tài)分析的傳統(tǒng)問題之一,存在大量成熟的解決方案,勢(shì)必存在對(duì)動(dòng)態(tài)分析領(lǐng)域有所借鑒的方法.通過第2 節(jié)、第3 節(jié)可以看出,已有一些相關(guān)方法結(jié)合了靜態(tài)分析技術(shù),例如反例指導(dǎo)下的程序綜合等.我們可以看到,當(dāng)前的方法主要是淺層的結(jié)合,即僅僅把靜態(tài)分析技術(shù)視為黑盒應(yīng)用.我們認(rèn)為還需要分析二者的內(nèi)部原理,加深二者的結(jié)合層次.例如,在分析大規(guī)模程序時(shí),如果為預(yù)言添加訪問上下文的謂詞,上下文敏感分析(context sensitive program analysis)就能與基于歸納產(chǎn)生的不變量結(jié)合,從而形成新的“上下文”,從而提升相關(guān)的程序分析和驗(yàn)證方法的性能.

(2) 提升當(dāng)前不變量綜合方法的性能

正如前文所述,當(dāng)前基于動(dòng)態(tài)分析的不變量綜合技術(shù)主要在規(guī)模較小、功能特定的程序集上驗(yàn)證,在大型實(shí)際項(xiàng)目上部署相關(guān)技術(shù)依舊面臨很大挑戰(zhàn).而且,在工業(yè)界應(yīng)用的方法還是以基于模板窮舉的方法為主.這些從側(cè)面說明許多當(dāng)前已有方法的性能還不足以大規(guī)模實(shí)用化.通過第2 節(jié)我們可以發(fā)現(xiàn):目前已有方法主要集中在提升表現(xiàn)力上,需要研究者更多地提升綜合方法的效率、精確度、效用性等其他方面的性能.

(3) 提出更多特定類型不變量的綜合方法

根據(jù)第2 節(jié)不變量綜合方法的分析,我們可以看到針對(duì)特定類型的不變量綜合方法逐漸增多,例如提出時(shí)序邏輯、二階邏輯以及分離邏輯描述的不變量.我們認(rèn)為:依然存在很多未知類型的不變量還沒有被挖掘,有待研究者以新的視角去發(fā)現(xiàn).也可以從應(yīng)用的角度出發(fā),通過限定應(yīng)用范圍,設(shè)計(jì)出高精確度且高效用性的不變量綜合方法.

(4) 與新的應(yīng)用場(chǎng)景結(jié)合

通過第3 節(jié)可以看出,基于動(dòng)態(tài)分析綜合的不變量已經(jīng)成功應(yīng)用于很多領(lǐng)域,例如軟件測(cè)試和軟件驗(yàn)證等.從歷史上看,該領(lǐng)域也一直嘗試在與新的應(yīng)用場(chǎng)景結(jié)合,例如早期被應(yīng)用于多線程程序的驗(yàn)證,以及近年來被應(yīng)用在信息物理系統(tǒng)錯(cuò)誤監(jiān)測(cè)和神經(jīng)網(wǎng)絡(luò)模型驗(yàn)證等新領(lǐng)域上.我們還需要積極尋找新的應(yīng)用場(chǎng)景,例如近年來備受關(guān)注的區(qū)塊鏈技術(shù)和物聯(lián)網(wǎng)技術(shù).這些領(lǐng)域?qū)浖_性驗(yàn)證有著很高的需求,與不變量的應(yīng)用場(chǎng)景十分契合.在已有技術(shù)的基礎(chǔ)上,我們需要充分分析新的場(chǎng)景的特點(diǎn),提出針對(duì)新問題的解決方案.

(5) 實(shí)驗(yàn)對(duì)象和工具

通過第4 節(jié),我們可以發(fā)現(xiàn)目前該領(lǐng)域的實(shí)驗(yàn)對(duì)象普遍存在一些問題,例如程序規(guī)模不大、程序類型過于單一以及實(shí)際工程項(xiàng)目較少等等.我們認(rèn)為:針對(duì)不同的不變量類型,需要統(tǒng)一的高質(zhì)量實(shí)驗(yàn)對(duì)象集,從而使新的方法驗(yàn)證更有說服力.另外,Daikon 作為本領(lǐng)域的成熟工具的代表,極大地推進(jìn)了該領(lǐng)域的發(fā)展,在研究中經(jīng)常被用于基準(zhǔn)工具.然而,在Daikon 之后還沒有新的不變量綜合方法的成熟工具能起到類似的作用.我們認(rèn)為,結(jié)合新的不變量綜合方法的成熟工具能在本領(lǐng)域的研究中起到十分重要的作用.