Methods of runtime verification of industrial information security tools based on formal access control models.

The paper discusses methods of runtime verification of software systems that are security protection mechanisms (PM) or include such mechanisms in their design. To ensure a high level of trust and security of software systems, it is necessary to use different verification methods and technologies. In this case, not only the potential power of the method is important, but also the possibility of using it in real conditions of industrial development of large and complex software systems. The rigor and accuracy of verification are ensured by formal methods; however, the use of classical formal methods dictates special, extremely high requirements for personnel and entails additional labor costs. The article proposes a technology for runtime verification of PM, which, on the one hand, is close to testing techniques, therefore it is easier for test engineers to master, and, on the other hand, uses formal access control models and specifications of external PM interfaces as a basis, which are already appearing among OS and DBMS developers, whose products must meet the requirements of the new national standard GOST R 59453.4-2025 "Information Security. Formal access control model. Part 4. Recommendations for verification of information security tools implementing access control policies based on formalized descriptions of the access control model. This standard is also presented in the article.