每天都有新弱點被發佈，其中有些惡名昭彰的弱點是多數程式員所熟悉的，例如，錯誤使用未限制的複製函數、或接受格式字串的函數。近幾年來，一種稱為整數錯誤的新型態程式弱點被發掘，許多重要的應用程式都有這樣的程式弱點，例如Microsoft Internet Explorer 以及 PHP等系統。這種弱點是由於整數溢位後，被運用於配置記憶體。因為整數溢位，配置的記憶體將少於所預期的數量，因而也造成記憶體溢位問題。正負整數轉換是所有整數問題的一部分，我們將在論文中探討、偵測此類問題的方法。

在論文中，我們提出一種偵測技術，以檢驗正負整數轉換相關運算，找出Ｃ程式可能的錯誤。此方法是基於程式控制流、與實際/符號混合測試技術(Concolic testing)。當測試到潛在問題時，我們使用總體特性檢查 (Universal Property Checking)，更進一步驗證常見、且已知軟體的弱點，判斷是否會引發正負整數轉換問題。

我們提出的方法，已在linux2.6.17平台上評估，對幾個有代表性的程式類型進行測試。這些類型分別為：(1)正號整數轉負號整數、(2)負號整數轉正號整數、(3)以及語意錯誤。對於真實案例評估，我們也偵測到qemu 0.8.2中的程式錯誤。

New vulnerabilities in software come out every day. Some of them are so infamous that most programmers are familiar with, e.g. misuse of unbounded copy functions or format string functions. A new type of vulnerability, called integer errors, emerges in recent years. Many major applications suffer from this kind of vulnerability, for example, Microsoft Internet Explorer and PHP. The vulnerability is caused by integer overflow and the integer is then used as size field to allocate heap memory. Because of the integer overflow, the allocated heap space is far less than what the programmers expect, thereby causing heap overflow then.

We have developed a technique that aims at finding integer signedness bugs in C programs. This technique is based on CONCOLIC-testing (CONCrete and symbOLIC) and control-path analysis. The control path analysis of the target program will help us identify the program input data which cause a suspicious integer conversion. This suspicious integer conversion may turn to integer signedness bugs by some rare input data. Then we use concolic testing and universal checking to verify whether there is a feasible bug that will be caused by this suspicious integer conversion.

The proposed method, called reflter algorithm, has been evaluated in Linux 2.6.17 with several representative program examples, including signed-to-unsigned and unsigned-to-signed conversions, along with semantic bugs. This method also detects a real bug in qemu 0.8.2.

1 Introduction 1
1.1 Numbers in Computer Science and integer error 1
1.2 Integer Conversion 3
1.3 Potentially Dangerous Integer Conversion 4
1.4 Signedness Problems 6
1.5 Input Validation 8
1.6 Our Approach 8
2 Software Verification, Testing Coverage and Concolic Testing 10
2.1 Dynamic verification 10
2.2 Test generation 10
2.3 Manually-generated and automatically generated test 11
2.4 Static verification 12
2.5 Concolic testing 12
2.6 ALERT 13
3 Algorithm 14
3.1 Refilter Algorithm 14
3.2 The Second Phase 15
3.3 Contribution 21
4 Implementation 22
4.1 ALERT Implementation 22
4.2 Refilter Algorithm Implementation 30
5 Evaluation 32
5.1 Signed-to-unsigned Conversion 32
5.2 testing of TestAntiSniff 34
5.3 Comparison of Calls to Universal Checker 37
5.4 Testing Detail of AntiSniff 38
6 Discussions 42
6.1 False Positive 42
6.2 False Negative 42
7 Related Works 43
8 Conclusions 45
9 References 46
Appendix A: Source Code of Modified AntiSniff 48

[1] J. Koziol, D. Litchfield and D. A. and, The Shellcoder's Handbook : Discovering and 　　　　　　　　　　Exploiting Security Holes. John Wiley Sons, 2004.
[2] SecurityTracker, "Microsoft Internet Explorer Integer Overflow in Processing Bitmap Files Lets Remote Users Execute Arbitrary Code," feb. 2004.
[3] SecurityTracker, "PHP emalloc() Integer Overflow May Let Remote Users Execute Arbitrary Code," apr. 2004.
[4] D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala and R. Majumdar, "The blast query language for software verification," in SAS, 2004, pp. 2-18.
[5] B. S. Gulavani, T. A. Henzinger, Y. Kannan, A. V. Nori and S. K. Rajamani, "SYNERGY: A new algorithm for property checking," in SIGSOFT '06/FSE-14: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2006, pp. 117-127.
[6] 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.
[7] J. C. King, "Symbolic execution and program testing," Commun ACM, vol. 19, pp. 385-394, 1976.
[8] 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.
[9] lp_solve. web page: http://tech.groups.yahoo.com/group/lp_solve/.
[10] C. Barrett and S. Berezin, "CVC lite: A new implementation of the cooperating validity checker," in Proceedings of the 16Th International Conference on Computer Aided Verification (CAV '04); Lecture Notes in Computer Science, 2004, pp. 515-518.
[11] V. Ganesh and D. L. Dill, "A decision procedure for bit-vectors and arrays," in Computer Aided Verification (CAV '07), 2007,
[12] D. Brumley, T. Chiueh and R. J. and, "Efficient and accurate detection of integer-based attacks," in Proceedings of the Annual Network and, 2007,
[13] G. C. Necula, S. McPeak, S. P. Rahul and W. 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, 2002, pp. 213-228.
[14] D. Molnar and D. Wagner, "Catchconv: Symbolic execution and run-time type inference for integer conversion errors," feb 2007.
[15] N. Nethercote and J. Seward, "Valgrind: A framework for heavyweight dynamic binary instrumentation," in PLDI '07: Proceedings of the 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation, 2007, pp. 89-100.
[16] O. Horovitz, "Big loop integer protection," Phrack, dec. 2002.
[17] S. Ranise and C. Tinelli, "The Satisfiability Modulo Theories Library (SMT-LIB)," 2006.
[18] B. Dutertre and L. d. Moura, "A fast linear-arithmetic solver for DPLL(T)," in Proceedings of the 18th Computer-Aided Verification Conference; LNCS, 2006, pp. 81-94.
[19] R. E. Bryant, S. K. Lahiri and S. A. Seshia, "Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions," in Computer Aided Verification; Lecture Notes in Computer Science, 2002, pp. 78-92.
[20] T. Ball and S. K. Rajamani, "Automatically validating temporal safety properties of interfaces," in SPIN '01: Proceedings of the 8th International SPIN Workshop on Model Checking of Software, 2001, pp. 103-122.
[21] M. Vuagnoux, "AUTODAFE an Act of Software Torture," 2005.
[22] P. Godefroid, M. Levin and D. Molnar, "Automated Whitebox Fuzz Testing," 2007.
[23] D. Wagner, J. S. Foster, E. A. Brewer and A. Aiken, "A first step towards automated detection of buffer overrun vulnerabilities," in NDSS, 2000,
[24] C. Cadar, V. Ganesh, P. M. Pawlowski, D. L. Dill and D. R. Engler, "EXE: Automatically generating inputs of death." in ACM Conference on Computer and Communications Security, 2006, pp. 322-335