Comparison of methods for modeling access control in OS and DBMS in Event-B for the purpose of their verification with Rodin and ProB tools

The paper presents two methods of modeling interacting systems with developed access control mechanisms, such as OS and DBMS. These methods are the result of translating the description of the formal access control model of Astra Linux Special Edition OS (MROSL DP-model) from mathematical to formalized notation using the formal Event-B method, as well as its automatic verification using Rodin and ProB tools. The considered methods are based on the use of various options for constructing a hierarchy of specifications of the MROSL DP-model in the formalized notation using the technique “refinement”. We compare these methods showing their advantages and disadvantages. They consist in the complexity of writing specifications, the need to repeat proofs during the verification with the Rodin tool, the possibility of eliminating the effect of “combinatorial explosion” during the verification with the ProB tool. Based on the results of the comparison, it is concluded that considered methods can be useful in the development of other formal access control models and their verification using appropriate tools.