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

R. E. Sharykin ; A. N. Kurbatskii

Journal of the Belarusian State University. Mathematics and Informatics, Tome 1 (2020), pp. 59-69.

Résumé

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.

Détail

Keywords: mathematical modeling; hybrid systems;stochastic systems; modelspecification; collaborative virus defense.

Bibliographie

[1] R. E. Sharykin, A. N. Kurbatskii, “Model raspredelennykh ob'ektno orientirovannykh stokhasticheskikh gibridnykh sistem”, Zhurnal Belorusskogo gosudarstvennogo universiteta. Matematika. Informatika, 2 (2019), 52–61 | DOI | MR | Zbl

[2] R. E. Sharykin, A. N. Kurbatskii, “Verifikatsiya raspredelennykh ob'ektno orientirovannykh stokhasticheskikh gibridnykh sistem”, Vestnik Grodnenskogo gosudarstvennogo universiteta imeni Yanki Kupaly. Matematika. Fizika. Informatika, vychislitelnaya tekhnika i upravlenie, 9(3) (2019), 123–132

[3] J. Meseguer, “Conditional rewriting logic as a unified model of concurrency”, Theoretical Computer Science, 96(1) (1992), 73–155 | DOI | MR | Zbl

[4] N. Marti-Oliet, J. Meseguer, “Rewriting logic: roadmap and bibliography”, Theoretical Computer Science, 285(2) (2002), 121–154 | DOI | MR | Zbl

[5] M. Clavel, F. Duran, S. Eker, P. Lincoln, N. Marti-Oliet, J. Meseguer, “Maude: Specification and programming in rewriting logic”, Theoretical Computer Science, 285(2) (2002), 187–243 | DOI | MR | Zbl

[6] M. Clavel, F. Duran, S. Eker, J. Meseguer, “Building equational proving tools by reflection in rewriting logic”, CAFE: an industrial-strength algebraic formal method, 2000, 1–31 | DOI | MR

[7] K. Sen, M. Viswanathan, G. Agha, “On statistical model checking of stochastic systems; Computer aided verification”, Proceedings of the 17th International conference on computer aided verification, 3576 (2005), 266–280, Berlin: Springer | DOI | MR | Zbl

[8] L. Briesmeister, P. Porras, “Microscopic simulation of a group defense strategy”, Proceedings of the 19th Workshop on principles of advanced and distributed simulation (Monterey, USA), 2005, 254–261, Los Alamitos: IEEE Computer Society | DOI

[9] K. G. Anagnostakis, M. B. Greenwald, S. Ioannidis, A. D. Keromytis, D. Li, “A cooperative immunization system for untrusting Internet”, The 11th IEEE International conference on networks (Sydney, Australia), 2003, 403–408, Los Alamitos: IEEE Computer Society | DOI

[10] D. Nojiri, J. Rowe, K. Levitt, “Cooperative response strategies for large scale attack mitigation”, Proceedings DARPA information survivability conference and exposition (Washington, USA), 2003, 293–302, Los Alamitos: IEEE Computer Society | DOI

[11] J. Twycross, M. M. Williamson, “Implementing and testing a virus throttle”, Proceedings of the 12th conference on USENIX security symposium (Washington, USA), 2003, 285–294, Berkeley: USENIX Association

[12] S. Singh, C. Estan, G. Varghese, S. Savage, “Automated worm fingerprinting”, Proceedings of the 6th conference on symposium on operating systems design and implementation (San Francisco, USA), 2004, 45–60, Berkeley: USENIX Association

[13] H-A. Kim, B. Karp, “Autograph: Toward automated, distributed worm signature detection”, Proceedings of the 13th conference on USENIX security symposium (San Diego, USA), 2004, 271–286, Berkeley: USENIX, The Advanced Computing Systems Association

[14] L. Briesmeister, P. Porras, “Automatically deducing propagation sequences that circumvent a collaborative worm defense”, Proceedings of the International performance computing and communications conference (Phoenix, USA), 2006, 587–592, Los Alamitos: IEEE Computer Society | DOI

[15] R. E. Sharykin, “Spetsifikatsiya kollaboratsionnoi sistemy zaschity ot virusnykh atak v srede Maude”, GitHub: {https://github.com/shymaude/virusDefense/blob/master/defense.shymaude}

[16] L. Briesemeister, P. A. Porras, A. Tiwari, “Model checking of worm quarantine and counter-quarantine under a group defense”, Technical Report. Menlo Park: SRI International, 2005

[17] S. Sebastio, A. Vandin, “MultiVeStA: statistical model checking for discrete event simulators”, Proceedings of the 7th International conference on performance evaluation methodologies and tools (Torino, Italy), 2013, 310–315, Brussels: Institute for Computer Sciences, Social-Informatics and Telecommunications Engineering | DOI

[18] M. AlTurki, J. Meseguer, “PVeStA: a parallel statistical model checking and quantitative analysis tool”, Algebra and coalgebra in computer science, Springer (Berlin), 2011