An Approach to Formally Validate and Verify the Compliance of Low Level Access Control Policies

Our research works are in the context of the integrity verification and optimization of access control policies in relational database management systems (RDBMSs). Indeed, resources in charge of administrating access control policies, like DBMSs, can easily permit the following malfunctions. (1) The record of illegal updates leading to a non-compliance of the policy regarding its original specification. This can occur after an intrusion attempt or an illegal delegation of rights. (2) The implementation of more than a unique access control model such as RBAC, DAC, etc. This situation can lead to redundancy, inconsistency or contradiction in the expression of the policy. (3) The exposure of the database to inner threats relative to illegal updates or access paradoxically made by authorized users. These vulnerabilities joined with challenges in the management of the policy, related to the evolution of access control models to fine grained access control, can easily corrupt the compliance of the policy. Hence, an important aspect is to help security architects verifying the correspondence and establishing the equivalence between the security planning and its real implementation. In this paper, we introduce our approach to address this problem. We transform the high level and the low level policies in a logic-like formalism that offers a solid environment to verify and validate properties of access control policies.