臺灣博碩士論文加值系統

軟體測試是軟體開發過程中確保軟體品質最重要的步驟之一，
因在軟體開發的過程中，我們無法保證程式不會發生錯誤。
近年來動靜態程式分析工具的發展已相當成熟，而在 2005 年，更發展出了結合動靜態分析法的導引式隨機測試法。
本論文實作了一個名為 ALERT，結合動靜態分析法的導引式隨機測試平台，
以及其上的軟體未規範實作功能探索模組，以導引式隨機測試方法探索軟體未規範實作功能。
藉由 SAT 模理論 (Satisfiability Modulo Theories) 的定理自動證明函式庫，分析特定的外部輸入所造成的程式流程，
並以控制程式堆疊空間，進一步地操作使用未初始化變數的程式執行結果。
本論文提出兩階段式執行測試方法：第一階段用動態分析工具分析原始程式，取得程式真實的執行資訊。
第二階段使用導引式隨機測試方法，配合第一階段所收集的執行資訊，做分析及推理。
推理所得的結果則為下一輪測試的輸入。
我們不斷重複這兩階段的測式分析，直到找出錯誤或將程式所有執行路徑全數列舉完畢。
我們將此一工具應用於尋找由未初始化變數所造成的程式未規範行為，
成功地萃取出傳統程式分析方法不能找出的軟體行為。
本論文提出的方法改善了現行導引式隨機測試方法中，因修改原始程式碼而造成測試時期和真正執行時期的差距，
提升了測試的精確度。

Testing is one of the most important phases of software quality assurance,
for the process of software construction cannot guarantee the absence of bugs.
Dynamic and static analysis tools are maturely developed in recent years.
In 2005, the concept of concolic (combined word of concrete and symbolic) testing was proposed,
which combines static and dynamic program analysis methods.
In this thesis, we implement ALERT, a concolic testing framework
and an Unspecified Software Feature (USF) Checker based on ALERT.
By using automatic theorem prover library for satisfiability modulo theories,
we can analyze and determine the inputs to direct program's execution along particular paths.
With this mechanism, we can control the values in stack section.
It can also be used to manipulate the values of uninitialized variables
and to trigger specific behavior of the program.
We present a two-phase testing algorithm in this thesis.
In the first phase, we use dynamic analysis tool to retrieve real run-time information.
In the second phase, we analyze the program by using concolic testing method
with the data collected in the first phase.
The result generated by the prover will be the input for the next testing run.
This testing process iterates until a fault is found or all the program execution paths are enumerated.
We use this tool to resolve unspecified program features caused by uninitialized variables.
It successfully extracts the program behavior which cannot be found with traditional program analysis methods.
The method in this thesis resolves the information lost problem caused by source code instrumentation in the
process of testing and improves the accuracy of the test.

摘要 i
Abstract ii
誌謝 iii
Contents iv
List of Figures vi
List of Tables vii
1 Introduction 1
1.1 Background 1
1.1.1 Software Property Checking 1
1.1.2 Software Testing 2
1.1.3 Unspecified Software Features 3
1.2 Problem Description 4
1.3 Motivation 4
1.4 Objective 4
1.4.1 Concept 5
1.5 Simple Example 5
1.6 Thesis Synopsis 7
2 Related work 8
2.1 Static Program Analysis 8
2.1.1 Software Model Checking 8
2.1.2 Abstract Interpretation 11
2.1.3 Assertions and Hoare logic 11
2.2 Dynamic Program Analysis 11
2.3 Concolic Testing 11
2.4 Ad-hoc Techniques 12
2.5 Comparison of Program analysis 12
3 Design and Implementation 14
3.1 ALERT 14
3.1.1 ALERT System Architecture 14
3.1.2 ALERT Execution Logic 17
3.1.3 Program Simplification 17
3.1.4 Symbolic Execution 17
3.1.5 Theorem Prover Library 19
3.2 Unspecified Software Feature (USF) Checker 20
3.2.1 USF Overview 20
3.2.2 USF Execution Logic 21
3.2.3 Symbolic Value Propagation 21
3.2.4 Stack Map 22
3.2.5 Integration with GDB 24
3.2.6 Integration with ALERT 25
4 Experimental Results 27
4.1 Test1: Overlap of Integer Variables 27
4.2 Test2: Two Short Variables Flowing into One Integer Value 30
4.3 Test3: One Integer Variable Flowing into Two Short Variables 33
4.4 Summary 36
5 Conclusion 37
5.1 The Uncertainty Principle 37
5.2 Future Work 37
References 39

[1] GDB: The GNU Project Debugger, http://www.gnu.org/software/gdb/.
[2] Objective Caml, http://caml.inria.fr/ocaml/.
[3] Valgrind, http://valgrind.org/.
[4] IEEE Standard Glossary of Software Engineering Terminology, IEEE std 610.12-1990, 1990.
[5] Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of c programs. In PLDI ’01: Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, pages 203–213, New York, NY, USA, 2001. ACM Press.
[6] Thomas Ball andSriram K. Rajamani. Bebop: A symbolic model checker for boolean programs. In Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, pages 113–130, London, UK, 2000. Springer-Verlag.
[7] Thomas Ball and Sriram K. Rajamani. Generating abstract explanations of spurious counterexamples in C programs. Technical report, Microsoft Research, Redmond, 09 2002.
[8] Thomas Ball and Sriram K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL ’02: Proceedings of the 29th ACM SIGPLAN- SIGACT symposium on Principles of programming languages, pages 1–3, New York, NY, USA, 2002. ACM Press.
[9] Clark Barrett and Sergey Berezin. CVC Lite: A New Implementation of the Cooperating Validity Checker. In Rajeev Alur and Doron A. Peled, editors, Proceedings of the 16th International Conference on Computer Aided Verification (CAV ’04), volume 3114 of Lecture Notes in Computer Science, pages 515–518. Springer-Verlag, July 2004. Boston, Massachusetts.
[10] Cristian Cadar and Dawson R. Engler. Execution generated test cases: How to make systems code crash itself. In Proceedings of the 12th SPIN Workshop on Model Checking Software, San Francisco, USA, 2005.
[11] Cristian Cadar, Vijay Ganesh, Peter M. Pawlowski, David L. Dill, and Dawson R. Engler. EXE: automatically generating inputs of death. In CCS ’06: Proceedings of the 13th ACM conference on Computer and communications security, pages 322–335, New York, NY, USA, 2006. ACM Press.
[12] Edmund M. Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In Computer Aided Verification, pages 154–169, 2000.
[13] David Evans, John Guttag, James Horning, and Yang Meng Tan. LCLint: a tool for using specifications to check code. In SIGSOFT ’94: Proceedings of the 2nd ACM SIGSOFT symposium on Foundations of software engineering, pages 87–96, New York, NY, USA, 1994. ACM Press.
[14] Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, and Raymie Stata. Extended static checking for java. In PLDI ’02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pages 234–245, New York, NY, USA, 2002. ACM Press.
[15] Patrice Godefroid, Nils Klarlund, and Koushik Sen. DART: directed automated random testing. In PLDI ’05: Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pages 213–223, New York, NY, USA, 2005. ACM Press.
[16] Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani. SYNERGY: a new algorithm for property checking. In SIGSOFT’06/FSE-14: Proceedingsof the 14th ACM SIGSOFTinternational symposium on Foundations of software engineering, pages 117–127, New York, NY, USA, 2006. ACM Press.
[17] Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software verification with Blast. In Proceedings of the Tenth International Workshop on Model Checking of Software (SPIN), volume 2648 of Lecture Notes in Computer Science, pages 235–239. Springer-Verlag, 2003.
[18] C. A. R. Hoare. An axiomatic basis for computer programming. Commun. ACM, 12(10):576–580, 1969.
[19] Gerard J. Holzmann. Static source code checking for user-defined properties. In IDPT ’02: Proceedings of The 6th World Conference on Integrated Design & Process Technology, Pasadena, CA, USA, 2002.
[20] Stephen Johnson. Lint, a C Program Checker. Technical Report 65, Bell Laboratories, 1978.
[21] David Larochelle and David Evans. Statically detecting likely buffer overflow vulnerabilities. In SSYM’01: Proceedings of the 10th conference on USENIX Security Symposium, pages 14–14, Berkeley, CA, USA, 2001. USENIX Association.
[22] Flavio Lerda and Willem Visser. Addressing dynamic issues of program model checking. In SPIN ’01: Proceedings of the 8th international SPIN workshop on Model checking of software, pages 80�釉102, New York, NY, USA, 2001. Springer-Verlag New York, Inc.
[23] Metasploit LLC. The Metasploit Project: An Equal Opportunity Exploiter, http://www.metasploit.com/.
[24] George C. Necula, Scott McPeak, Shree Prakash Rahul, and Westley Weimer. CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In CC ’02: Proceedings of the 11th International Conference on Compiler Construction, pages 213�釉228, London, UK, 2002. Springer-Verlag.
[25] Koushik Sen, Darko Marinov, and Gul 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, pages 263�釉272, New York, NY, USA, 2005. ACM Press.
[26] Julian Seward and Nicholas Nethercote. Using Valgrind to detect undefined value errors with bit-precision. In ATEC�嗷�05: Proceedings of the USENIX Annual Technical Conference 2005 on USENIX Annual Technical Conference, pages 2�釉2, Berkeley, CA, USA, 2005. USENIX Association.
[27] Aaron Stump, Clark W. Barrett, and David L. Dill. CVC: A Cooperating Validity Checker. In Ed Brinksma and Kim Guldstrand Larsen, editors, Proceedings of the 14th International Conference on Computer Aided Verification (CAV ’02), volume 2404 of Lecture Notes in Computer Science, pages 500�釉504. Springer-Verlag, July 2002. Copenhagen, Denmark.
[28] Willem Visser, KlausHavelund, Guillaume Brat, andSeungJoon Park. Model Checking Programs. In ASE ’00: Proceedings of the 15th IEEE international conference on Automated software engineering, page 3, Washington, DC, USA, 2000. IEEE Computer Society.