記憶體洩漏是記憶體資源不正常消耗問題的一種，由於程式設計師的疏忽或
是設計錯誤造成程序未能釋放已經不再使用的記憶體，這是由於一般程式設計師
在撰寫程式時，不經意使用了已經釋放的資源或是會習慣地假設系統有無限多的
資源可供使用。隨著網際網路的普及化，駭客可以利用記憶體洩漏所造成的系統
漏洞來進行阻斷服務攻擊，使得記憶體洩漏的現象到現在依然影響系統甚鉅，儘
管有許多檢測工具與方法不斷的被發明出來，仍有未盡完善之處。
模型檢驗是一種驗證有限狀態機（finite-state machine）中的時序邏輯
（temporal properties）的一種技術，可以針對所有可能的狀態進行檢驗，在近年
來才逐漸應用在軟體上面。本研究的目的在於希望能夠利用模型檢驗的技術，並
結合先前對於資源測試的研究所找出的準則，利用模型檢驗工具來檢測C語言的
程式碼是否有記憶體洩漏的現象。

none

第一章 緒論 1
第一節 研究背景 1
第二節 研究動機 2
第三節 研究目的與問題描述 3
第四節 論文架構 4
第二章 文獻探討 5
第一節 軟體測試（Software Testing） 5
第二節 記憶體管理問題（The Memory Management Problems） 7
一、緩衝區溢位（Memory leak） 7
二、雙重釋放（Double free） 8
三、記憶體洩漏（Memory leak） 9
第三節 資源測試（Resource-Oriented Testing） 11
第四節 模型檢驗（Model Checking） 14
一、模型檢驗的過程 14
二、時序邏輯（Temporal logic） 15
三、模型檢驗的演進 18
四、軟體模型檢驗（Software model checking, SMC） 20
第三章 實驗架構與實作 22
第一節 實驗工具 22
一、模型檢驗工具：ANSI-C bounded model checker 22
二、以斷言為基礎的驗證（Assertion-based verification） 23
第二節 實驗流程 28
一、第一階段：初步分析（Initial analysis） 28
二、第二階段：插裝斷言（Instrument assertion） 30
四、第四階段：回饋並修正（Feedback for modification） 33
第四章 實驗結果 34
第一節 案例分析 35
一、經常性的記憶體洩漏 35
二、偶發性的記憶體洩漏 37
三、一次性的記憶體洩漏 38
第二節 分析結果 39
第五章 結論 41
第六章 研究限制與未來方向 42
參考文獻 43

Armando, A., Mantovani, J., & Platania, L. (2009). Bounded model checking of software using smt solvers instead of sat solvers. International Journal on Software Tools for Technology Transfer (STTT), 11(1), 69-83.
Beyer, D., Henzinger, T., Jhala, R., & Majumdar, R. (2005). Checking memory safety with blast. Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE), 2–18.
Beyer, D., Henzinger, T., Jhala, R., & Majumdar, R. (2007). The software model checker blast. International Journal on Software Tools for Technology Transfer (STTT), 9(5), 505-525.
Biere, A., Cimatti, A., Clark, E., Zhu, Y., & SCIENCE, C.-M. U. P. P. S. O. C. (1999). Symbolic model checking without bdds.
Bryant, R. (1986). Graph-based algorithms for boolean function manipulation. IEEE Transactions on computers.
Burch, J., Clarke, E., Long, D., McMillan, K., & Dill, D. (1994). Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4), 401-424.
Burch, J., Clarke, E., McMillan, K., Dill, D., & Hwang, L. (1990). Symbolic model checking: 10 20 states and beyond. Logic in Computer Science, 1990. LICS'90, Proceedings., Fifth Annual IEEE Symposium on e, 428-439.
Bush, W., Pincus, J., & Sielaff, D. (2000). A static analyzer for finding dynamic programming errors. Software: Practice and Experience, 30(7), 775-802.
Checking, C. The cprover user manual.
Chen, H., Dean, D., & Wagner, D. (2004). Model checking one million lines of c code. Proceedings of the 11th Annual Network and Distributed System Security Symposium, 171–185.
Chou, A., Yang, J., Chelf, B., Hallem, S., & Engler, D. (2001). An empirical study of operating systems errors. Proceedings of the eighteenth ACM symposium on Operating systems principles, 73-88.
Clarke, E., Emerson, E., & Sistla, A. (1986). Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM transactions on Programming Languages and Systems, 8(2), 244-263.
Clarke, E., Grumberg, O., & Long, D. (1994). Model checking and abstraction. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(5), 1512-1542.
Clarke, E., & Kroening, D. (2003). Ansi-c bounded model checker user manual.
Clarke, E., Kroening, D., & Lerda, F. (2004). A tool for checking ansi-c programs. Lecture Notes in Computer Science, 168-176.
Clarke, E., Kroening, D., & Yorav, K. (2003). Behavioral consistency of c and verilog programs using bounded model checking. Design Automation Conference, 2003. Proceedings, 368-371.
Clarke, E. M., Grumberg, O., & Peled, D. (2001). Model checking: Cambridge: MIT Press.
Common vulnerabilities and exposures. from http://cve.mitre.org/
Cowan, C., Pu, C., Maier, D., Hinton, H., Walpole, J., Bakke, P., et al. (1998). Stackguard: Automatic adaptive detection and prevention of buffer-overflow attacks. Proceedings of the 7th USENIX Security Conference, 78.
Demri, S., & Schnoebelen, P. (1998). The complexity of propositional linear temporal logics in simple cases (extended abstract). Proceedings of the 15th Annual Symposium on Theoretical Aspects of Computer Science, 61-72.
Gelperin, D., & Hetzel, B. (1988). The growth of software testing. Communications of the ACM, 31(6), 687-695.
Hastings, R., & Joyce, B. (2003). Purify: Fast detection of memory leaks and access errors. 1-10.
Havelund, K., & Pressburger, T. (2000). Model checking java programs using java pathfinder. International Journal on Software Tools for Technology Transfer (STTT), 2(4), 366-381.
Heine, D. (2004). Static memory leak detection.
Heine, D., & Lam, M. (2003). A practical flow-sensitive and context-sensitive c and c++ memory leak detector. ACM SIGPLAN Notices, 38(5), 168-181.
Huth, M., & Ryan, M. (2004). Logic in computer science: Modelling and reasoning about systems: Cambridge University Press.
Ivančić, F., Yang, Z., Ganai, M., Gupta, A., & Ashar, P. (2008). Efficient sat-based bounded model checking for software verification. Theoretical Computer Science, 404(3), 256-274.
Jhala, R., Majumdar, R., & Sutre, G. Blast: Berkeley lazy abstraction software verification tool Retrieved June, 30, 2009, from http://mtc.epfl.ch/software-tools/blast/
Ku, K. (2008). Software model-checking: Benchmarking and techniques for buffer overflow analysis.
Merz, S. (2001). Model checking: A tutorial overview. Lecture Notes in Computer Science, 3-38.
Miihlberg, J., & Liittgen, G. (2007). Blasting linux code. Formal Methods Applications and Technology: 11th International Workshop, FMICS 2006 and 5th International Workshop, PDMC 2006, Bonn, Germany, August 26-27, and August 31, 2006: Revised Selected Papers, 211.
Myers, G. J., Badgett, T., Thomas, T. M., & Sandler, C. (2004). The art of software testing: John Wiley and Sons.
Post, H., & Kuchlin, W. (2007). Integrated static analysis for linux device driver verification. Lecture Notes in Computer Science, 4591, 518.
Rabinovitz, I., & Grumberg, O. (2005). Bounded model checking of concurrent programs. Computer-Aided Verification (CAV), 82–97.
Regehr, J., Cooprider, N., Archer, W., & Eide, E. (2006). Efficient type and memory safety for tiny embedded systems. Proceedings of the 3rd workshop on Programming languages and operating systems: linguistic support for modern operating systems.
Slam. Retrieved June, 30, 2009, from http://research.microsoft.com/en-us/projects/slam/
Vaidyanathan, K., & Trivedi, K. (1999). A measurement-based model for estimation of resource exhaustion inoperational software systems. Software Reliability Engineering, 1999. Proceedings. 10th International Symposium on, 84-93.
Visser, W., Havelund, K., Brat, G., Park, S., & Lerda, F. (2003). Model checking programs. Automated Software Engineering, 10(2), 203-232.
Whittaker, J., & Thompson, H. (2003). How to break software security: Addison Wesley.
Yang, C., Souter, A., & Pollock, L. (1998). All-du-path coverage for parallel programs. ACM SIGSOFT Software Engineering Notes, 23(2), 153-162.
劉威成 (2007). 將資源使用分析應用於軟體測試. 中山大學.
蔡昌憲, 許立文, 吳孟勳, & 黃世昆 (2008). 作業系統核心安全驗證技術探討. 資訊安全通訊, 14(2).