程序不變量檢測技術研究進展

劉志明　時小芳　李萌　劉杰

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

關鍵詞：程序不變量；動態檢測；Daikon

中圖分類圖：TP311 文獻標志碼：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

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

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

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

1 程序不變量檢測工具

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

Daikon先后用Python、java語言開發過，可以動態檢測C、C ++、Java等多種程序的屬性，且支持記錄結構化數據源[3]；Diduce是受Daikon啟發開發得來的，側重于輔助程序員查看程序中存在的漏洞，并定位錯誤的具體位置，已經被成功應用在JSSE等較大規模的程序排錯[2]；TDDPA針對面向對象程序不變量設計并實現的一種交互式的動態檢測工具，是基于關系數據庫理論提出的；DySy使用了強大的符號執行和簡化引擎實現了動態符號執行技術，大幅度地提高了推斷不變量的質量。它們的檢測過程和特點如表1所示：endprint

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

2 程序不變量檢測技術

程序不變量檢測技術是為了擴充Daikon的預置庫形式而提出的。基于合約的程序不變量檢測等多種檢測技術都遵循圖1理論模型。

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

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

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

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

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

（5） 接口重載不變量檢測：把前置條件和后置條件分成兩個單獨的階段來處理，先提取所有可執行方法的前置條件，然后再針對每個接口重載函數，查找與之相符的前置條件，若找到，則提取出與之對應的后置條件，以完成重載方法不變量的提取[6]。有效地解決了面向對象中方法調用時調用者和被調用者產生的不變量不一致的問題。但因為針對同一個測試用例運行了兩次程序，效率不高。

2.1 其他方法

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

3 程序不變量的應用

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

4 總結與展望

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

參考文獻：

[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的指數對數型程序不變量發現方法[J].南華大學學報，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] 單錦輝，姜瑛，劉江紅，等.基于合約的構件易測試性設計支撐工具的設計與實現[J] .北京大學學報：自然科學版，2005，（5）：815-819.endprint