論文使用權限 Thesis access permission:校內一年後公開,校外永不公開 campus withheld
開放時間 Available:
校內 Campus: 已公開 available
校外 Off-campus:永不公開 not available
論文名稱 Title |
應用模型檢驗於軟體資源測試 Applying Model Checking to Software Resource Testing |
||
系所名稱 Department |
|||
畢業學年期 Year, semester |
語文別 Language |
||
學位類別 Degree |
頁數 Number of pages |
51 |
|
研究生 Author |
|||
指導教授 Advisor |
|||
召集委員 Convenor |
|||
口試委員 Advisory Committee |
|||
口試日期 Date of Exam |
2009-07-20 |
繳交日期 Date of Submission |
2009-08-31 |
關鍵字 Keywords |
模型檢驗、資源測試、記憶體洩漏 none |
||
統計 Statistics |
本論文已被瀏覽 5781 次,被下載 0 次 The thesis/dissertation has been browsed 5781 times, has been downloaded 0 times. |
中文摘要 |
記憶體洩漏是記憶體資源不正常消耗問題的一種,由於程式設計師的疏忽或 是設計錯誤造成程序未能釋放已經不再使用的記憶體,這是由於一般程式設計師 在撰寫程式時,不經意使用了已經釋放的資源或是會習慣地假設系統有無限多的 資源可供使用。隨著網際網路的普及化,駭客可以利用記憶體洩漏所造成的系統 漏洞來進行阻斷服務攻擊,使得記憶體洩漏的現象到現在依然影響系統甚鉅,儘 管有許多檢測工具與方法不斷的被發明出來,仍有未盡完善之處。 模型檢驗是一種驗證有限狀態機(finite-state machine)中的時序邏輯 (temporal properties)的一種技術,可以針對所有可能的狀態進行檢驗,在近年 來才逐漸應用在軟體上面。本研究的目的在於希望能夠利用模型檢驗的技術,並 結合先前對於資源測試的研究所找出的準則,利用模型檢驗工具來檢測C語言的 程式碼是否有記憶體洩漏的現象。 |
Abstract |
none |
目次 Table of Contents |
第一章 緒論 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 |
參考文獻 References |
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). |
電子全文 Fulltext |
本電子全文僅授權使用者為學術研究之目的,進行個人非營利性質之檢索、閱讀、列印。請遵守中華民國著作權法之相關規定,切勿任意重製、散佈、改作、轉貼、播送,以免觸法。 論文使用權限 Thesis access permission:校內一年後公開,校外永不公開 campus withheld 開放時間 Available: 校內 Campus: 已公開 available 校外 Off-campus:永不公開 not available 您的 IP(校外) 位址是 3.144.28.50 論文開放下載的時間是 校外不公開 Your IP address is 3.144.28.50 This thesis will be available to you on Indicate off-campus access is not available. |
紙本論文 Printed copies |
紙本論文的公開資訊在102學年度以後相對較為完整。如果需要查詢101學年度以前的紙本論文公開資訊,請聯繫圖資處紙本論文服務櫃台。如有不便之處敬請見諒。 開放時間 available 已公開 available |
QR Code |