Application of formal methods in the design of a collaborative virus defense system

Authors

  • Raman E. Sharykin Belarusian State University, 4 Niezaliežnasci Avenue, Minsk 220030, Belarus
  • Alexander N. Kourbatski Belarusian State University, 4 Niezaliežnasci Avenue, Minsk 220030, Belarus

Keywords:

mathematical modeling, hybrid systems, stochastic systems, model specification, collaborative worm defense

Abstract

This article proposes an approach that allows us to study a mathematical model of a virus protection system at the stage of its design using statistical analysis of an executable model specification based on the formalism of Distributed Object Based Stochastic Hybrid Systems (DOBSHS). Important aspects of the model are its distributed and probabilistic nature. These aspects make the model more difficult to carry out attacks, but at the same time significantly complicate the understanding of its properties by the developer. In this example, we show how, using the specification of the system as a DOBSHS model, coupled with its statistical analysis, we can investigate its properties at an early stage of design and how, using this approach, we can detect «defects» of the model and correct them during the process of creating the model.

Author Biographies

  • Raman E. Sharykin, Belarusian State University, 4 Niezaliežnasci Avenue, Minsk 220030, Belarus

    competitor at the department of software engineering, faculty of applied mathematics and computer science

  • Alexander N. Kourbatski, Belarusian State University, 4 Niezaliežnasci Avenue, Minsk 220030, Belarus

    doctor of science (engineering), full professor; head of the department of software engineering, faculty of applied mathematics and computer science

References

  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).

Downloads

Additional Files

Published

2020-03-29

Issue

No. 1 (2020): Journal of the Belarusian State University. Mathematics and Informatics

Section

Theoretical Foundations of Computer Science

License

The authors who are published in this journal agree to the following:

  1. The authors retain copyright on the work and provide the journal with the right of first publication of the work on condition of license Creative Commons Attribution-NonCommercial. 4.0 International (CC BY-NC 4.0).
  2. The authors retain the right to enter into certain contractual agreements relating to the non-exclusive distribution of the published version of the work (e.g. post it on the institutional repository, publication in the book), with the reference to its original publication in this journal.
  3. The authors have the right to post their work on the Internet (e.g. on the institutional store or personal website) prior to and during the review process, conducted by the journal, as this may lead to a productive discussion and a large number of references to this work. (See The Effect of Open Access.)

How to Cite

[1]
Sharykin, R.E. and Kourbatski, A.N. 2020. Application of formal methods in the design of a collaborative virus defense system. Journal of the Belarusian State University. Mathematics and Informatics. 1 (Mar. 2020), 59–69. DOI:https://doi.org/10.33581/2520-6508-2020-1-59-69.