劉志明　時小芳　李萌　劉杰

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

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

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

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

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

1 程序不變量檢測工具

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

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

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

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

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

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

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

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

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

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

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

2.1 其他方法

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

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

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

4 總結(jié)與展望

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

參考文獻：

[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ù)對數(shù)型程序不變量發(fā)現(xiàn)方法[J].南華大學(xué)學(xué)報，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)件易測試性設(shè)計支撐工具的設(shè)計與實現(xiàn)[J] .北京大學(xué)學(xué)報：自然科學(xué)版，2005，（5）：815-819.endprint