陳宇星

（四川大學計算機學院，成都 610000）

模型檢測技術在程序內(nèi)存泄漏檢測中的應用

陳宇星

（四川大學計算機學院，成都 610000）

軟件開發(fā)常用的動態(tài)內(nèi)存管理技術雖然使得程序的設計更靈活卻很容易造成內(nèi)存管理漏洞，特別是內(nèi)存泄漏問題。內(nèi)存泄漏的堆積會導致程序運行異常甚至崩潰，因此內(nèi)存泄漏檢測是一個長期熱門的研究課題。而模型檢測技術是基于對程序所有可能執(zhí)行路徑的盡可能地仿真來檢測出程序中潛在的漏洞，所以可以將模型檢測技術用于程序內(nèi)存泄漏檢測中。采用系統(tǒng)化文獻綜述的方法歸納總結應用模型檢測技術的內(nèi)存泄漏檢測方法和工具。

內(nèi)存泄漏檢測；模型檢測；內(nèi)存錯誤；系統(tǒng)文獻綜述

0 引言

現(xiàn)階段的動態(tài)內(nèi)存機制雖然使得程序的設計更靈活和方便，但這個機制很容易造成內(nèi)存錯誤，其中內(nèi)存泄漏又是最難檢測并定位的。因此，如何有效檢測程序中的內(nèi)存泄漏是一個長期熱門的研究課題。內(nèi)存泄漏（Memory Leak）是由于程序在運行過程中動態(tài)分配的內(nèi)存不再使用了卻沒有被及時釋放造成的[1]。在這種情況下，程序不斷的運行，泄漏的內(nèi)存會不斷地增加，程序的性能也會因此而不斷下降，甚至程序會由于內(nèi)存被耗盡而崩潰。對于嵌入式系統(tǒng)這類內(nèi)存有限的系統(tǒng)或者服務器這類會運行很長時間的系統(tǒng)來說,內(nèi)存泄漏是個十分嚴重的缺陷。因此盡早地檢測到并處理程序中的內(nèi)存泄漏問題是十分必要的。

模型檢測（Model Checking）技術是一種通過窮舉搜索有限狀態(tài)空間來實現(xiàn)對模型的檢測的自動驗證技術，已經(jīng)越來越被重視并將其應用到了廣泛的范圍當中[2]。因此這篇論文著重對模型檢測技術在C/C++程序中的內(nèi)存泄漏檢測的應用進行了綜述分析。為研究學者們下一步的研究課題提供綜合性的參考，也能為工業(yè)界應用這個領域的技術提出一個決策的依據(jù)。

1 研究方法

系統(tǒng)文獻綜述(Systematic Literature Review)又被稱作系統(tǒng)評價，是一種針對某一研究問題開展的基于文獻的系統(tǒng)化綜述方法[3]。一開始主要用于醫(yī)學領域以及社會學研究領域，在2004年被引入了軟件工程領域，系統(tǒng)綜述主要包含了3個階段[3]:

（1）制定計劃

在這個階段對綜述的需求進行分析，并確定開展此綜述的目的，然后設計出展開綜述的步驟方案，以便引導后續(xù)的工作。主要要分以下三步：

①提出研究問題

問題1：現(xiàn)有的應用了模型檢測技術的內(nèi)存泄漏檢測方法和工具有哪些？

問題2：模型檢測技術在內(nèi)存泄漏檢測上應用的不足和發(fā)展前景？

②檢索策略

這篇論文用于分析的數(shù)據(jù)來源于IEEE Xplore，Web of Science、ACM以及CNKI等數(shù)據(jù)庫。檢索詞包括：“內(nèi)存泄漏”、“模型檢測”、“內(nèi)存錯誤”、“memory leak”、“model checking”、“memory error”。

③篩選原則

對于檢索出來的文獻通過其發(fā)表年限、被引用次數(shù)、發(fā)表期刊、篇幅以及主題是否是關于模型檢測技術在內(nèi)存泄漏檢測中的應用來決定是否將其錄入最終用來分析的論文庫。

（2）執(zhí)行計劃

這個階段按第一步制定的檢索策略和篩選原則來收集能夠回答研究問題的文獻并進行數(shù)據(jù)提取與分析。最終檢索到的文獻通過第一步消重，刪除掉錄入Endnote中的重復論文后共有155條記錄；第二步通過閱讀題目和摘要來過濾與研究主題不相關的論文；第三步刪除掉短文和引用次數(shù)很少的論文。通過以上步驟，最終確定選入的文獻共53篇。

（3）完成文獻綜述報告

最終被錄入的研究，按照文獻綜述的需求來提取數(shù)據(jù)，對所獲得的數(shù)據(jù)進行歸納分析,并對結果給出解釋。最終整個綜述過程和結果，形成研究報告。

2 研究結果

基于模型檢測的內(nèi)存泄漏檢測通常是對被測程序進行語法、詞法分析，然后使用模型檢測算法來判斷分析后的結果。而各種方法用于分析的程序的形式不同，有些方法是直接分析被測程序的源代碼，有些方法是分析被測程序的匯編語言形式的代碼，但他們獲得匯編代碼的方式又可能不同，例如MLAB框架和X86EBMC工具，它們分析的匯編代碼是由被測程序的可執(zhí)行文件經(jīng)過反匯編后獲得的，而LLBMC工具則是通過編譯被測程序的源代碼來獲得匯編代碼的。各種內(nèi)存泄漏檢測方法使用的模型檢測方法和工具也不盡相同。

2.1 基于模型檢測的內(nèi)存泄漏檢測方法

（1）TMC（Type and Model Checking）

TMC是一種結合了類型分析技術和模型檢測技術的檢測內(nèi)存泄漏的靜態(tài)分析方法，利用模型檢測來對使用類型分析方法得出的結果進行更仔細的檢查[4]。TMC方法首先是通過類型分析來獲得程序的控制流圖和數(shù)據(jù)流信息（如別名分析），然后分析出的結果就會作為模型檢測分析的對象輸入模型檢測模塊[4]。最終得出檢測結果。TMC通過將模型檢測方法與類型分析方法的優(yōu)點結合起來，可以獲得比單用類型分析方法更為準確的結果[4]。但是其分析工具功能還不夠完善，還不能有效地對大型軟件系統(tǒng)進行屬性檢查。

（2）MLAB(Memory Leak Analysis for Binaries)

MLAB是用于檢測二進制可執(zhí)行文件中的內(nèi)存泄漏漏洞的框架方案，它能把二進制形式的代碼恢復成同機器不相干的編譯中間表示形式，還能將程序中的控制流與數(shù)據(jù)流信息恢復過來，然后利用模型檢測算法來分析恢復過來的控制流和數(shù)據(jù)流信息，從而檢測出被測程序中的內(nèi)存泄漏[5]。MLAB框架中使用了上述TMC算法。MLAB不需要掌握任何與源代碼有關的信息，僅僅根據(jù)程序的二進制形式就可以恢復程序的控制流和數(shù)據(jù)流信息。MLAB具有不錯的可擴展性，是對二進制程序?qū)嵤傩苑治龅囊环N常用的方法[5]。

（3）基于SMT的有界模型檢測方法

2010年，Carsten Sinz等人提出了一種基于有界模型檢測（BMC）來檢測C程序中的內(nèi)存錯誤（非法內(nèi)存方法、堆棧溢出、內(nèi)存泄漏、非法釋放等）的方法[6]。這個方法不是直接在C源碼上檢測，而是檢測一種由LLVM（Low Level Virtual Machine）編譯器框架產(chǎn)生的類似RISC匯編語言的中介碼。因此這個方法的分析結果就跟實際運行程序檢測到的結果相近。后端的SMT求解器采用Boolector或者STP工具。后文提到的LLBMC工具采用的是STP工具。LLVM編譯器前端（llvm-gcc）將C程序源代碼轉化成LLVM-IR程序，之后把它輸入循環(huán)展開/函數(shù)內(nèi)聯(lián)模塊，輸出的結果是被轉化的匯編碼，循環(huán)展開以及函數(shù)內(nèi)聯(lián)是由LLVM的庫提供的代碼完成的，然后將被轉化的代碼輸入到邏輯編碼模塊，共同輸入的還有一個內(nèi)存模型，這個內(nèi)存模型包含了C程序中的關于內(nèi)存訪問的語義信息。邏輯編碼模塊輸出的位向量和數(shù)組的邏輯形式通過SMT求解器后輸出驗證的結果以及錯誤路徑，這個錯誤報告是由LLVM的調(diào)試信息模塊產(chǎn)生的。

2.2 基于模型檢測的內(nèi)存泄漏檢測工具

（1）CodeAuditor

CodeAuditor[7]是一個包含了前端預處理模塊和后端模型檢測模塊的內(nèi)存泄漏檢測原型工具。它的實現(xiàn)原理是將約束分析和模型檢測技術相結合，通過跟蹤與緩存相關的變量的內(nèi)存大小并在潛在漏洞點插入約束斷言，這樣就將漏洞檢測轉換成了通過模型檢測來驗證這些斷言的可達性。通過對插入了斷言的代碼進行程序切片來減小程序的大小，從而減輕了程序系統(tǒng)狀態(tài)的組合爆炸給模型檢測帶來的負擔。由于程序切片并沒有改變切片標準重的變量的值，所以當程序被切片時，斷言的安全將不會被改變。CodeAuditor基于程序分析和模型檢測工具BLAST，具有較小的錯誤報警率。

（2）WBoxTool結合Blast

付曉毓等人提出了一種結合了靜態(tài)分析、代碼插裝以及模型檢測技術的內(nèi)存泄漏故障的靜態(tài)檢測系統(tǒng)，這個系統(tǒng)與CodeAuditor框架類似。它的主要原理是首先構建出指針屬性的約束條件，接著以斷言的形式將其插入到程序源代碼當中，這樣檢測程序中的內(nèi)存泄漏就被轉化成了判定源代碼中特定位置的斷言的可達性[8]。最后使用一個模型檢測工具來判定那些斷言，若判定的結果是不正確，那么該位置處的代碼就有可能會造成內(nèi)存泄漏[8]。這個靜態(tài)檢測系統(tǒng)由函數(shù)靜態(tài)信息提取模塊、插裝模塊以及模型檢測模塊等三個模塊構成，其中模型檢測模塊使用了由UC Berkeley開發(fā)的針對C程序的安全性驗證的工具——Blast模型檢測工具[8]。WBoxTool與Blast工具的結合雖然在小型實例程序檢測上取得了較好的成果，但是要將其應用到大規(guī)模的軟件上還遠遠不夠。

（3）Goanna

2007年，F(xiàn)ehnker等人開發(fā)出了第一個使用了模型檢測器NuSMV的C/C++靜態(tài)源碼分析工具——Goanna[9]。那時的Goanna只是一個原型工具，它可以分析程序的的部分特性。用戶需要做的僅是提供一個CTL（Computation Tree Logic）的規(guī)格說明并且以查詢語句為單位來定義這個規(guī)格說明的原子命題（Atomic Proposition）。把程序翻譯成控制流圖、模式匹配、隨后的貼標以及報告錯誤，這些過程都是全自動的，大大減小了用戶的負擔。盡管Goanna在實際使用上已經(jīng)足夠，但是其性能仍然有很大的空間有待改善。針對Goanna中存在的各種問題，F(xiàn)ehnker等人在2012年開發(fā)出了最新版本的Goanna解決了性能問題。并且，最新版的Goanna除了可以執(zhí)行內(nèi)存泄漏檢測外，還能執(zhí)行超過250個有很高價值的檢查，例如數(shù)組越界、空指針錯誤、內(nèi)存損壞、字符串溢出、雙重釋放、安全性缺陷、算數(shù)錯誤、可移植性缺陷等[10]。最新開發(fā)的Goanna不需要編譯或執(zhí)行被測程序，只需要分析程序的源代碼就可以自動地找到程序中的漏洞，因此在軟件開發(fā)生命周期的最早階段就能及時發(fā)現(xiàn)漏洞，所以，用戶可以在降低開發(fā)成本的同時提高其代碼的質(zhì)量，也節(jié)約了產(chǎn)品開發(fā)的時間，使其能夠更快地進入市場。Goanna可以將檢測到的缺陷通過一個方便使用的接口繪制成可視化的報告。

（4）X86EBMC(X86 Executable Bounded Model Check)

X86EBMC[11]是一個使用了有界模型檢測方法的針對可執(zhí)行文件的模型檢測工具，能夠檢測內(nèi)存泄漏、緩存溢出等漏洞。它是反匯編工具IDA Pro的插件，因為采用了面向?qū)ο蟮姆椒▽崿F(xiàn)，因此其可擴展性和跨平臺性的較強。X86EBMC采用LTL線性時序邏輯來描述系統(tǒng)的安全屬性，由于模型檢測器SPIN主要用于檢測LTL公式的可滿足性，所以X86EBMC采用SPIN作為模型檢測模塊使用的工具。

（5）LLBMC

2012，Carsten Sinz等人根據(jù)他們在2010年提出的方法，開發(fā)了一個基于有界模型檢測的靜態(tài)軟件分析工具LLBMC[12]，在2013年，又更新了最新版本的LLBMC。它可以用于查找C程序中的漏洞。LLBMC是全自動的，它僅需要極少的前期準備和用戶交互，囊括了所有的C結構。通過高度精確地將內(nèi)存訪問操作模型化從而找到很難被檢測到的內(nèi)存錯誤，例如內(nèi)存泄漏。由于LLBMC的高精確性，它幾乎沒有誤報。

（6）F-soft

F-soft[13-14]是由Ilya Shlyakhter等人開發(fā)的一個原型軟件模型檢測工具，提供了一系列模型軟件的抽象，并且使用了針對軟件的自定義的基于SAT（satisfiability）和基于BDD（Binary Decision Diagrams）的有界模型檢測技術。主要用于檢測順序C程序。它除了能檢測內(nèi)存泄漏漏洞以外，還能檢測數(shù)組邊界違規(guī)、空指針引用、除零等漏洞。

（7）CMC

Madanlal Musuvathi等人開發(fā)了一種模型檢測工具——CMC[15]，它的特點是直接檢測C/C++的實現(xiàn)代碼，而不是像F-soft那樣檢測一個系統(tǒng)行為的抽象形式，還有一個特點是可以保存狀態(tài)以避免重復的狀態(tài)探索。CMC有兩個主要的優(yōu)點：減少了錯誤的漏報以及減少了因為誤報而造成的時間的浪費。CMC可以檢測的漏洞有：指針訪問違規(guī)、程序斷言失敗、內(nèi)存泄漏等。

（8）CBMC

CBMC[16]是卡內(nèi)基·梅隆大學的Edmund Clarke等人開發(fā)的一個形式化驗證底層ANSI-C程序的工具。它的驗證過程是高度自動的，用戶僅需要輸入BMC的邊界就行。它采用的模型檢測技術是基于SAT的有界模型檢測技術。CBMC除了可以檢測內(nèi)存泄漏問題外，還能檢測的錯誤有指針安全、數(shù)組越界等。

2.3 基于模型檢測的內(nèi)存泄漏檢測方法與工具的比較

表1展示了上述方法和工具的比較。

表1 各模型檢測工具和方法的對比

3 結語

動態(tài)內(nèi)存管理機制方便了內(nèi)存的分配與釋放，但當程序結構比較復雜的時候,很容易因為開發(fā)人員的大意造成邏輯錯誤，從而可能會使得程序產(chǎn)生內(nèi)存泄漏。內(nèi)存泄漏的堆積會對程序的性能造成很大的影響，因此有效并及時地檢測出程序中潛在的內(nèi)存泄漏是意義深遠的，它也是確保軟件產(chǎn)品質(zhì)量的必要方式。

本文采用系統(tǒng)化文獻綜述的方法，分析了關于模型檢測技術在內(nèi)存泄漏檢測中的應用方面的成果，綜述分析了應用了模型檢測技術的內(nèi)存泄漏檢測方法和工具的基礎結構、應用的技術以及其優(yōu)缺點等方面的信息。同時也指出了這個研究領域亟待解決的問題以及未來的研究趨勢。因此，這篇論文可以為研究學者們下一步的研究題目提供綜合性的參考，也能為工業(yè)界應用這個領域的技術提出一個決策的依據(jù)。

[1]王喆.C/C++代碼內(nèi)存泄漏缺陷檢測方法研究[C]，2012．

[2]趙振西.一種混合式內(nèi)存泄漏靜態(tài)檢測方法[J].小型微型計算機系統(tǒng),2008:1935-1939.

[3]聶坤明,張莉,樊志強.軟件產(chǎn)品線可變性建模技術系統(tǒng)綜述[J].Journal of Software,2013.

[4]Hu,Y,et al.Hybrid Static Method for Memory Leak Detection[J].Journal of Chinese Computer Systems,2008.

[5]趙振西.一種針對可執(zhí)行代碼的內(nèi)存泄漏靜態(tài)分析方案[N].中國科學技術大學學報,2009.

[6]Sinz,C,S.Falke,and F.Merz.A Precise Memory Model for Low-Level Bounded Model Checking[C].In Proceedings of the 5th International Conference on Systems Software Verification，2010.

[7]Lei,W,Z.Qiang,Z.PengChao.Automated Detection of Code Vulnerabilities Based on Program Analysis and Model Checking[C].2008 Eighth IEEE International Working Conference on Source Code Analysis and Manipulation(SCAM 2008),2008:165-73.

[8]付曉毓，朱利，顧偉.基于模型檢測的內(nèi)存泄露靜態(tài)測試方法[J].微電子學與計算機,2010(10):170-173.

[9]Fehnker,A,et al.Model Checking Software at Compile Time[C].Theoretical Aspects of Software Engineering,2007.

[10]Fehnker,A.，R.Huuck.Model Checking Driven Static Analysis for the Real World:Designing and Tuning Large Scale Bug Detection [C].Innovations in Systems and Software Engineering,2013，9(1):45-56.

[11]Tang,Z.-c,et al.Bounded Model Checking Security Properties of Executables[J].Journal of Chinese Computer Systems,2008，29(9): 1674-8.

[12]Merz,F,S.Falke,C.Sinz.LLBMC:Bounded Model Checking of C and C++Programs Using a Compiler IR.in Verified Software: Theories,Tools,Experiments.2012,Springer.146-161.

[13]Ivancic,F,et al.Model Checking C Programs Using F-Soft[C].in Computer Design:VLSI in Computers and Processors,2005.ICCD 2005.Proceedings.2005 IEEE International Conference on.2005.IEEE.

[14]Ivan i,F,et al.F-Soft:Software Verification Platform.in Computer Aided Verification.2005.Springer.

[15]Musuvathi,M,et al.CMC:A Pragmatic Approach to Model Checking Real Code.ACM SIGOPS Operating Systems Review,2002.36 (SI):75-88.

[16]Clarke,E,D.Kroening,and F.Lerda.A Tool for Checking ANSI-C Programs.in Tools and Algorithms for the Construction and Analysis of Systems.2004,Springer.168-176.

The Memory Leak Detections with Model Checking

CHEN Yu-xing

（College of Computer Science,Sichuan University，Chengdu610000）

The popular dynamic memory management technology used in software development makes the design process more flexible,but it is also very likely to cause memory management issues,especially the memory leak problem.Memory leaks can cause abnormal operation or even crash the program,so memory leak detection is a hot research topic for a long time.The model checking technology is based on the detection of all possible execution paths of the program as simulation to detect run-time errors,so model checking can be used in memory leak detection.Therefore,draws on a systematic literature review methods to summarize the existing methods and tools of memory leak detection which uses the model checking technology.

Memory Leak Detection;Model Checking;Memory Error;Systematic Literature Review

1007-1423（2017）04-0053-05

10.3969/j.issn.1007-1423.2017.04.012

陳宇星（1993-），女，四川眉山人，碩士研究生，研究方向為軟件自動化測試

2016-11-29

2016-01-13