Применение формальных методов при проектировании коллаборационной системы противовирусной защиты

  • Роман Евгеньевич Шарыкин Белорусский государственный университет, пр. Независимости, 4, 220030, г. Минск, Беларусь
  • Александр Николаевич Курбацкий Белорусский государственный университет, пр. Независимости, 4, 220030, г. Минск, Беларусь
DOI: https://doi.org/10.33581/2520-6508-2020-1-59-69

Аннотация

Предлагается подход, позволяющий исследовать математическую модель системы защиты от вирусов на этапе ее проектирования с помощью статистического анализа исполняемой спецификации модели, основанной на формализме распределенных объектно ориентированных стохастических гибридных систем (РООСГС). Важными аспектами модели являются ее распределенный и вероятностный характер. Эти аспекты делают модель более сложной для проведения атак, но в то же время значительно усложняют понимание ее свойств разработчиком. На данном примере мы показываем, как с помощью использования спецификации системы в качестве модели РООСГС вкупе со статистическим анализом можно исследовать ее свойства на раннем этапе проектирования и как с применением данного подхода можно обнаружить «дефекты» модели и исправить их еще в процессе ее создания.

Биографии авторов

Роман Евгеньевич Шарыкин, Белорусский государственный университет, пр. Независимости, 4, 220030, г. Минск, Беларусь

соискатель кафедры технологий программирования факультета прикладной математики и информатики. Научный руководитель – А. Н. Курбацкий

Александр Николаевич Курбацкий, Белорусский государственный университет, пр. Независимости, 4, 220030, г. Минск, Беларусь

доктор технических наук, профессор; заведующий кафедрой технологий программирования факультета прикладной математики и информатики

Литература

  1. Sharykin RE, Kourbatski AN. A model of distributed object-based stochastic hybrid systems. Journal of the Belarusian State University. Mathematics and Informatics. 2019;2:52–61. Russian. DOI: 10.33581/2520-6508-2019-2-52-61.
  2. Sharykin RE, Kourbatski AN. Verification of distributed object-oriented stochastic hybrid systems. Vestnik Grodnenskogo gosudarstvennogo universiteta imeni Yanki Kupaly. Seriya 2. Matematika. Fizika. Informatika, vychislitel’naya tekhnika i upravlenie. 2019;9(3):123–132. Russian.
  3. Meseguer J. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science. 1992;96(1):73–155. DOI: 10.1016/0304-3975(92)90182-F.
  4. Martí-Oliet N, Meseguer J. Rewriting logic: roadmap and bibliography. Theoretical Computer Science. 2002;285(2):121–154. DOI: 10.1016/S0304-3975(01)00357-7.
  5. Clavel M, Durán F, Eker S, Lincoln P, Martí-Oliet N, Meseguer J, et al. Maude: Specification and programming in rewriting logic. Theoretical Computer Science. 2002;285(2):187–243. DOI: 10.1016/S0304-3975(01)00359-0.
  6. Clavel M, Durán F, Eker S, Meseguer J. Chapter 1. Building equational proving tools by reflection in rewriting logic. In: Futatsugi K, Nakagawa AT, Tamai T, editors. CAFE: an industrial-strength algebraic formal method. [S. l.]: Elsevier; 2000. p. 1–31. DOI: 10.1016/B978-044450556-9/50061-7.
  7. Sen K, Viswanathan M, Agha G. On statistical model checking of stochastic systems. In: Etessami K, Rajamani SK, editors. Computer aided verification. Proceedings of the 17th International conference on computer aided verification. Berlin: Springer; 2005. p. 266–280. (Lecture notes in computer science; volume 3576). DOI: 10.1007/11513988_26.
  8. Briesmeister L, Porras P. Microscopic simulation of a group defense strategy. In: Nicol D, editor. Proceedings of the 19th Workshop on principles of advanced and distributed simulation; 2005 June 1–3; Monterey, USA. Los Alamitos: IEEE Computer Society; 2005. p. 254–261. DOI: 10.1109/PADS.2005.13.
  9. Anagnostakis KG, Greenwald MB, Ioannidis S, Keromytis AD, Li D. A cooperative immunization system for untrusting Internet. In: Moreton N, editor. The 11th IEEE International conference on networks; 2003 September 28 – October 1; Sydney, Australia. Los Alamitos: IEEE Computer Society; 2003. p. 403–408. DOI: 10.1109/ICON.2003.1266224.
  10. Nojiri D, Rowe J, Levitt K. Cooperative response strategies for large scale attack mitigation. In: Werner B, editor. Proceedings DARPA information survivability conference and exposition; 2003 April 22–24; Washington, USA. Los Alamitos: IEEE Computer Society; 2003. p. 293–302. DOI: 10.1109/DISCEX.2003.1194893.
  11. Twycross J, Williamson MM. Implementing and testing a virus throttle. In: Paxson V, editors. Proceedings of the 12th conference on USENIX security symposium; 2003 August 4–8; Washington, USA. Berkeley: USENIX Association; 2003. p. 285–294.
  12. Singh S, Estan C, Varghese G, Savage S. Automated worm fingerprinting. In: Brewer E, editor. Proceedings of the 6th conference on symposium on operating systems design and implementation; 2004 December 6–8; San Francisco, USA. Berkeley: USENIX Association; 2004. p. 45–60.
  13. Kim H-A, Karp B. Autograph: Toward automated, distributed worm signature detection. In: Blaze M, editor. Proceedings of the 13th conference on USENIX security symposium; 2004 August 9–13; San Diego, USA. Berkeley: USENIX, The Advanced Computing Systems Association; 2004. p. 271–286.
  14. Briesmeister L, Porras P. Automatically deducing propagation sequences that circumvent a collaborative worm defense. In: Hassanein H, editor. Proceedings of the International performance computing and communications conference; 2006 April 10–12; Phoenix, USA. Los Alamitos: IEEE Computer Society; 2006. p. 587–592. DOI: 10.1109/.2006.1629456.
  15. Sharykin RE. Maude specification of the stochastic collaborative virus defense system [Internet]. GitHub [cited 2020 January 2]. Available from: https://github.com/shymaude/virusDefense/blob/master/defense.shymaude.
  16. Briesemeister L, Porras PA, Tiwari A (Computer Science Laboratory). Model checking of worm quarantine and counter-quarantine under a group defense. Technical Report. Menlo Park: SRI International; 2005. Technical Report Number: SRI-CSL-05-03, SRI Project 13738.
  17. Sebastio S, Vandin A. MultiVeStA: statistical model checking for discrete event simulators. In: Horvath A, editor. Proceedings of the 7th International conference on performance evaluation methodologies and tools; 2013 December 10–12; Torino, Italy. Brussels: Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering; 2013. p. 310–315. DOI: 10.4108/icst. valuetools.2013.254377.
  18. AlTurki M, Meseguer J. PVeStA: a parallel statistical model checking and quantitative analysis tool. In: Corradini A, Klin B, Cirstea C, editors. Algebra and coalgebra in computer science. International conference on algebra and coalgebra in computer science. Berlin: Springer; 2011. p. 386–392. (Lecture notes in computer science; volume 6859).
Опубликован
2020-03-29
Ключевые слова: математическое моделирование, гибридные системы, стохастические системы, спецификация моделей, совместная антивирусная защита
Как цитировать
Шарыкин, Р. Е., & Курбацкий, А. Н. (2020). Применение формальных методов при проектировании коллаборационной системы противовирусной защиты. Журнал Белорусского государственного университета. Математика. Информатика, 1, 59-69. https://doi.org/10.33581/2520-6508-2020-1-59-69
Выпуск
№ 1 (2020): Журнал Белорусского государственного университета. Математика. Информатика
Раздел
Теоретические основы информатики

Copyright (c) 2020 Журнал Белорусского государственного университета. Математика. Информатика

Лицензия Creative Commons

Это произведение доступно по лицензии Creative Commons «Attribution-NonCommercial» («Атрибуция — Некоммерческое использование») 4.0 Всемирная.

Авторы, публикующиеся в данном журнале, соглашаются со следующим:

  1. Авторы сохраняют за собой авторские права на работу и предоставляют журналу право первой публикации работы на условиях лицензии Creative Commons Attribution-NonCommercial. 4.0 International (CC BY-NC 4.0).
  2. Авторы сохраняют право заключать отдельные контрактные договоренности, касающиеся неэксклюзивного распространения версии работы в опубликованном здесь виде (например, размещение ее в институтском хранилище, публикацию в книге) со ссылкой на ее оригинальную публикацию в этом журнале.
  3. Авторы имеют право размещать их работу в интернете (например, в институтском хранилище или на персональном сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению и большему количеству ссылок на данную работу. (См. The Effect of Open Access).