Местоположение издательства:Road Town, United Kingdom
Первая страница:443
Последняя страница:453
Аннотация:Designing a trusted access control mechanism of an operating system (OS) is a complex task if the goal is to achieve high level of security assurance and guarantees of unwanted information flows
absence. Even more complex it becomes when the integration of several heterogeneous mechanisms, like
role-based access control (RBAC), mandatory integrity control (MIC), and multi-level security (MLS) is
considered. This paper presents results of developement 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. Previous 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 level (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. The model is implemented in a Linux-based operating
system using the Linux Security Modules infrastructure