Paradigm in Verification of Access Control

Access control (AC) is one of the most fundamental and widely used requirements for privacy and security. Given a subject´s access request on a resource in a system, AC determines whether this request is permitted or denied based on AC policies (ACPs). This position paper introduces our approach to ensure the correctness of AC using verification. More specifically, given a model of an ACP, our approach detects inconsistencies between models, specifications, and expected behaviors of AC. Such inconsistencies represent faults (in the ACP), which we target at detecting before ACP deployment.