Эффективное исполнение программного кода в контролируемом окружении как способ улучшения результатов статического анализа и верификации программ


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. (In Russ.) https://doi.org/10.18255/1818-1015-2015-6-763-772

Просмотров: 508

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)