Symbolic Execution Based Intra-Procedural Analysis for Search for Defects
https://doi.org/10.15514/ISPRAS-2020-32(6)-7
Abstract
Svace is a static analysis tool for bug detection in C/C++/Java source code. To analyze a program, Svace performs an intra-procedure analysis of individual functions, starting from the leaves of a call-graph and moving towards the roots, and uses summaries of previously analyzed procedures at call-cites. In this paper, we overview the approaches and techniques employed by Svace for the intra-procedural analysis. This phase is performed by an analyzer engine and an extensible set of detectors. The core engine employs a symbolic execution approach with state merging. It uses value numbering to reduce the set of symbolic expressions, maintains points-to relationship graph for memory modeling, and performs strong and weak updates of program values. Detectors are responsible for discovering and reporting bugs. They calculate different properties of program values using a variety of abstract domains. All detectors work simultaneously orchestrated by the engine. Svace analysis is unsound and employs a variety of heuristics to speed-up. We designed Svace to analyze big projects (several MLOCs) in just a few hours and report as many warnings as possible, while keeping a good quality of reports ≥ 65 of true positives). For example, Tizen 5.5 (20MLOC) analysis takes 8.6 hours and produces 18,920 warnings, more than 70% of which are true-positive.
About the Authors
Alexey Evgenevich BORODIN
Ivannikov Institute for System Programming of the RAS
Russian Federation
PhD, researcher
Russian Federation
PhD, researcher
Irina Aleksandrovna DUDINA
1Ivannikov Institute for System Programming of the RAS, Lomonosov Moscow State University
Russian Federation
PhD, employee of ISP RAS and assistant of the Department of System Programming of the Faculty of CMC
Russian Federation
PhD, employee of ISP RAS and assistant of the Department of System Programming of the Faculty of CMC
References
1. В.П. Иванников, А.А. Белеванцев, А.Е. Бородин, В.Н. Игнатьев, Д.М. Журихин, А.И. Аветисян, М.И. Леонов. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды ИСП РАН, том 26, вып. 1, 2014 г., стр. 231-250 / V.P. Ivannikov, A.A. Belevantsev, A.E. Borodin, V.N. Ignatyev, D.M. Zhurikhin, A.I. Avetisyan, M.I. Leonov. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 231-250 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7.
2. A. Borodin, A. Belevantsev, D. Zhurikhin, and A. Izbyshev. Deterministic static analysis. In Proc. of the 2018 Ivannikov Memorial Workshop, 2018, pp. 10-14. DOI: 10.1109/IVMEM.2018.00009.
3. Clang. URL: https://clang.llvm.org, accessed September 10, 2020.
4. The javac compiler. URL: https: //docs.oracle.com/en/java/javase/11/tools/javac.html, accessed September 10, 2020.
5. LLVM bitcode. URL: https: //releases.llvm.org/8.0.1/docs/BitCodeFormat.html, accessed September 10, 2020.
6. J. C. King. Symbolic execution and program testing. Communications of the ACM, vol. 19, no. 7, 1976, pp. 385-394.
7. А.Е. Бородин и А.А. Белеванцев. Статический анализатор Svace как коллекция анализаторов разных уровней сложности. Труды ИСП РАН, том 27, вып. 2, 2015 г., стр. 111-134 / A.E. Borodin, A.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, 2015, pp.111-134 (in Russian). DOI: 10.15514/ISPRAS-2015-27(6)-8.
8. Р.Р. Мулюков, А.Е. Бородин. Использование анализа недостижимого кода в статическом анализаторе для поиска ошибок в исходном коде программ. Труды ИСП РАН, том 28, вып. 5, 2016 г., стр. 145-158 / R.R. Mulyukov, A.E. Borodin. Using unreachable code analysis in static analysis tool for finding defects in source code. Trudy ISP RAN/Proc. ISP RAS, 2016, vol. 28, issue 5, 2016, pp. 145-158 (in Russian). DOI: 10.15514/ISPRAS-2016-28(5)-9.
9. W.R. Bush, J.D. Pincus, and D.J. Sielaff. A static analyzer for finding dynamic programming errors. Software-Practice and Experience, vol. 30, no. 7, 2000, pp. 775-802.
10. Y. Xie, A. Chou, and D. Engler. Archer: using symbolic, path-sensitive analysis to detect memory access errors. ACM SIGSOFT Software Engineering Notes, vol. 28, no. 5, 2003, pp. 327–336.
11. A. Bessey, K. Block, B. Chelf, A. Chou, B. Fulton, S. Hallem, C. Henri-Gros, A. Kamsky, S. McPeak, and D. Engler. A few billion lines of code later: using static analysis to find bugs in the real world. Communications of the ACM, vol. 53, no. 2, 2010, pp. 66–75.
12. A. Aiken, S. Bugrara, I. Dillig, T. Dillig, B. Hackett, and P. Hawkins. An overview of the saturn project. In Proc of the 7th ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, 2007, pp. 43–48. ACM.
13. D. Babic and A.J. Hu. Calysto: scalable and precise extended static checking. In Proc. of the 30th International Conference on Software Engineering, 2008, pp. 211–220.
14. В.К. Кошелев, И.А. Дудина, В.Н. Игнатьев, А.И. Борзилов. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды ИСП РАН, том 27, вып. 5, 2015 г., стр. 59-86 / V.K. Koshelev, I.A. Dudina, V.N. Ignatyev, A.I. 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.
15. V. Koshelev, V. Ignatiev, A. Borzilov, and A. Belevantsev. Sharpchecker: static analysis tool for C# programs. Programming and Computer Software, vol. 43, no. 4, 2017, pp. 268–276. DOI: 10.1134/S0361768817040041.
Review
For citations:
BORODIN A.E., DUDINA I.A. Symbolic Execution Based Intra-Procedural Analysis for Search for Defects. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(6):87-100. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(6)-7
Email this article 