由於資訊領域的快速發展與應用，各類安全威脅日趨嚴重，而這些威脅都根源於軟體的缺陷，軟體安全性的探討因此成為重要的議題。這些議題中，最大的威脅來自於軟體缺陷經常性地被揭露、使得駭客的攻擊事件層出不窮，其中零日攻擊(zero-day attacks)更造成系統及經濟上的重大危害。我們以軟體發展過程的角度分析，瞭解到安全漏洞的修補過程，是一場與零日攻擊的時間競賽，若能儘早修補漏洞，將可大幅降低其威脅性。為了快速掌握漏洞，我們運用在軟體測試領域中，已被廣泛研究運用、自動尋找程式錯誤的方法。然而如何分析眾多的程式錯誤，優先尋找出安全性威脅的漏洞，仍是一個很困難的研究領域。在此論文中，我們將轉換角色，以攻擊者的角度來試圖產生攻擊程式碼、並將過程自動化，以此證明程式中存在安全性漏洞。我們提出基於符號執行的軟體測試方法，實作攻擊程式產生器，可任意攔截控制流程。此概念已實驗在多個真實的程式，證明此方法之可行性。

Due to the rapid deployment of information technology, the threats on information assets are getting more serious. These threats are originated from software vulnerabilities. The vulnerabilities bring about attacks. If attacks launched before the public exposure of the targeted vulnerability, they are called zero-day attacks. These attacks usually damage system and economy seriously. We have analyzed the process of zero-day attacks in the perspective of software process and recognize that it is a race competition between attacks and software patch development and deployment. If developers can fix the vulnerabilities as soon as possible, the threats will be significantly reduced. In order to faster the vulnerability finding process, we use the software testing techniques, focusing on finding bugs automatically. However, it is still hard to locate security vulnerabilities from a large number of bugs. In our paper, we switch to the roles of attackers and aim at generating attacks automatically to prove that a bug is a security vulnerability. Based on symbolic execution, we are able to automatically generate exploit for control-flow hijacking attacks and perform several experiments with real-world programs to prove our method is feasible.

摘要 i
Abstract ii
誌謝 iii
Contents iv
List of Listings vi
List of Figures vii
List of Tables viii
List of Algorithms ix
1 Introduction 1
1.1 Motivation 1
1.2 Objective 2
1.3 Overview 2
2 Background 3
2.1 Software Testing 3
2.1.1 Fuzz Testing 3
2.1.2 Symbolic Execution 4
2.1.3 Concolic Testing 5
2.2 Software Security 7
2.2.1 Vulnerability and Exploit 7
2.2.2 CPU Architecture and Operating System 7
2.2.2.1 Stack and Heap 8
2.2.3 Software Vulnerabilities 10
2.2.3.1 Stack Buffer Overflow 10
2.2.3.2 Off-by-one Overflow 10
2.2.3.3 Heap Buffer Overflow 10
2.2.3.4 Uninitialized Variable 10
2.2.3.5 Format String 11
2.2.4 Protection Mechanisms 12
2.3 Related Work 13
2.3.1 Symbolic Execution and Constraint Solving 13
2.3.2 Exploit Generation 13
3 Method 15
3.1 The Weakness of AEG 15
3.2 The Used Tool and Intuitive Idea 16
3.3 Our Method 18
3.3.1 EIP Register Corrupted Detection 18
3.3.2 Exploit Generation 19
3.3.2.1 Shellcode Injection 19
3.3.2.2 Nop Sled and Exploit Generation 20
3.3.3 Pointer Corrupted Detection 20
3.4 Path Selection 21
3.4.1 Concolic-mode Simulation 21
3.4.2 Code Selection 22
4 Implementation 24
4.1 Register Corruption Detection 24
4.2 Exploit Generation 27
4.2.1 Memory Model in S2E 27
4.2.2 Finding Symbolic Memory Blocks 27
4.2.3 Shellcode Injection 28
4.2.4 NOP Sled 30
4.2.5 Other Types of Exploit 33
4.2.5.1 Return-to-libc 33
4.2.5.2 Jump-to-register 34
4.3 Pointer Corruption Detection 35
4.4 Concolic-mode Simulation 35
4.5 Code Selection 37
5 Experimental Results 38
5.1 Testing Method and Environment 38
5.2 Sample Code 39
5.3 Other Types of Exploits 40
5.4 Real-world Programs 42
6 Conclusion and Further Work 44
6.1 Conclusion 44
6.2 Further Work 45
References 48
Appendices 49
A Sample Code and Exploits 49
A.1 Shellcode 49
A.2 Stack Buffer Overflow Vulnerability 49
A.3 Heap Buffer Overflow Vulnerability 51
A.4 Off-by-one Buffer Overflow Vulnerability 52
A.5 Uninitialized Variable Vulnerability 53
A.6 Format String Vulnerability 54

[1] T. Wang, T. Wei, Z. Lin, and W. Zou, “IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution,” in Proceedings of the Network and Distributed System Security Symposium (NDSS’09), San Diego, California, USA, February 2009.
[2] D. Molnar, X. C. Li, and D. Wagner, “Dynamic Test Generation to Find Integer Bugs in x86 Binary Linux Programs,” in Proceedings of the 18th USENIX Security Symposium, Montreal, Canada, August 2009, pp. 67–82.
[3] C. Cadar and D. R. Engler, “Execution Generated Test Cases: How to Make Systems Code Crash Itself,” in Proceedings of the 12th International SPIN Workshop on Model Checking Software, San Francisco, CA, USA, August 2005, pp. 2–23.
[4] C. S. P˘as˘areanu andW. Visser, “A survey of new trends in symbolic execution for software testing and analysis,” International Journal on Software Tools for Technology Transfer (STTT), vol. 11, no. 4, pp. 339–353, 2009.
[5] E. J. Schwartz, T. Avgerinos, and D. Brumley, “All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask),” in Proceedings of the 31st IEEE Symposium on Security and Privacy (S&P 2010), Berleley/Oakland, California, USA, May 2010, pp. 317–331.
[6] C. Cadar, P. Godefroid, S. Khurshid, C. S. P˘as˘areanu, K. Sen, N. Tillmann, and W. Visser, “Symbolic execution for software testing in practice: preliminary assessment,” in Proceedings of the 33rd International Conference on Software Engineering (ICSE’11), Waikiki, Honolulu , HI, USA, May 2011, pp. 1066–1071.
[7] P. Godefroid, N. Klarlund, and K. Sen, “DART: directed automated random testing,” in Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation (PLDI’05), Chicago, IL, USA, June 2005, pp. 213–223.
[8] K. Sen, D. Marinov, and G. Agha, “CUTE: a concolic unit testing engine for C,” in Proceedings of the 10th European Software Engineering Conference held jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/SIGSOFT FSE’05), Lisbon, Portugal, September 2005, pp. 263–272.
[9] P. Godefroid, M. Y. Levin, and D. A. Molnar, “Automated Whitebox Fuzz Testing,” in Proceedings of the Network and Distributed System Security Symposium (NDSS’08), San Diego, California, USA, February 2008.
[10] D. A. Molnar and D. Wagner, “Catchconv: Symbolic execution and run-time type inference for integer conversion errors,” EECS Department, University of California, Berkeley, Tech. Rep. UCB/EECS-2007-23, February 2007.
[11] N. Nethercote and J. Seward, “Valgrind: a framework for heavyweight dynamic binary instrumentation,” in Proceedings of the ACM SIGPLAN 2007 Conference on Programming Language Design and Implementation (PLDI’07), San Diego, California, USA, June 2007, pp. 89–100.
[12] C. Cadar, D. Dunbar, and D. R. Engler, “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs,” in Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI’08), San Diego, California, USA, December 2008, pp. 209–224.
[13] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill, and D. R. Engler, “EXE: automatically generating inputs of death,” in Proceedings of the 13th ACM Conference on Computer and Communications Security(CCS’06), Alexandria, VA, USA, October - November 2006, pp. 322–335.
[14] C. Lattner and V. S. Adve, “LLVM: A Compilation Framework for Lifelong Program Analysis & Transformation,” in Proceedings of the 2nd IEEE / ACM International Symposium on Code Generation and Optimization (CGO’04), San Jose, CA, USA, March 2004, pp. 75–88.
[15] R. A. Santelices and M. J. Harrold, “Exploiting program dependencies for scalable multiple-path symbolic execution,” in Proceedings of the Nineteenth International Symposium on Software Testing and Analysis (ISSTA’10), Trento, Italy, July 2010, pp. 195–206.
[16] P. Boonstoppel, C. Cadar, and D. R. Engler, “RWset: Attacking Path Explosion in Constraint-Based Test Generation,” in Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), Budapest, Hungary, March - April 2008, pp. 351–366.
[17] M. Delahaye, B. Botella, and A. Gotlieb, “Explanation-Based Generalization of Infeasible Path,” in Proceedings of the Third International Conference on Software Testing, Verification and Validation (ICST’10), Paris, France, April 2010, pp. 215–224.
[18] S. Bardin and P. Herrmann, “Pruning the Search Space in Path-Based Test Generation,” in Proceedings of the Second International Conference on Software Testing Verification and Validation (ICST’09), Denver, Colorado, USA, April 2009, pp. 240–249.
[19] V. Ganesh and D. L. Dill, “A Decision Procedure for Bit-Vectors and Arrays,” in Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07), Berlin, Germany, July 2007, pp. 519–531.
[20] C. Barrett and C. Tinelli, “CVC3,” in Proceedings of the 19th International Conference on Computer Aided Verification (CAV’07), Berlin, Germany, July 2007, pp. 298–302.
[21] B. Dutertre and L. de Moura, “The Yices SMT solver,” Computer Science Laboratory, SRI International, Tech. Rep., August 2006.
[22] L. M. de Moura and N. Bjørner, “Z3: An Efficient SMT Solver,” in Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’08), Budapest, Hungary, March - April 2008, pp. 337–340.
[23] A. Kiezun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst, “HAMPI: a solver for string constraints,” in Proceedings of the Eighteenth International Symposium on Software Testing and Analysis (ISSTA’09), Chicago, IL, USA, July 2009, pp. 105–116.
[24] J. Caballero, P. Poosankam, S. McCamant, D. Babi´c, and D. Song, “Input generation via decomposition and re-stitching: finding bugs in Malware,” in Proceedings of the 17th ACM Conference on Computer and Communications Security (CCS’10), Chicago, Illinois, USA, October 2010, pp. 413–425.
[25] L. Ciortea, C. Zamfir, S. Bucur, V. Chipounov, and G. Candea, “Cloud9: a software testing service,” Operating Systems Review, vol. 43, no. 4, pp. 5–10, 2009.
[26] S. Bucur, V. Ureche, C. Zamfir, and G. Candea, “Parallel symbolic execution for automated real-world software testing,” in Proceedings of the sixth conference on Computer systems (EuroSys ’11), Salzburg, Austria, April 2011, pp. 183–198.
[27] D. Brumley, P. Poosankam, D. X. Song, and J. Zheng, “Automatic Patch-Based Exploit Generation is Possible: Techniques and Implications,” in Proceedings of the 2008 IEEE Symposium on Security and Privacy (S&P 2008), Oakland, California, USA, May 2008, pp. 143–157.
[28] T. Avgerinos, S. K. Cha, B. L. T. Hao, and D. Brumley, “AEG: Automatic Exploit Generation,” in Proceedings of the Network and Distributed System Security Symposium (NDSS’11), San Diego, California, USA, February 2011.
[29] E. J. Schwartz, T. Avgerinos, and D. Brumley, “Q: Exploit Hardening Made Easy,” in Proceedings of the 20th USENIX Security Symposium (USENIX’11), San Francisco, CA, USA, August 2011.
[30] S. Heelan and D. Kroening, “Automatic Generation of Control Flow Hijacking Exploits for Software Vulnerabilities,” MSc Computer Science Dissertation, University of Oxford, UK, 2009.
[31] C. Miller, J. Caballero, N. M. Johnson, M. G. Kang, S. McCamant, P. Poosankam, and D. Song, “Crash Analysis using BitBlaze,” in Proceedings of the Black Hat USA 2010, Las Vegas, US, July 2010.
[32] V. Chipounov, V. Kuznetsov, and G. Candea, “S2E: a platform for in-vivo multi-path analysis of software systems,” in Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS’11), Newport Beach, CA, USA, March 2011, pp. 265–278.
[33] F. Bellard, “QEMU, a fast and portable dynamic translator,” in Proceedings of the FREENIX Track: 2005 USENIX Annual Technical Conference, Anaheim, CA, USA, April 2005, pp. 41–46.
[34] V. Chipounov and G. Candea, “Dynamically Translating x86 to LLVM using QEMU,” School of Computer and Communication Sciences, ´ Ecole Polytechnique F´ed´erale de Lausanne (EPFL), Switzerland, Tech. Rep. EPFL-TR-149975, March 2010.
[35] V. Chipounov, V. Georgescu, C. Zamfir, and G. Candea, “Selective Symbolic Execution,” in Proceedings of the 5th Workshop on Hot Topics in System Dependability (HotDep), Lisbon, Portugal, June 2009.