Summary

The main feature of a secure information system is protecting sensitive data and services of an organization. This goal can be achieved via enforcing various security controls such as authentication, authorization, encryption, intrusion detection, audit, availability and privacy mechanisms. Among those mechanisms, the access control is considered as one of the most important and strong driving forces for protecting the data and preserving the privacy. It orchestrates access to resources based on appropriate rights in defined policies. On another hand, resources in charge of administrating access control policies, like Data Base Management Systems (DBMSs), can easily permit the following malfunctions. (1) The record of illegal updates leading to non-compliance between the concrete instance of the policy and its original specification. This can occur following an intrusion attempt or an illegal delegation of rights. (2) DBMSs usually support several mechanisms for managing access control such as DAC, MAC, RBAC based access, etc. This can lead to redundancy, inconsistency and contradiction in the expression of the low level policy if it is managed using more than one mechanism. In this paper, we provide a synthesis of the problem of non-conformity in concrete RBAC-based policies. Then, we introduce a formal system to face this problem. The proposal relies on logic-like formalisms which offer a solid environment to verify access control properties. After that, we discuss the relevance of our proposal and provide future directives. Key words