Proceedings of the Institute for System Programming of the RAS
RUS  ENG    JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB  
General information
Latest issue
Archive

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Proceedings of ISP RAS:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Proceedings of the Institute for System Programming of the RAS, 2016, Volume 28, Issue 1, Pages 41–62
DOI: https://doi.org/10.15514/ISPRAS-2016-28(1)-3
(Mi tisp3)
 

Summary-based method of implementing arbitrary context-sensitive checks for source-based analysis via symbolic execution

A. Dergachev, A. Sidorin

Samsung R&D Institute Russia, Dvintsev 12, 127018 Moscow, Russia
References:
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.
Keywords: C, C++, Clang Static Analyzer, static analysis, symbolic execution, interprocedural analysis, context-sensitive analysis, summary-based analysis.
Bibliographic databases:
Document Type: Article
Language: Russian
Citation: A. Dergachev, A. Sidorin, “Summary-based method of implementing arbitrary context-sensitive checks for source-based analysis via symbolic execution”, Proceedings of ISP RAS, 28:1 (2016), 41–62
Citation in format AMSBIB
\Bibitem{DerSid16}
\by A.~Dergachev, A.~Sidorin
\paper Summary-based method of implementing arbitrary context-sensitive checks for source-based analysis via symbolic execution
\jour Proceedings of ISP RAS
\yr 2016
\vol 28
\issue 1
\pages 41--62
\mathnet{http://mi.mathnet.ru/tisp3}
\crossref{https://doi.org/10.15514/ISPRAS-2016-28(1)-3}
\elib{https://elibrary.ru/item.asp?id=26166304}
Linking options:
  • https://www.mathnet.ru/eng/tisp3
  • https://www.mathnet.ru/eng/tisp/v28/i1/p41
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Proceedings of the Institute for System Programming of the RAS
     
      Contact us:
     Terms of Use  Registration to the website  Logotypes © Steklov Mathematical Institute RAS, 2024