• A
  • A
  • A
  • ABC
  • ABC
  • ABC
  • А
  • А
  • А
  • А
  • А
Regular version of the site

Article

Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System

Programming and Computer Software, Pleiades Publishing, Ltd.. 2020. Vol. 46. No. 7. P. 1-11.
Devyanina P. N., Khoroshilov A. V., Kuliamin V., Petrenko A. K., Shchepetkov I.

Designing a trused access control mechanism of operating system (OS) is a complex task if the goal is to achieve high level of security assurance and guarantees of unwanted informatin flows absence. Even more complex it becomes when the integration of several haterogeneous mechanisms, like role-based access control (RBAC), mandatory integrity control (MIC), and multi-level security (MLS) is considered. This paper presents results of development of a hierarchical integrated model of access control and information flows (HIMACF), which provides a holistic integration of RBAC, MIC, and MLS preserving key security properties of all those mechanisms. Previos version of this model is called MROSL DP - model. Now the model is formalized using Event-B formal method and its correctness is formally verified. In the hierarchical representation of the model, each hierarchy lavel (module) corresponds to a separate security control mechanism, so the model can be verified with less effort reusing the results of verification of lower level modules. Nhe model is implemented in a Linux-based operating system using the Linux Security Modules infrastructure.