Summary-based method of implementing arbitrary context-sensitive checks for source-based analysis via symbolic execution
https://doi.org/10.15514/ISPRAS-2016-28(1)-3
Abstract
A specific approach to summary-based interprocedural symbolic execution is described. The approach is suitable for analysis of program source code developed with high-level programming languages and allows executing arbitrarily complex checks during symbolic execution, including throwing reports in the callee function about defects that only become certain within the caller context. The structure of the function summary, procedure of applying the summary in a particular context, composition of symbolic values for particular contexts, effect of summary-based analysis on complexity of implementing specific checker modules, procedure for constructing path-sensitive bug reports, and other aspects of the implementation are discussed in detail. A particular implementation of the approach, based on Clang Static Analyzer, is described. The implementation is scalable enough to allow analysis of large-scale software projects in reasonable time, finding bugs faster than the existing implementation of the inlining-based interprocedural analysis, without sacrificing correctness and soundness of the analysis. Particular checker modules, which find various defects, such as integer overflows, modifications of constant-qualified memory, multithreading issues, array bound checks, exception safety checks, and file stream errors, were updated to use the summary-based approach, demonstrating flexibility of the technique proposed. The implementation was tested by running full intra-unit inter-procedural analysis of the Android Open Source Project codebase.
About the Authors
A. . Dergachev
Samsung R&D Institute Russia
Russian Federation
Russian Federation
A. . Sidorin
Samsung R&D Institute Russia
Russian Federation
Russian Federation
References
1. David A. Wheeler. How to Prevent the next Heartbleed. 2015. http://www.dwheeler.com/essays/heartbleed.html
2. John Carmack. Static Code Analysis. 2011. http://www.viva64.com/en/a/0087/
3. King James C. Symbolic Execution and Program Testing. Commun. ACM, 19(7), 1976. P. 385-394.
4. Godefroid Patrice, Klarlund Nils, Sen Koushik. DART: Directed Automated Random Testing. Proceedings of the 2005 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI ’05. New York, NY, USA: ACM, 2005. P. 213-223.
5. Saswat Anand, Păsăreanu Corina S, Willem Visser. JPF-SE: A Symbolic Execution Extension to Java Pathfinder. International conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2007.
6. V.P. Ivannikov, A.A. Belevancev, A.E. Borodin et. al. Staticheskij analizator Svace dlja poiska defektov v ishodnom kode program. [Static analyzer Svace for finding defects in a source program code]. Trudy ISP RАN [Proceedings of ISP RAS]. 2014, vol. 26, issue 1, pp. 231-250 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7
7. Matsumoto Hiroo. Applying Clang Static Analyzer to Linux Kernel. 2012 LinuxCon Japan. Yokohama: 2012. 6.
8. Cadar Cristian, Dunbar Daniel, Engler Dawson. KLEE: Unassisted and Automatic Generation of High-coverage Tests for Complex Systems Programs. Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation. OSDI’08. Berkeley, CA, USA: USENIX Association, 2008. P. 209-224.
9. Android Open Source Project. http://source.android.com/
10. Reps Thomas, Horwitz Susan, Sagiv Mooly. Precise Interprocedural Dataflow Analysis via Graph Reachability. Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. POPL ’95. New York, NY, USA: ACM, 1995. P. 49-61.
11. Compilers: Principles, Techniques, and Tools (2nd Edition). A.V. Aho, M.S. Lam, Ravi Sethi, D.D. Ullman. Pearson Education, Inc, 2006.
12. Rojas José Miguel, Păsăreanu Corina S. Compositional Symbolic Execution through Program Specialization. BYTECODE 2013, 8th Workshop on Bytecode Semantics, Verification, Analysis and Transformation, 2013.
13. Godefroid Patrice. Compositional Dynamic Test Generation. SIGPLAN Not. 2007. 42(1). P. 47-54.
14. Summary-based inference of quantitative bounds of live heap objects. Vı́ctor Brabermana, Diego Garbervetskya, Samuel Hymc, Sergio Yovinea Science of Computer Programming, 92, 2013. P. 56-84.
15. Xu Zhenbo, Zhang Jian, Xu Zhongxing. Melton: a practical and precise memory leak detection tool for C programs. Frontiers of Computer Science in China, 9(1), 2015. P. 34-54.
16. Clang Static Analyzer. http://clang-analyzer.llvm.org/
17. Strom, Robert E.; Yemini, Shaula. Typestate: A programming language concept for enhancing software reliability. IEEE Transactions on Software Engineering (IEEE), 12, 1986. P. 157-171.
18. Xu Zhongxing, Kremenek Ted, Zhang Jian. A Memory Model for Static Analysis of C Programs. Proceedings of the 4th International Conference on Leveraging Applications of Formal Methods, Verification, and Validation. Volume Part I. ISoLA’10. Berlin, Heidelberg: Springer-Verlag, 2010. P. 535-548.
Review
For citations:
Dergachev A., Sidorin A. Summary-based method of implementing arbitrary context-sensitive checks for source-based analysis via symbolic execution. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2016;28(1):41-62. (In Russ.) https://doi.org/10.15514/ISPRAS-2016-28(1)-3
Email this article 