Skip to main content
SpringerLink
Log in

Multi-level Static Analysis for Finding Error Patterns and Defects in Source Code

  • Conference paper
  • First Online:
Perspectives of System Informatics (PSI 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10742))

Abstract

This paper presents the formalism for multiple level static analysis for defect detection in source code. The first level has the program and memory model that are suitable for AST-level checks. The following levels address detection of critical errors: on the second level interprocedural partially context-sensitive analysis is performed via dataflow analysis and symbolic execution with state merging, whereas the third level adds path-sensitivity via predicate tracking for the dataflow information computed on the second. The analysis designer can freely choose the appropriate analysis level or their combination to check the desired program property. The presented methods are implemented in the Svace static analysis toolset. The first analysis levels for C/C++ and Java are implemented as extensions of corresponding production compilers (Clang and javac) and FindBugs tool plugins, while the second and third levels make the core of Svace analyzer together with 100+ implemented checkers for critical defects. The evaluation on extra large codebases of millions lines of code such as full-blown Android and Tizen OSes has shown the approach scalability and the acceptable false positives ratio (less than 40%).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Checkers that are more concerned with memory properties (like memory leaks) get benefit from attaching attributes directly to memory locations instead of value classes [8], but we do not discuss it in more details in this paper.

  2. 2.

    In case we have nontrivial VC for glob variable, we can further improve the precision if e.g. the conditional operator will never be executed and we don’t have to consider the instruction at line 5.

  3. 3.

    We do not use the CSA path-sensitive infrastructure, as its scope is limited by the compilation unit, but move the heavy checkers to our own analyzer engine.

  4. 4.

    One example is the Android app fast analysis that takes into account the calculated analysis data for the full Android OS.

  5. 5.

    The predicate representation has to be regularly reviewed as the path-sensitive analysis portion in the analyzer grows over time.

References

  1. Cousot, P., Cousot, R., Feret, J., et al.: Why does Astrée scale up? Form Methods Syst. Des. 35, 229 (2009). https://doi.org/10.1007/s10703-009-0089-6

    Article  MATH  Google Scholar 

  2. Xie, Y., Aiken, A.: Saturn: a scalable framework for error detection using Boolean satisfiability. ACM Trans. Program. Lang. Syst. 29(3), 1–43 (2007). Article 16

    Article  Google Scholar 

  3. Sankaranarayanan, S., Ivančić, F., Gupta, A.: Program analysis using symbolic ranges. In: Nielson, H.R., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 366–383. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74061-2_23

    Chapter  Google Scholar 

  4. Xu, Z., Kremenek, T., Zhang, J.: A memory model for static analysis of C programs. In: Margaria, T., Steffen, B. (eds.) ISoLA 2010, Part I. LNCS, vol. 6415, pp. 535–548. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16558-0_44

    Chapter  Google Scholar 

  5. Ignatiev, V.: Using static analysis for customizable checks of C/C++ semantic constraints. Ph.D. thesis, Moscow (2015)

    Google Scholar 

  6. Strein, D., Kratz, H., Lowe, W.: Cross-language program analysis and refactoring. In: Proceedings of the Sixth IEEE International Workshop on Source Code Analysis and Manipulation (SCAM 2006), Washington, DC, USA, pp. 207–216. IEEE Computer Society (2006)

    Google Scholar 

  7. Zubov, M.V., Pustygin, A.N., Startsev, E.V.: Use of the intermediate software representations for static analysis of source code. Doklady TUSUR 27, 64–68 (2013). (in Russian)

    Google Scholar 

  8. Borodin, A.: Interprocedural context-sensitive static analysis for finding defects in C/C++ program source code. Ph.D. thesis, Moscow (2016)

    Google Scholar 

  9. LLVM Language Reference Manual. http://llvm.org/docs/LangRef.html

  10. Tucker Taft. The use of value numbers in static analysis. http://www.adacore.com/knowledge/technical-papers/the-use-of-value-numbers-in-static-analysis/

  11. MISRA C 2012 Guidelines. https://www.misra.org.uk/MISRAHome/MISRAC2012/tabid/196/Default.aspx

  12. CERT C Coding Standard. https://www.securecoding.cert.org/confluence/display/c/SEI+CERT+C+Coding+Standard

  13. CWE, Common Weakness Enumeration Database. https://cwe.mitre.org/

  14. Briggs, P., Cooper, K.D., Taylor Simpson, L.: Value numbering. Softw. Pract. Exper. 27(6), 701–724 (1997). https://doi.org/10.1002/zaac.201500219

    Article  Google Scholar 

  15. Borodin, A., Belevantsev, A.: A static analysis tool Svace as a collection of analyzers with various complexity levels. Trudy ISP RAN/Proc. ISP RAS 27(6), 111–134 (2015). (in Russian)

    Article  Google Scholar 

  16. Ivannikov, V.P., Belevantsev, A.A., Borodin, A.E., Ignat’ev, V.N., Zhurikhin, D.M., Avetisjan, A.I., Leonov, M.I.: Staticheskij analizator Svace dlja poiska defektov v iskhodnom kode programm [Svace: static analyzer for detecting of defects in program source code]. Trudy ISP RAN [The Proceedings of ISP RAS] 26(1), 231–250 (2011). https://doi.org/10.15514/ispras-2014-26(1)-7. (in Russian)

    Article  Google Scholar 

  17. Avetisjan, A.I., Belevantsev, A.A., Borodin, A.E., Nesov, V.S.: Ispol’zovanie staticheskogo analiza dlja poiska ujazvimostej i kriticheskikh oshibok v iskhodnom kode program [Using static analysis for searching vulnerabilities and critical errors in the source code of programs]. Trudy ISP RAN [The Proceedings of ISP RAS] 21, 23–38 (2011). (in Russian)

    Google Scholar 

  18. Koshelev, V.K., Ignatyev, V.N., Borzilov, A.I.: C# static analysis framework. Trudy ISP RAN/Proc. ISP RAS 28(1), 21–40 (2016). (in Russian)

    Article  Google Scholar 

  19. FindBugs tool. http://findbugs.sourceforge.net/

  20. Clang Static Analyzer. http://clang-analyzer.llvm.org/

  21. Z3 Theorem Prover. https://github.com/Z3Prover/z3

  22. Svace tool deployed in Samsung. Vedomosti news. http://www.vedomosti.ru/technology/articles/2016/11/17/665253-russkie-programmisti-samsung

  23. Dudina, I.: Inter-procedural buffer overflows detection in C/C++ source code via static analysis. Trudy ISP RAN/Proc. ISP RAS 28(5), 119–134 (2016). https://doi.org/10.15514/ispras-2016-28(5)-7. (in Russian)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute for System Programming of the Russian Academy of Sciences, Moscow, Russia

    Andrey Belevantsev & Arutyun Avetisyan

  2. Moscow State University, Moscow, Russia

    Andrey Belevantsev & Arutyun Avetisyan

  3. Moscow Institute of Physics and Technology (National University), Moscow, Russia

    Arutyun Avetisyan

  4. National Research University Higher School of Economics, Moscow, Russia

    Arutyun Avetisyan

Authors
  1. Andrey Belevantsev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arutyun Avetisyan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrey Belevantsev .

Editor information

Editors and Affiliations

  1. Ivannikov Institute for System Programming of RAS, Moscow, Russia

    Alexander K. Petrenko

  2. The University of Manchester, Manchester, United Kingdom

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Belevantsev, A., Avetisyan, A. (2018). Multi-level Static Analysis for Finding Error Patterns and Defects in Source Code. In: Petrenko, A., Voronkov, A. (eds) Perspectives of System Informatics. PSI 2017. Lecture Notes in Computer Science(), vol 10742. Springer, Cham. https://doi.org/10.1007/978-3-319-74313-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-74313-4_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-74312-7

  • Online ISBN: 978-3-319-74313-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation