Applying Algebraic Virtual Machine to Cybersecurity Tasks

The paper presents the formal methods for application within the cybersecurity domain in the scope of the program system AVM (Algebraic Virtual Machine). It was developed on the basis of behavior algebra and the theory of interaction of agents and environments. AVM allows the use of different methods for verification of system properties, detection of the behavior given as algebraic patterns, and the definition of equivalency of the formal systems. Two case studies are considered as the application of the algebraic approach for resolving the problem of vulnerability detection and checking resistance to cyber-attacks. It can be efficiently used in model-driven development of safety-critical systems correspondingly to requirements in standards to apply formal methods for verification and testing.