Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя
https://doi.org/10.15514/ISPRAS-2015-27(5)-5
Аннотация
В данной работе рассматривается вопрос построения масштабируемого чувствительного к путям анализа дефектов в программах на языке C#. Производится формализация дефекта разыменования нулевого указателя и сведение задачи поиска данного дефекта к задаче выполнимости формул логики предикатов. Приведены результаты анализатора, основанного на данном методе, подтверждающие его применимость для анализа промышленных программ.
Об авторах
В. К. Кошелев
ИСП РАН
Россия
Россия
И. А. Дудина
ИСП РАН
Россия
Россия
В. И. Игнатьев
ИСП РАН
Россия
Россия
А. И. Борзилов
ИСП РАН
Россия
Россия
Список литературы
1. P. Tu, D. Padua. Efficient Building and Placing of Gating Functions, SIGPLAN Not. 1995. Vol. 30, no. 6. pp. 47-55. doi: 10.1145/223428.207115
2. B. Clark, F. Pascal, T. Cesare. The SMT-LIB Standard: Version 2.5. Department of Computer Science, The University of Iowa, 2015. www.SMT-LIB.org.
3. В.П. Иванников А.А. Белеванцев А.Е. Бородин В.Н. Игнатьев Д.М. Журихин А.И. Аветисян М.И. Леонов. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды Института системного программирования РАН. 2014. Том. 26, выпуск 1. pp. 231-250. DOI: 10.15514/ISPRAS-2014-26(1)-7
4. G. Ramalingam. The Undecidability of Aliasing. ACM Trans. Program. Lang. Syst. 1994. Vol. 16, no. 5. pp. 1467-1471. doi: 10.1145/186025.186041
5. E. Clarke, D. Kroening. Hardware Verification using ANSI-C Programs as a Reference. Proceedings of ASP-DAC. 2003, pp. 308-311.
6. Falke Stephan, Merz Florian, Sinz Carsten. LLBMC: Improved Bounded Model Checking of C Programs Using LLVM. Tools and Algorithms for the Construction and Analysis of Systems. pp. 623-626. doi: 10.1007/978-3-642-36742-7_48
7. Babic D., Hu A.J. Calysto. Software Engineering, 2008. ICSE ’08. ACM/IEEE 30th International Conference on. 2008. May. pp. 211-220.
8. E. Clarke, O. Grumberg, S. Jha at al. Counterexample-Guided Abstraction Refinement. Computer Aided Verification. 2000. pp. 154-169. doi: 10.1007/10722167_15
9. SLAM2: Static Driver Verification with Under 4% False Alarms, T. Ball, E. Bounimova, R. Kumar, V. Levin. Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. 2010. pp. 35-42.
10. D. Beyer, T. Henzinger, R. Jhala, R. Majumdar. The software model checker Blast. International Journal on Software Tools for Technology Transfer. 2007. Vol. 9, no. 5-6. Pp. 505-525.
11. D. Beyer, M.E. Keremoglu. CPAchecker: A Tool for Configurable Software Verification. Computer Aided Verification. 2011. pp. 184-190.
12. И.С. Захаров М.У. Мандрыкин В.С. Мутилин Е.М. Новиков А.К. Петренко А.В. Хорошилов. Конфигурируемая система статической верификации модулей ядра операционных систем. Программирование. 2015. Том. 41, номер. 1. сс. 44-67.
13. P. Cousot, R. Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. Proceedings of the 4th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. 1977. pp. 238-252. doi: 10.1145/512950.512973
14. P. Cousot, R. Cousot, J. Feret at al. The ASTREÉ Analyzer. Programming Languages´ and Systems Vol. 3444 of Lecture Notes in Computer Science. Pp. 21-30.
15. J. King. Symbolic Execution and Program Testing. Commun. ACM. 1976. Vol. 19, no. 7. pp. 385-394.
16. Y. Xie, A. Aiken. Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability ACM Trans. Program. Lang. Syst. 2007. Vol. 29, no. 3.
17. F. Ivančić, G. Balakrishnan, A. Gupta at al. Scalable and scope-bounded software verification in Varvel. Automated Software Engineering. 2015. Vol. 22, no. 4. pp. 517-559.
18. Z. Xu, and T. Kremenek and J. Zhang. A memory model for static analysis of C programs. Leveraging Applications of Formal Methods, Verification, and Validation. 2010. Pp 535-548.
19. D. Babic, F. Hutter. Spear theorem prover. Proc. of the SAT. 2008. pp. 187-201.
20. J. Reif, H. Lewis. Symbolic evaluation and the global value graph. Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages. 1977. pp. 104-118.
Рецензия
Для цитирования:
Кошелев В.К., Дудина И.А., Игнатьев В.И., Борзилов А.И. Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды Института системного программирования РАН. 2015;27(5):59-86. https://doi.org/10.15514/ISPRAS-2015-27(5)-5
For citation:
Koshelev V., Dudina I., Ignatyev V., Borzilov A. Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2015;27(5):59-86. (In Russ.) https://doi.org/10.15514/ISPRAS-2015-27(5)-5
Послать статью по эл. почте 