Inter-procedural buffer overflows detection in C/C++ source code via static analysis
https://doi.org/10.15514/ISPRAS-2016-28(5)-7
Abstract
We propose inter-procedural static analysis tool for buffer overflow detection. It is based on previously developed intra-procedural algorithm which uses symbolic execution with state merging. This algorithm is path-sensitive and supports tracking several kinds of value relations such as arithmetic operations, cast instructions, binary relations from constraints. In this paper we provide a formal definition for inter-procedural buffer overflow errors and discuss different kinds of such errors. We use function summaries for inter-procedural analysis, so it provides natural path-sensitivity in some degree. This approach allowed us to improve intra-procedural algorithm by tracking inter-procedural value dependencies. Furthermore, we introduce a technique to extract the sufficient condition of buffer overflow for a function, which is supposed to be stored in the summary of this function and checked at every call site. This approach was implemented for Svace static analyzer as the new buffer overflow detector, and it has shown 64% true-positive ratio on Android 5.0.2.
About the Author
I. . Dudina
ISP RAS; CMC MSU, CMC faculty, 2 educational building
Russian Federation
Russian Federation
References
1. I. Dudina, V. Koshelev, A. Borodin. [Statically detecting buffer overflows in C/C++]. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 4, 2016, pp. 149-168 (in Russian). DOI: 10.15514/ISPRAS-2016-28(4)-9
2. V. Koshelev, I. Dudina, V. Ignatyev, A. Borzilov. [Path-Sensitive Bug Detection Analysis of C# Program Illustrated by Null Pointer Dereference], Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 5, 2015, pp. 59-86 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-5
3. D. Larochelle, D. Evans. Statically detecting likely buffer overflow vulnerabilities. 10th USENIX Security Symposium, Washington, D.C., August 2001.
4. V.P. Ivannikov, A.A. Belevantsev, A.E. Borodin, V.N. Ignatiev, D.M. Zhurikhin, A.I. Avetisyan, M.I. Leonov. [Static analyzer Svace for finding of defects in program source code]. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 231-250 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7
5. V. Kuznetsov, J. Kinder, S. Bucur, and G. Candea. 2012. Efficient state merging in symbolic execution. SIGPLAN Not. 47, 6 (June 2012), 193-204. DOI: 10.1145/2345156.2254088
6. A. Borodin, A. Belevancev. [A Static Analysis Tool Svace as a Collection of Analyzers with Various Complexity Levels]. Trudy ISP RAN/Proc. ISP RAS, vol. 27, issue 6, pp. 111-134 (in Russian). DOI: 10.15514/ISPRAS-2015-27(6)-8.
7. A. Borodin. PhD thesis. Interprocedural contex-sensitive static analysis for error detection in C/C++ source code. ISP RAN, Moscow, 2016
8. Shahriar, H., and Zulkernine, M. Classification of static analysis-based buffer overflow detectors. SSIRI-C 2010 - 4th IEEE International Conference on Secure Software Integration and Reliability Improvement Companion, 2010, pp. 94-101.
9. Y. Xie, A. Chou, and D. Engler, “ARCHER: Using Symbolic, Path-sensitive Analysis to Detect Memory Access Errors,” Proceedings of the 9th European Software Engineering Conference, Helsinki, Finland, 2003, pp. 327-336.
Review
For citations:
Dudina I. Inter-procedural buffer overflows detection in C/C++ source code via static analysis. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(5):119-134. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(5)-7
Email this article 