為了增強軟體的強健度，找出軟體的錯誤行為一直是軟體工程領域裡面一個相當重要的課題。在過去已有許多這方面的研究使用靜態或動態程式分析的技術。然而，有時靜態分析回報的錯誤不一定在執行時期會發生，而動態分析通常無法找出全部潛在的錯誤。在本論文中，我們實做一個測試平台，此平台在執行被測程式的過程中，可以同時蒐集目前執行路徑上的條件限制，然後利用這些條件限制來自動地產生測試資料，以覆蓋不同的執行路徑。由於我們的測試平台可以自動地產生高覆蓋率的測試資料，因此我們的方法理論上可以找出全部潛在的錯誤。另一方面，因為我們有實際執行被測程式，所以回報的錯誤都是在執行時期真實會發生的。在本論文中，我們使用此平台來檢測一個由靜態分析工具回報的程式狀態所隱含的臭蟲，是否可能在執行時期發生。此平台會自動地嘗試產生一組測試資料來觸發目標的程式狀態，或是回報目標的程式狀態不可能在執行時期觸發。

Locating software bugs is an important topic in software engineering for enhancing software robustness. Research topics in these areas with static analysis or dynamic analysis have been proposed. However, the diagnosis of static analysis usually has false positive, and dynamic analysis usually has false negative. We implement a testing framework which runs a tested program and collects symbolic constraints along its execution path. It can automatically generate test cases to cover different execution paths. In theory the diagnosis of our testing framework has no false negative because it can automatically produce test cases with high coverage. On the other hands, the diagnosis of our testing framework has no false positive because we concretely run the tested program. In this thesis, we use this tool to check whether or not a program state with potential bug reported by a static analysis tool is feasible in run time. The tool automatically tries to find a test case which can trigger the target program state, or report the target program state is infeasible.

1. Introduction 1
1.1 Motivation 1
1.2 Objective 2
1.3 Example 2
2. Related Work 5
2.1 Static Analysis 5
2.2 Dynamic Analysis 5
2.3 Concolic Execution 6
2.4 Model Checking 6
3. Concolic Execution Implementation 8
3.1 Testing Framework Overview 8
3.2 Preprocessing 11
3.3 Symbolic Execution 14
3.4 Combination of symbolic execution and concrete run 16
4. Target Directed Random Testing 30
4.1 Incomplete Target Execution Path 30
4.2 Path Searching Algorithm 31
5. Experimental Results 37
6. Conclusions 42
References 42

[1] A. Gotlieb and M. Petit, "Path-oriented random testing," in RT '06: Proceedings of the 1st International Workshop on Random Testing, 2006, pp. 28-35.
[2] P. Godefroid, N. Klarlund and K. Sen, "DART: Directed automated random testing," in PLDI '05: Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2005, pp. 213-223.
[3] K. Sen, D. Marinov and G. Agha, "CUTE: A concolic unit testing engine for C," in ESEC/FSE-13: Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005, pp. 263-272.
[4] C. Cadar and D. Engler, "Execution Generated Test Cases," 2005.
[5] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill and D. R. Engler, "EXE: Automatically generating inputs of death," in CCS '06: Proceedings of the 13th ACM Conference on Computer and Communications Security, 2006, pp. 322-335.
[6] J. Yang, C. Sar, P. Twohey, C. Cadar and D. Engler, "Automatically generating malicious disks using symbolic execution," in SP '06: Proceedings of the 2006 IEEE Symposium on Security and Privacy (S\&P'06), 2006, pp. 243-257.
[7] J. S. Foster, T. Terauchi and A. Aiken, "Flow-sensitive type qualifiers," in PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002, pp. 1-12.
[8] C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe and R. Stata, "Extended static checking for java," in PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, 2002, pp. 234-245.
[9] E. Haugh and M. Bishop, "Testing C Programs for Buffer Overflow Vulnerabilities," 2003
[10] D. Avots, M. Dalton, V. B. Livshits and M. S. Lam, "Improving software security with a C pointer analysis," in ICSE '05: Proceedings of the 27th International Conference on Software Engineering, 2005, pp. 332-341.
[11] E. Clarke, O. Grumberg, S. Jha, Y. Lu and H. Veith, "Counterexample-guided abstraction refinement for symbolic model checking," J. ACM, vol. 50, pp. 752-794, 2003.
[12] D. Beyer, A. J. Chlipala and R. Majumdar, "Generating tests from counterexamples," in ICSE '04: Proceedings of the 26th International Conference on Software Engineering, 2004, pp. 326-335.
[13] E. Clarke, "SATABS: SAT-based predicate abstraction for ANSI-C," in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005); Lecture Notes in Computer Science, 2005, pp. 570-574.
[14] E. Clarke, "A tool for checking ANSI-C programs," in Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2004); Lecture Notes in Computer Science, 2004, pp. 168-176.
[15] G. C. Necula, S. McPeak, S. P. Rahul and W. Weimer, "CIL: Intermediate language and tools for analysis and transformation of C programs," in Computational Complexity, 2002, pp. 213-228.
[16] C. Barrett and S. Berezin, "CVC lite: A new implementation of the cooperating validity checker," in Proceedings of the International Conference on Computer Aided Verification (CAV '04); Lecture Notes in Computer Science, 2004, pp. 515-518.
[17] “Antiword: a free MS word document reader” http://www.winfield.demon.nl/