程序不變量檢測(cè)技術(shù)研究進(jìn)展

劉志明　時(shí)小芳　李萌　劉杰

摘要：伴隨著經(jīng)濟(jì)的迅猛發(fā)展，軟件更新速度日益加快，傳統(tǒng)的軟件測(cè)試方法已不能有效保障軟件質(zhì)量。對(duì)軟件測(cè)試起到重要影響作用的不變量，受到了廣泛的關(guān)注。經(jīng)過近二十年的研究，程序不變量檢測(cè)技術(shù)已經(jīng)在軟件開發(fā)、軟件測(cè)試、逆向工程等領(lǐng)域得到了廣泛應(yīng)用。該文對(duì)程序不變量檢測(cè)技術(shù)在國內(nèi)外的研究現(xiàn)狀進(jìn)行了總結(jié)。主要論述了較成熟的程序不變量檢測(cè)工具的工作原理、基于合約的程序不變量檢測(cè)等各種方法的檢測(cè)過程、不變量的應(yīng)用范圍，并分析了以上各種檢測(cè)工具和方法的優(yōu)缺點(diǎn)，最后，針對(duì)已有程序不變量檢測(cè)技術(shù)及應(yīng)用中待探究的問題進(jìn)行了展望。

關(guān)鍵詞：程序不變量；動(dòng)態(tài)檢測(cè)；Daikon

中圖分類圖：TP311 文獻(xiàn)標(biāo)志碼：A 文章編號(hào)：1009-3044（2018）02-0216-03

Review of Program Invariant Detection Technology

LIU Zhi-ming， SHI Xiao-fang*， LI Meng， LIU Jie

（School of Computer， University of South China， Hengyang 421001， China）

Abstract： With the rapid development of economic， the update of software is increasingly accelerating， traditional methods of software test cant effectively guarantee the quality of software cant not be guaranteed effectively by traditional methods of software. Program invariant accords with people's expectation which is one of the most important indicators of health management in software runtime. After nearly two decades of research， Program invariant detection technology has been widely used in software development， software test， reverse engineering and other fields. In this paper， the research on invariant at home and abroad is described. Mainly discussed the working principle， the detection process and shortcomings of invariants Based on the Contract as well as the scope of invariants. Besides， it also analyzes merits and shortcomings of the above testing tools and methods. Finally， the possible research goal of the invariant is prospected in connection with the deficiency of existing detection.

Key words： Program Invariant； Dynamical Detection； Daikon

隨著經(jīng)濟(jì)的發(fā)展，軟件更新速度日益加快，軟件出錯(cuò)率隨之增大，如何有效保障和提高軟件質(zhì)量日益重要。在保障軟件質(zhì)量過程中，軟件測(cè)試作為一種不可或缺的檢測(cè)技術(shù)，對(duì)高效發(fā)現(xiàn)隱藏在軟件中的漏洞起到十分重要的作用。程序不變量作為影響軟件測(cè)試質(zhì)量的重要因素之一，是在運(yùn)行程序的整個(gè)過程中，能夠反映程序代碼中具有不變屬性的邏輯語句，不但能夠在執(zhí)行程序時(shí)表現(xiàn)代碼的各種屬性特點(diǎn)，而且能夠反映程序數(shù)據(jù)結(jié)構(gòu)等各方面的信息，在程序的設(shè)計(jì)、編碼、測(cè)試等各方面都發(fā)揮著不可代替的作用[1]，基于此，致力于研究不變量檢測(cè)技術(shù)非常有必要。

通常，從是否運(yùn)行被測(cè)程序的角度出發(fā)，可將不變量檢測(cè)分為靜態(tài)分析和動(dòng)態(tài)檢測(cè)兩種方法。靜態(tài)分析是指在不運(yùn)行程序代碼的情況下，通過檢查程序記錄文檔和代碼來發(fā)現(xiàn)潛伏在程序中一直不會(huì)改變的屬性，一般只應(yīng)用于中小型程序；動(dòng)態(tài)不變量檢測(cè)是一種可以應(yīng)用于任意數(shù)據(jù)的機(jī)器學(xué)習(xí)技術(shù)，是指在測(cè)試環(huán)境中，根據(jù)所測(cè)代碼設(shè)計(jì)適量的測(cè)試用例，然后再運(yùn)行被測(cè)程序獲取程序運(yùn)行軌跡，之后再對(duì)獲得的軌跡數(shù)據(jù)進(jìn)行分析來發(fā)現(xiàn)程序中的抽象邏輯屬性，彌補(bǔ)了靜態(tài)分析的不足，適用于較大規(guī)模程序[2]。

本文主要介紹了程序不變量動(dòng)態(tài)檢測(cè)的各種工具、技術(shù)和應(yīng)用背景并分析了其優(yōu)缺點(diǎn)，最后針對(duì)程序不變量檢測(cè)技術(shù)的研究及應(yīng)用中待探究的問題進(jìn)行了展望。

1 程序不變量檢測(cè)工具

自從不變量的定義提出之后，為了能從程序中挖掘出大量精確的不變量，致力于相關(guān)工作的研究員已開發(fā)出很多不變量檢測(cè)工具，在此，主要介紹Daikon、Diduce、TDDPA、DySy四種較成熟的不變量動(dòng)態(tài)檢測(cè)工具。

Daikon先后用Python、java語言開發(fā)過，可以動(dòng)態(tài)檢測(cè)C、C ++、Java等多種程序的屬性，且支持記錄結(jié)構(gòu)化數(shù)據(jù)源[3]；Diduce是受Daikon啟發(fā)開發(fā)得來的，側(cè)重于輔助程序員查看程序中存在的漏洞，并定位錯(cuò)誤的具體位置，已經(jīng)被成功應(yīng)用在JSSE等較大規(guī)模的程序排錯(cuò)[2]；TDDPA針對(duì)面向?qū)ο蟪绦虿蛔兞吭O(shè)計(jì)并實(shí)現(xiàn)的一種交互式的動(dòng)態(tài)檢測(cè)工具，是基于關(guān)系數(shù)據(jù)庫理論提出的；DySy使用了強(qiáng)大的符號(hào)執(zhí)行和簡化引擎實(shí)現(xiàn)了動(dòng)態(tài)符號(hào)執(zhí)行技術(shù)，大幅度地提高了推斷不變量的質(zhì)量。它們的檢測(cè)過程和特點(diǎn)如表1所示：endprint

表1主要描述了Daikon、Diduce、TDDPA、DySy四種檢測(cè)工具的檢測(cè)過程和特點(diǎn)，為以后不變量檢測(cè)技術(shù)的研究提供了依據(jù)。

2 程序不變量檢測(cè)技術(shù)

程序不變量檢測(cè)技術(shù)是為了擴(kuò)充Daikon的預(yù)置庫形式而提出的?；诤霞s的程序不變量檢測(cè)等多種檢測(cè)技術(shù)都遵循圖1理論模型。

圖1主要描述了動(dòng)態(tài)不變量檢測(cè)技術(shù)的流程，其流程主要是將待檢測(cè)程序預(yù)編譯后設(shè)置觀測(cè)點(diǎn)進(jìn)行編配，然后設(shè)計(jì)與程序相符的測(cè)試用例，在測(cè)試用例上運(yùn)行編配后的程序，運(yùn)行后會(huì)得到觀測(cè)點(diǎn)對(duì)應(yīng)的輸出數(shù)據(jù)，這些輸出數(shù)據(jù)會(huì)以文件的形式保存到數(shù)據(jù)庫中，最后再對(duì)文件數(shù)據(jù)進(jìn)行分析，得到最終不變量。以下各種檢測(cè)方法都遵循以上檢測(cè)流程，但都有各自的創(chuàng)新之處，下面逐一對(duì)之說明。

（1） 基于合約的不變量動(dòng)態(tài)檢測(cè)：存儲(chǔ)時(shí)將待測(cè)數(shù)據(jù)分成了類層次關(guān)系、方法依賴關(guān)系和變量內(nèi)在隱含關(guān)系3個(gè)層次關(guān)系，然后運(yùn)用數(shù)據(jù)挖掘算法對(duì)其進(jìn)行分析并根據(jù)層次關(guān)系將它們進(jìn)行聚類[5]。巧妙得結(jié)合了數(shù)據(jù)庫理論知識(shí)和適當(dāng)?shù)臄?shù)據(jù)挖掘算法有效地解決了軌跡數(shù)據(jù)如何存儲(chǔ)、以及如何推導(dǎo)變量之間的隱含關(guān)系的問題。

（2） 基于契約的程序不變量檢測(cè)：提出了一種新的思想來分析不變量：通過給定待測(cè)函數(shù)的前置條件與后置條件來保障程序代碼質(zhì)量，簡單來說，就是，對(duì)任意一個(gè)待測(cè)函數(shù)，提供滿足條件的輸入，應(yīng)該得到明確的輸出，不管是輸入還是輸出有錯(cuò)誤，能夠精確定位出錯(cuò)位置（參數(shù)or程序本身）。此方法從一種新的視角維度來保障軟件質(zhì)量，對(duì)未來不變量的檢測(cè)技術(shù)研究有很強(qiáng)的借鑒意義。

（3） 非函數(shù)依賴程序不變量檢測(cè)：首先指定要選取的變量類型，然后，選取或構(gòu)造與之對(duì)應(yīng)的檢測(cè)條件，然后通過與之對(duì)應(yīng)的語句模板產(chǎn)生精確的查詢語句，運(yùn)行之后便能夠查詢出符合需要的不變量，最后，將這些目標(biāo)不變量全部放入不變量集合中[5]。此方法可以按照實(shí)際情況靈活地定義新的檢測(cè)條件并生成與之對(duì)應(yīng)的查詢語句，在一定程度上增加了檢測(cè)不變量的精確性。

（4） 函數(shù)依賴程序不變量檢測(cè)：對(duì)軌跡數(shù)據(jù)進(jìn)行分析時(shí)運(yùn)用了數(shù)據(jù)挖掘中的FP-growth關(guān)聯(lián)規(guī)則來分析變量之間的關(guān)聯(lián)性， 而且，在確定函數(shù)依賴關(guān)系階段利用了回歸分析方法對(duì)理想化的一元以及多元變量關(guān)系進(jìn)行檢測(cè)，有效地證實(shí)了函數(shù)依賴不變量檢測(cè)的可行性。但是它只分析了簡單的幾種線性不變量，對(duì)復(fù)雜的線性不變量還未深入研究。

（5） 接口重載不變量檢測(cè)：把前置條件和后置條件分成兩個(gè)單獨(dú)的階段來處理，先提取所有可執(zhí)行方法的前置條件，然后再針對(duì)每個(gè)接口重載函數(shù)，查找與之相符的前置條件，若找到，則提取出與之對(duì)應(yīng)的后置條件，以完成重載方法不變量的提取[6]。有效地解決了面向?qū)ο笾蟹椒ㄕ{(diào)用時(shí)調(diào)用者和被調(diào)用者產(chǎn)生的不變量不一致的問題。但因?yàn)獒槍?duì)同一個(gè)測(cè)試用例運(yùn)行了兩次程序，效率不高。

2.1 其他方法

近年來，很多工作者致力于不變量檢測(cè)的相關(guān)研究中。相繼有相關(guān)研究人員運(yùn)用數(shù)學(xué)理論與圖形化結(jié)合的方法有效發(fā)現(xiàn)了區(qū)間型程序不變量，運(yùn)用啟發(fā)式發(fā)現(xiàn)規(guī)則和檢測(cè)算法進(jìn)行一元多項(xiàng)式不等式動(dòng)態(tài)檢測(cè)、多元多項(xiàng)式不等式動(dòng)態(tài)檢測(cè)，運(yùn)用基因表達(dá)式編程算法對(duì)線性指數(shù)型函數(shù)進(jìn)行動(dòng)態(tài)檢測(cè)，運(yùn)用GEP-RNC算法對(duì)指數(shù)與對(duì)數(shù)型程序不變量進(jìn)行檢測(cè)等[7]，克服了原有技術(shù)的計(jì)算盲目性，進(jìn)一步擴(kuò)充了Daikon的預(yù)置庫形式，使不變量形式更加多樣化，增大了挖掘出更多不變量的概率，對(duì)不變量檢測(cè)技術(shù)進(jìn)行了補(bǔ)充。

3 程序不變量的應(yīng)用

不變量被廣泛應(yīng)用于程序開發(fā)中，可以作為斷言插入到程序中以確保在進(jìn)一步測(cè)試時(shí)隨著代碼的演變不被竄改；可以過濾無效測(cè)試用例、驗(yàn)證和改進(jìn)測(cè)試套件、檢測(cè)軟件缺陷并準(zhǔn)確定位軟件錯(cuò)誤位置；可以檢測(cè)程序重構(gòu)對(duì)象以保證程序的性能；可以靜態(tài)分析操作系統(tǒng)內(nèi)核的屬性是否完整；可以檢測(cè)程序是否發(fā)生并發(fā)錯(cuò)誤；除此之外，不變量還可以形成光譜以指示程序和輸入屬性的改變[8，9]。應(yīng)用不變量比較成功的一個(gè)實(shí)例是美國布朗大學(xué)研究人員開發(fā)出了一個(gè)利用不變量自動(dòng)查找程序錯(cuò)誤的工具Carrot，它的工作原理是先確定不變量庫，通過多次運(yùn)行程序，不斷擴(kuò)展其運(yùn)行軌跡，最后再對(duì)比正確運(yùn)行軌跡和錯(cuò)誤運(yùn)行軌跡的差異。另外一個(gè)不變量應(yīng)用較為成功的實(shí)例是使用Gibraltar工具進(jìn)行內(nèi)核數(shù)據(jù)結(jié)構(gòu)不變量的自動(dòng)推理和執(zhí)行[10]，它主要是先通過外部PCI卡周期性地捕獲內(nèi)核內(nèi)存的快照，然后由Gibraltar進(jìn)行處理，自動(dòng)檢測(cè)內(nèi)核數(shù)據(jù)結(jié)構(gòu)，進(jìn)而查找到修改了關(guān)鍵內(nèi)核數(shù)據(jù)結(jié)構(gòu)的rootkit，使系統(tǒng)質(zhì)量得到保證。不變量不僅僅在以上各方面得到了應(yīng)用，在諧波雷達(dá)等領(lǐng)域也得到了成功的運(yùn)用，是一個(gè)很大的突破。

4 總結(jié)與展望

本文系統(tǒng)地討論了不變量檢測(cè)技術(shù)及其在各個(gè)領(lǐng)域的應(yīng)用，并取得了階段性成果。在回顧了不變量基本概念基礎(chǔ)上，詳細(xì)分析和總結(jié)了不變量檢測(cè)技術(shù)在國內(nèi)外的研究現(xiàn)狀以及不變量的適用背景。從以上分析中可看出：雖然現(xiàn)有的不變量檢測(cè)技術(shù)對(duì)不變量的檢測(cè)有一定的成效，但在檢測(cè)性能和效率方面仍有進(jìn)一步提升的空間，而測(cè)試用例集的完備性、編配時(shí)觀測(cè)點(diǎn)的選取、軌跡數(shù)據(jù)的記錄格式是影響程序不變量檢測(cè)性能和效率的重要因素，基于此，如何降低以上因素的影響是研究者需要進(jìn)一步研究的問題；雖然已有不變量檢測(cè)方法對(duì)Daikon預(yù)置庫形式進(jìn)行了大量的擴(kuò)充，但是，對(duì)矩形函數(shù)、積分函數(shù)等較為復(fù)雜的函數(shù)并未涉及，未來程序不變量檢測(cè)方法的研究應(yīng)該著眼于這些問題的研究和解決上；除此之外，程序不變量在新型軟件中的應(yīng)用亦有待更進(jìn)一步的研究。

參考文獻(xiàn)：

[1] Ernst M D，Notkin D.Dynamically discovering likely program invariants[J].Software Engineering IEEE Transactions on，2001，27（2）：99-123.endprint

[2] University N H，Hengyang H，Liu C，et al.Dynamically Discovering Likely Program Invariants Based on the Contract[J].2006.

[3] http：//plse.cs.washington.edu/daikon/

[4] Csallner C，Tillmann N，Smaragdakis Y.DySy：dynamic symbolic execution for invariant inference[C] //ACM/IEEE International Conference on Software Engineering.2015：281-290.

[5] Bocchi L，Honda K，Tuosto E，et al.A theory of design-by-contract for distributed multiparty interactions[C] //International Conference on Concurrency Theory.Springer-Verlag，2010：162-176.

[6] Baliga A，Ganapathy V，Iftode L.Automatic Inference and Enforcement of Kernel Data Structure Invariants[C] //Computer Security Applications Conference. IEEE Computer Society，2008：77-86.

[7] 李玉燕，陽小華，吳取勁.基于GEP-RNC的指數(shù)對(duì)數(shù)型程序不變量發(fā)現(xiàn)方法[J].南華大學(xué)學(xué)報(bào)，2017，31（1）：72-76.

[8] Wei J，Zhu F，Shinjo Y.Static analysis based invariant detection for commodity operating systems[J]. Computers & Security，2014，43（6）：49-63.

[9] Roest D，Deursen A V，Mesbah A.Invariant-Based Automatic Testing of Modern Web Applications[J].IEEE Transactions on Software Engineering，2012，38（1）：35-53.

[10] 單錦輝，姜瑛，劉江紅，等.基于合約的構(gòu)件易測(cè)試性設(shè)計(jì)支撐工具的設(shè)計(jì)與實(shí)現(xiàn)[J] .北京大學(xué)學(xué)報(bào)：自然科學(xué)版，2005，（5）：815-819.endprint