Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ
https://doi.org/10.18255/1818-1015-2015-6-763-772
Аннотация
Существующие средства и методы статического анализа и верификации кода на языке С используют различные методики упрощения программной модели, приводящие к значительному снижению точности анализа. В данной работе представлен новый подход к повышению точности анализа путем исполнения программной модели в контролируемом окружении, которое позволяет точно определять ошибочные ситуации, такие, как нарушения контрактов кода и ошибки работы с памятью, оставаясь при этом эффективным с точки зрения затрат по времени и по памяти. Данный подход был реализован в модуле под названием «Tassadar» в рамках средства ограниченной проверки моделей «Borealis». Прототип был опробован на стандартных наборах тестовых программ данного средства и показал минимальное влияние на его общую производительность.
Статья представляет собой расширенную версию доклада на VI Международном семинаре “Program Semantics, Specification and Verification: Theory and Applications”, Казань, 2015.
Статья публикуется в авторской редакции.
Об авторах
М. А. Беляев
Санкт-Петербургский политехнический университет им. Петра Великого
Россия
Россия
ассистент,
194021, г. Санкт-Петербург, Политехническая ул., 21
В. М. Ицыксон
Санкт-Петербургский политехнический университет им. Петра Великого
Россия
Россия
доцент,
194021, г. Санкт-Петербург, Политехническая ул., 21
Список литературы
1. M. Akhin, M. Belyaev, V. Itsykson, “Software defect detection by combining bounded model checking and approximations of functions”, Automatic Control and Computer Sciences, 48:7 (2014), 389–397.
2. P. Baudin, J. C. Filliˆatre, T. Hubert, C. March´e, B. Monate, Y. Moy, V. Prevosto, 2008, ACSL: ANSI/ISO C Specification Language. Preliminary Design, version 1.4., Preliminary.
3. J. L. Bentley, “Solutions to klee’s rectangle problems”, Technical report, 1977.
4. D. Beyer, “Competition on software verification”, 2012, 504–524.
5. A. Biere, A. Cimatti, E. M. Clarke, Y. Zhu, “Symbolic model checking without BDDs”, 1999, 193–207.
6. M. K. Buckland, F. C. Gey, “The relationship between recall and precision”, JASIS, 45:1 (1994), 12–19.
7. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, “Counterexample-guided abstraction refinement”, CAV, 2000, 154–169.
8. R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, F. K. Zadeck, “Efficiently computing static single assignment form and the control dependence graph”, ACM TOPLAS, 13:4 (1991), 451–490.
9. A. Groce, R. Joshi, “Extending model checking with dynamic analysis”, Verification, model checking, and abstract interpretation, 2008, 142–156.
10. ISO, The ANSI C standard (C99), ISO/IEC, 1999.
11. F. Ivanˇci´c, S. Sankaranarayanan, “NECLA static analysis benchmarks”, 2009.
12. D. Kroening, A. Groce, E. Clarke, “Counterexample guided abstraction refinement via program execution”, Formal methods and software engineering, 2004, 224–238.
13. C. Lattner, V. Adve, “LLVM: A compilation framework for lifelong program analysis & transformation”, 2004, 75–86.
14. D. Novillo, “Tree SSA: A new optimization infrastructure for GCC”, Proceedings of the 2003 gCC developers’ summit, 21, 2014, 83–93.
Рецензия
Для цитирования:
Беляев М.А., Ицыксон В.М. Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ. Моделирование и анализ информационных систем. 2015;22(6):763-772. https://doi.org/10.18255/1818-1015-2015-6-763-772
For citation:
Belyaev M., Itsykson V. Fast and Safe Concrete Code Execution for Reinforcing Static Analysis and Verification. Modeling and Analysis of Information Systems. 2015;22(6):763-772. https://doi.org/10.18255/1818-1015-2015-6-763-772
Просмотров: 1258
Послать статью по эл. почте 