Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Journal "Software Engineering"
a journal on theoretical and applied science and technology
ISSN 2220-3397
Issue N4 2020 year
Formal access control models are used to design, implement and justify the security of the access control mechanism, which is part of many information security systems such as operating systems (OS), DBMS. Russian practice of developing information security systems, it is advisable to mention the mandatory entity-role model of access control and information flows in OS of Linux set (MROSL DP-model), developed for implementation in OS Astra Linux Special Edition. The model is formalized using Event-B formal method (formalized notation) and its correctness is formally verified with the help of the Rodin toolset. This article presents methods of formalization of the MROSL DP-model using subtypes and total functions of Event-B, which allow logically integrate checks of conditions specified for role-based access control (RBAC), mandatory integrity control (MIC) and multi-level security (MLS), and improve the structure of formalized notation elements used. The result of using these methods in refining the formalized notation was its approach to the practical implementation of the access control mechanism in the OS Astra Linux Special Edition; simplification of formal deductive verification of formalized notation using the Rodin tool, at the same time automated detection of possible errors or their duplication, addition of refinement levels also. Refinement levels simulate (other) systems interacting with OS. Those systems implement complex access control mechanisms independently, for example, DBMS PostgreSQL. These methods are used in development of the MROSL DP-model, and can also be useful in development of other formal access control models and verification using tools, which meet the actual regulatory documents of FSTEC Russia.