軟體安全日漸成為重要的研究主題，起因於越來越多的軟體攻擊行為發生，這些狀況有一部份是源自於程式語言本身的缺陷，而另一方面也是程式設計師本身的粗心所導致。因此，我們將藉由軟體偵測技術以減少這些問題。在論文中探討目前被廣泛運用的的程式漏洞-緩衝區溢位(Buffer overflow)，例如西元2003年八月造成重大損失的疾風(Blaster)病毒即利用此種漏洞進行破壞。為了防止此類型的漏洞，本論文使用KLEE的符號執行模組(symbolic execution model)並引入新的記憶體對映機制(memory map)來探測緩衝區溢位。相較於傳統的檢測工具，本論文所提出的工具可確實產生、可利用的測資來觸發漏洞的行為，進而證實漏洞的存在。這些測資事實上就是一組攻擊字串，有別於駭客手動方式產生，我們將提出自動產生的方法。

Software security is getting more important recently. There are more and more attacks than before. It is partially due to some design flaws of the programming language and the lack of secure programming practices by programmers. The most serious vulnerability this thesis concerns with is buffer overflow, present in many C/C++ programs, such as the Blaster worm. For preventing from such vulnerabilities, we use symbolic execution with a new memory model supported by KLEE to detect buffer overflow vulnerabilities. This thesis actually generates an exploitable input to trigger buffer overflow and verify the presence of the vulnerability. The input suites we generate are realistic attacks. Unlike the usual hacking methods with manual techniques to reason on the tainting paths, we propose methods to generate exploitable input automatically.

1. Introduction 1
1.1 Background 2
1.1.1 Common Vulnerabilities 2
1.1.2 Existing Detection Tactics 6
1.1.3 Random testing (Fuzzing) 7
1.1.4 Symbolic Execution 7
1.1.5 Concolic Testing 7
1.2 Motivation 9
1.3 Problem Description 11
1.4 Objective 15
2. Related Work 16
3. Method and Steps 18
3.1 New symbolic memory offset map 19
3.2 New symbolic memory function 20
3.3 Symbolic array index dereference approach 21
4 Implementation 22
4.1 Memory offset map 22
4.2 New Making Symbolic Strategy 26
4.3 Symbolic array index dereference handling 28
4.3.1 Memory dereference in LLVM IR form 29
4.3.2 Branch condition evaluation 31
4.4 Symbolic solution management 36
5 Result and Experiment 37
5.1 Trivial example of SAGE 37
5.2 Evaluations on real programs 38
5.3 Atypical symbolic analysis 39
6 Conclusion 43
7 Future works 43
Reference 44

[1] C. Lattner and V. Adve. LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation. In CGO , 2004.
[2] C. Cadar, D. Dunbar, D. Engler. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,In Stanford University 2008
[3] S. Nagarakatte, J. Zhao, M. Martin, S. A. Zdancewic. SoftBound: Highly Compatible and Complete Spatial Memory Safety for C, In University of Pennsylvania 2009
[4] E. Haugh and M. Bishop. Testing C programs for buffer overflow vulnerabilities. In Proceedings of the Network and Distributed System Security Symposium, February 2003.
[5] P. Godefroid, N. Klarlund, K. Sen. DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
[6] K. Sen, D. Marinov, and G. Agha. CUTE: A concolic unit testing engine for C. Technical Report UIUCDCS-R-2005-2597, UIUC, 2005.
[7] R. Majumdar and K. Sen. Hybrid concolic testing. In 29th International Conference on Software Engineering (ICSE'07), pages 416{426. IEEE, 2007.
[8] Koushik Sen. Concolic testing. ASE 2007
[9] N. Nethercote and J. Seward. Valgrind: A framework for heavyweight dynamic binary instrumentation, in Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007, pp. 89-100.
[10] W. Le and M. L. Soffa. Refining buffer overflow detection via demand-driven path-sensitive analysis, in Proceedings of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2007, pp. 63-68.
[11] Cristian Cadar, Paul Twohey, Vijay Ganesh, Dawson Engler. EXE: A System for Automatically Generating Inputs of Death Using Symbolic Execution, 2006
[12] J.Yang, C. Sar, P. Twohey, C. Cadar and D. Engler. Automatically Generating Malicious Disks using Symbolic Execution , Stanford University Computer Systems Laboratory
[13] Z. Lin X. Zhang D. Xu. Convicting Exploitable Software Vulnerabilities: An Efficient Input Provenance Based Approach, Department of Computer Sciences and CERIAS Purdue University
[14] H. Shahriar and M. Zulkernine. Mutation-based Testing of Buffer Overflow Vulnerabilities , School of Computing Queen’s University, Kingston, Ontario, Canada
[15] O. Crameri, R. Bachwani, T. Brecht, R. Bianchini, D. Kostic, W.Zwaenepoel.
Oasis: Concolic Execution Driven by Test Suites and Code Modifications , EPFL Technical report
[16] D.Vanoverberghe , N. Tillmann , F. Piessens. Test Input Generation for Programs with Pointers, Proceedings of the 15th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York UK, March 22-29 2009
[17] L. Ciortea, C. Zamfir, S. Bucur, V. Chipounov, G. Candea. Cloud9: A Software Testing Service , School of Computer and Communication Sciences
École Polytechnique Fédérale de Lausanne (EPFL), Switzerland
[18] B. Elkarablieh P. Godefroid M.Y. Levin. Precise Pointer Reasoning for Dynamic Test Generation, 2009
[19] J. Burnim K. Sen. CREST : Heuristics for Scalable Dynamic Test Generation. Presented at 23rd IEEE/ACM International Conference on Aitomated Software Engineering, ASE 2008
[20] J. C. King. Symbolic Execution and Program Testing, Communications
of the ACM, vol. 19, no. 7, pp. 385–394, 1976.
[21] R. Majumdar and K. Sen. Latest: Lazy dynamic test input generation. Technical Report UCB/EECS-2007-36, EECS Department, University of California, Berkeley, 2007.
[22] O. Ruwase and M. S. Lam. CRED : A practical dynamic buffer overflow detector. In Proceedings of the 11th Annual Network and Distributed System Security Symposium,pages 159–169, 2004
[23] Y. Younan , W.Joosen and F. Piessens. Security of memory allocators for C and C++. Department of Computer Science, K.U.Leuven, 2005
[24] Uno : http://spinroot.com/uno/
[25] ZZUF : http://caca.zoy.org/wiki/zzuf
[26] You-Siang Lin. CAST: Automatic and Dynamic Software Verification Tool, NCTU , Master thesis, 2009
[27] Richard W M Jones and Paul H J Kelly. Backwards-compatible bounds checking for arrays and pointers in C programs. Department of Computing Imperial College if Science, Technology and Medicine 180 Queen’s Gate, London.
[28] KLEE : http://klee.llvm.org/
[29] LLVM : http://llvm.org/
[30] CERT advisorie : http://www.cert.org/advisories/
[31] Cyber Security Bulletins : http://www.us-cert.gov/cas/bulletins/
[32] Snort 2.9.4.0 : http://www.snort.org/
[33] Asterisk : http://www.asterisk.org/downloads
[34] CVE : http://nvd.nist.gov/home.cfm