Основанный на резюме метод реализации произвольных контекстно-чувствительных проверок при анализе исходного кода посредством символьного выполнения
Автор: Дергачв А.В., Сидорин А.В.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 1 т.28, 2016 года.
Бесплатный доступ
Описывается методика, позволяющая реализовать поиск дефектов достаточно общего и произвольного вида при использовании межпроцедурного анализа методом резюме при анализе исходного кода программы на высокоуровневых языках программирования, таких как C и C++. Основное внимание уделено трудностям, возникающим при построении и применении резюме в процессе анализа исходного кода (по сравнению с анализом низкоуровневого представления программы), а также достижению гибкости метода анализа, необходимой для поиска дефектов произвольного вида.
Статический анализ, символьное выполнение, межпроцедурный анализ, контекстно-чувствительный анализ, резюме
Короткий адрес: https://sciup.org/14916328
IDR: 14916328 | DOI: 10.15514/ISPRAS-2016-28(1)-3
Список литературы Основанный на резюме метод реализации произвольных контекстно-чувствительных проверок при анализе исходного кода посредством символьного выполнения
- David A. Wheeler. How to Prevent the next Heartbleed. 2015. http://www.dwheeler.com/essays/heartbleed.html
- John Carmack. Static Code Analysis. 2011. http://www.viva64.com/en/a/0087/
- King James C. Symbolic Execution and Program Testing. Commun. ACM, 19(7), 1976. P. 385-394.
- 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.
- 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.
- V.P. Ivannikov, A.A. Belevancev, A.E. Borodin et. al. Staticheskij analizator Svace dlja poiska defektov v ishodnom kode program. Trudy ISP RАN 2014, vol. 26, issue 1, pp. 231-250 DOI: 10.15514/ISPRAS-2014-26(1)-7
- Matsumoto Hiroo. Applying Clang Static Analyzer to Linux Kernel. 2012 LinuxCon Japan. Yokohama: 2012. 6.
- 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.
- Android Open Source Project. http://source.android.com/
- 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.
- Compilers: Principles, Techniques, and Tools (2nd Edition). A.V. Aho, M.S. Lam, Ravi Sethi, D.D. Ullman. Pearson Education, Inc, 2006.
- 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.
- Godefroid Patrice. Compositional Dynamic Test Generation. SIGPLAN Not. 2007. 42(1). P. 47-54.
- 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.
- 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.
- Clang Static Analyzer. http://clang-analyzer.llvm.org/
- 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.
- 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.
