Основанный на резюме метод реализации произвольных контекстно-чувствительных проверок при анализе исходного кода посредством символьного выполнения
https://doi.org/10.15514/ISPRAS-2016-28(1)-3
Аннотация
Описывается методика, позволяющая реализовать поиск дефектов достаточно общего и произвольного вида при использовании межпроцедурного анализа методом резюме при анализе исходного кода программы на высокоуровневых языках программирования, таких как C и C++. Основное внимание уделено трудностям, возникающим при построении и применении резюме в процессе анализа исходного кода (по сравнению с анализом низкоуровневого представления программы), а также достижению гибкости метода анализа, необходимой для поиска дефектов произвольного вида.
Об авторах
А. В. Дергачёв
Исследовательский центр Samsung
Россия
Россия
А. В. Сидорин
Исследовательский центр Samsung
Россия
Россия
Список литературы
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. В.П. Иванников, А.А. Белеванцев, А.Е. Бородин и др. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды Института системного программирования РАН. 2014, 26 (1). С. 231–250.
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. Компиляторы. Принципы, технологии и инструментарий. А.В. Ахо, М.С. Лам, Рави Сети, Д.Д. Ульман. Вильямс, 2003. — 1184 с.
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
16. leak detection tool for C programs. Frontiers of Computer Science in China, 9(1), 2015. P. 34–54.
17. Clang Static Analyzer. http://clang-analyzer.llvm.org/
18. 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.
19. 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.
Рецензия
Для цитирования:
Дергачёв А.В., Сидорин А.В. Основанный на резюме метод реализации произвольных контекстно-чувствительных проверок при анализе исходного кода посредством символьного выполнения. Труды Института системного программирования РАН. 2016;28(1):41-62. https://doi.org/10.15514/ISPRAS-2016-28(1)-3
For citation:
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
Послать статью по эл. почте 