A Rule-based Approach to the Decidability of Safety of ABACα

ABACα is a foundational model for attribute-based access control with a minimal set of capabilities to configure many access control models of interest, including the dominant traditional ones: discretionary (DAC), mandatory (MAC), and role-based (RBAC). A fundamental security problem in the design of ABAC is to ensure safety, that is, to guarantee that a certain subject can never gain certain permissions to access certain object(s). We propose a rule-based specification of ABACα and of its configurations, and the semantic framework of ρLog to turn this specification into executable code for the operational model of ABACα. Next, we identify some important properties of the operational model which allow us to define a rule-based algorithm for the safety problem, and to execute it with ρLog. The outcome is a practical tool to check safety of ABACα configurations. ρLog is a system for rule-based programming with strategies and built-in support for constraint logic programming (CLP). We argue that ρLog is an adequate framework for the specification and verification of safety of ABACα configurations. In particular, the authorization policies of ABACα can be interpreted properly by the CLP component of ρLog, and the operations of its functional specification can be described by five strategies defined by conditional rewrite rules.