模型檢測技術在程序內存泄漏檢測中的應用

陳宇星

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

模型檢測技術在程序內存泄漏檢測中的應用

陳宇星

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

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

內存泄漏檢測；模型檢測；內存錯誤；系統文獻綜述

0 引言

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

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

1 研究方法

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

（1）制定計劃

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

①提出研究問題

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

問題2：模型檢測技術在內存泄漏檢測上應用的不足和發展前景？

②檢索策略

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

③篩選原則

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

（2）執行計劃

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

（3）完成文獻綜述報告

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

2 研究結果

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

2.1 基于模型檢測的內存泄漏檢測方法

（1）TMC（Type and Model Checking）

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

（2）MLAB(Memory Leak Analysis for Binaries)

MLAB是用于檢測二進制可執行文件中的內存泄漏漏洞的框架方案，它能把二進制形式的代碼恢復成同機器不相干的編譯中間表示形式，還能將程序中的控制流與數據流信息恢復過來，然后利用模型檢測算法來分析恢復過來的控制流和數據流信息，從而檢測出被測程序中的內存泄漏[5]。MLAB框架中使用了上述TMC算法。MLAB不需要掌握任何與源代碼有關的信息，僅僅根據程序的二進制形式就可以恢復程序的控制流和數據流信息。MLAB具有不錯的可擴展性，是對二進制程序實施屬性分析的一種常用的方法[5]。

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

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

2.2 基于模型檢測的內存泄漏檢測工具

（1）CodeAuditor

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

（2）WBoxTool結合Blast

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

（3）Goanna

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

（4）X86EBMC(X86 Executable Bounded Model Check)

X86EBMC[11]是一個使用了有界模型檢測方法的針對可執行文件的模型檢測工具，能夠檢測內存泄漏、緩存溢出等漏洞。它是反匯編工具IDA Pro的插件，因為采用了面向對象的方法實現，因此其可擴展性和跨平臺性的較強。X86EBMC采用LTL線性時序邏輯來描述系統的安全屬性，由于模型檢測器SPIN主要用于檢測LTL公式的可滿足性，所以X86EBMC采用SPIN作為模型檢測模塊使用的工具。

（5）LLBMC

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

（6）F-soft

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

（7）CMC

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

（8）CBMC

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

2.3 基于模型檢測的內存泄漏檢測方法與工具的比較

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

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

3 結語

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

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

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

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

[3]聶坤明,張莉,樊志強.軟件產品線可變性建模技術系統綜述[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]趙振西.一種針對可執行代碼的內存泄漏靜態分析方案[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]付曉毓，朱利，顧偉.基于模型檢測的內存泄露靜態測試方法[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