Specification and Analysis of ABAC Policies in a Rule-Based Framework

Abstract

Attribute-based access control (ABAC) is an access control paradigm whereby access rights to system resources are granted through the use of policies that are evaluated against the attributes of entities (user, subject, and object), operations, and the environment relevant to a request. Many ABAC models, with different variations, have been proposed and formalized. Since the access control policies that can be implemented in ABAC have inherent rule-based specifications, it is natural to adopt a rule-based framework to specify and analyse their properties. We describe the design and implementation of a software tool implemented in Mathematica. Our tool makes use of the rule-based capabilities of a rule-based package developed by us, can be used to specify configurations for the foundational model ABAC$_{\alpha }$ of ABAC, and to check safety properties.

1 Introduction

Access (authorization) control is a fundamental security technique concerned with determining the allowed activities of legitimate users, and mediating every attempt by a user to access a resource in a computing environment. Over the years, many access control models have been developed to address various aspects of computer security, including: Mandatory Access Control (MAC)  [12], Discretionary Access Control (DAC)  [13], and Role-based Access Control (RBAC)  [4]. Attribute-Based Access Control (ABAC) has received significant attention recently, although the concept has existed for more than twenty years. According to NIST  [5]

ABAC is an access control method where subject requests to perform operations on objects are granted or denied based on assigned attributes of the subject, assigned attributes of the object, environment conditions, and a set of policies that are specified in terms of those attributes and conditions.

ABAC is considered a next generation authorization paradigm which eliminates many limitations of the previous access control paradigms. It is dynamic: access control permissions are determined when the access control request is made; it is fine-grained: attributes can be added, to form detailed rules for access control policies; it has support for contextual/environmental conditions; and last but not least: it is flexible, and scalable. In fact, the access control policies that can be implemented in ABAC are limited only by the computational language and the richness of the available attributes. In particular, ABAC policies can be easily configured to simulate DAC, MAC and RBAC.

Until recently, there were no widely accepted formal models for ABAC. The foundational operational models ABAC$_{\alpha }$ and ABAC$_{\beta }$, and the administrative model GURA were proposed recently  [6] as models with “just sufficient” features that can be used to easily and naturally configure the traditional access control models and some advanced features and extensions of RBAC.

The (efficient) implementation and analysis of these formal operational models of ABAC is of great importance. We argue that a rule-based framework is adequate to achieve these goals. For this purpose, we designed and implemented a software tool that allows to specify configurations of ABAC$_{\alpha }$ policies, and to analyse them. The tool is implemented in Mathematica  [15] and is based on the capabilities of $\rho$Log  [8, 9], a rule-based system implemented by us on top of the rule-based capabilities of Mathematica. We highlight the main features that make our rule-based system adequate to specify and analyze the configurations of the access control policies of ABAC$_{\alpha }$.

The rest of this chapter is structured as follows. Section 2 contains a brief description of $\rho$Log and the foundational model ABAC$_{\alpha }$. In Sect. 3 we describe the rule-based tool designed by us for the specification and analysis of ABAC$_{\alpha }$. In Sect. 4 we draw some conclusions and directions for future work.

2 Preliminaries

2.1 The $\rho$Log System

$\rho$Log is a system for rule-based programming with strategies and built-in support for constraint logic programming (CLP). This is a programming style similar to Constraint Logic Programming, where programs consist of rules which are used to answer queries using a calculus based on a variation of SLDNF-resolution  [2] combined with constraint solving. There are, however, some significant differences.

The specification language has an alphabet $\mathscr {A}$ consisting of the following pairwise disjoint sets of symbols:

• $\mathscr {V}_\mathsf{T}$: term variables, denoted by $x,y,z,\ldots$,

• $\mathscr {V}_\mathsf{S}$: hedge variables, denoted by $\overline{x},\overline{y},\overline{z},\ldots$,

• $\mathscr {V}_\mathsf{F}$: function variables, denoted by $X,Y,Z,\ldots$,

• $\mathscr {V}_\mathsf{C}$: context variables, denoted by $\overline{X},\overline{Y},\overline{Y},\ldots$,

• $\mathscr {F}$: unranked function symbols, denoted by $f,g,h,\ldots$.

and distinguishes the following syntactic categories:

$$\begin{aligned} \begin{aligned} t&{:}{:}= x \mid f(\tilde{s}) \mid X(\tilde{s}) \mid \overline{X}(t)&\quad&\text {Term}\\ \tilde{t}&{:}{:}= t_1,\ldots ,t_n \quad (n\ge 0)&\quad&\text {Sequence of terms}\\ s&{:}{:}= t \mid \overline{x}&\quad&\text {Hedge element}\\ \tilde{s}&{:}{:}= s_1,\ldots ,s_n \quad (n\ge 0)&\quad&\text {Hedge} \\ C&{:}{:}= \circ \mid f(\tilde{s}_1,C,\tilde{s}_2) \mid X(\tilde{s}_1,C,\tilde{s}_2) \mid \overline{X}(C)&\quad&\text {Context} \end{aligned} \end{aligned}$$

Hence, hedges are sequences of hedge elements, hedge variables are not terms, term sequences do not contain hedge variables, contexts (which are not terms either) contain a single occurrence of the hole. We do not distinguish between a singleton hedge and its sole element.

We denote the set of terms by $\mathscr {T}(\mathscr {F},\mathscr {V})$, hedges by $\mathscr {H}(\mathscr {F},\mathscr {V})$, and contexts by $\mathscr {C}(\mathscr {F},\mathscr {V})$. Ground (i.e., variable-free) subsets of these sets are denoted by $\mathscr {T}(\mathscr {F})$, $\mathscr {H}(\mathscr {F})$, and $\mathscr {C}(\mathscr {F})$, respectively.

We make a couple of conventions to improve readability. We put parentheses around hedges, writing, e.g., $(f(a),\overline{x},b)$ instead of $f(a),\overline{x},b$. The empty hedge is written as (). The terms a() and X() are abbreviated as a and X, respectively, when it is guaranteed that terms and symbols are not confused. For hedges $\tilde{s}=(s_1,\ldots ,s_n)$ and $\tilde{s}'=(s'_1,\ldots ,s'_{m})$, the notation $(\tilde{s},\tilde{s}')$ stands for the hedge $(s_1,\ldots ,s_n,s'_1,\ldots ,s'_m)$. We use $\tilde{s}$ and $\tilde{r}$ for arbitrary hedges, and $\tilde{t}$ for sequences of terms.

We will also need anonymous variables for each variable category. They are variables without name, well-known in declarative programming. We write just $\_$ for an anonymous term or function variable, and $\_\_$ for an anonymous hedge or context variable. The set of anonymous variables is denoted by $\mathscr {V}_\mathsf{An}$.

A syntactic expression (or, just an expression) is an element of the set $\mathscr {F}\cup \mathscr {V}\cup \mathscr {T}(\mathscr {F},\mathscr {V})\cup \mathscr {H}(\mathscr {F},\mathscr {V}) \cup \mathscr {C}(\mathscr {F},\mathscr {V})$. We denote expressions by E. Atoms are reducibility formulas $t{:}{:}t_1\Longrightarrow t_2$ with the intended reading “$t_1$ reduces to $t_2$ with strategy t.” The negation of this atom is written as .

The rules of $\rho$Log are of the form

$$\begin{aligned} f(\tilde{s}){:}{:}t'\Longrightarrow t''\leftarrow cond_1,\ldots , cond_n. \end{aligned}$$

(1)

with the intended reading “$f(\tilde{s}){:}{:}t'\Longrightarrow t''$ holds whenever $cond_1$ and ... and $cond_n$ hold”, and provide declarative semantics for reducibility formulas. f is the identifier of the strategy and $\tilde{s}$ is its argument: If $\tilde{s}$ is (), the strategy is atomic, otherwise it is parametric. We view (1) as a partial definition of f.

Some strategies with frequent applications are predefined:

• id${:}{:}s\Longrightarrow t$ holds if $s=t$.

• elem${:}{:}l\Longrightarrow e$ holds if e is an element of list l.

• subset${:}{:}l\Longrightarrow s$ holds if s is subset of set l.

• fmap$(t){:}{:}f(s_1,\ldots ,s_n)\Longrightarrow f(t_1,\ldots ,t_n)$ holds if $t{:}{:}s_i\Longrightarrow t_i$ for $1\le i\le n$.

Another way to specify strategies is by using the predefined combinators:

• $t_1\circ t_2{:}{:}t'\Longrightarrow t''$ holds if $t_1{:}{:}t'\Longrightarrow u$ and $t_2{:}{:}u\Longrightarrow t''$ hold for some u.

• $t_1|t_2{:}{:}t'\Longrightarrow t''$ holds if either $t_1{:}{:}t'\Longrightarrow t''$ or $t_2{:}{:}t'\Longrightarrow t''$ holds.

• $t^*{:}{:}t'\Longrightarrow t''$ holds if either $t'=t''$ or there exist $u_1,\ldots ,u_n$ such that $u_1=t'$, $u_n=t''$ and $t{:}{:}u_i\Longrightarrow u_{i+1}$ for all $1\le i<n$.

• $\mathtt{first\_one}(t_1,\ldots ,t_n){:}{:}t'\Longrightarrow t''$ holds if there exists $1\le i\le n$ such that

  $t_i{:}{:}t'\Longrightarrow t''$ and hold for $1\le j<i$.

• $\mathtt{nf}(t){:}{:}t'\Longrightarrow t''$ holds if both $t^*{:}{:}t'\Longrightarrow t''$ and hold.

$\rho$Log can answer queries of the form $cond_1\wedge \ldots \wedge cond_m$ where the variables are (implicitly) existentially quantified. The constraints $cond_i$ in queries and programs are of three kinds: reducibility atoms $t{:}{:}t'\Longrightarrow t''$, irreducibility literals ; and (3) boolean formulas that can be properly interpreted by the constraint solving component of $\rho$Log. To instruct our system to compute one (resp. all) substitution(s) for the variables in the query $cond_1\wedge \ldots \wedge cond_n$ for which it holds, we can submit requests of the form

Another use of $\rho$Log is to compute one or all reducts of a term with respect to a strategy. The request

instructs $\rho$Log to compute one (if any) reduct of $t'$ with respect to strategy t, that is, a term $t''$ such that formula $t{:}{:}t'\Longrightarrow t''$ holds. $\rho$Log reports “no solution found.” if there is no reduct of $t'$ with t. $\rho$Log can also be instructed to find all reducts of a term with respect to a strategy, with

To illustrate, consider the rule-based solutions to the following problems:

• 1. To eliminate all duplicates of elements in a list L, we submit the request

  ApplyRule(nf(elim2),L) where strategy elim2 is defined by the rule

  

  For example, ApplyRule(nf(elim2),$\{1,2,7,2,3,1\}$) yields answer $\{1,2,7,3\}$.

• 2. To find out if (or which) $\mathtt e$ is an element of a list L, we can submit the request Request(elem::$L\Longrightarrow x$) where strategy elim is defined by the rule

  

  For example, Request(elem${:}{:}\{1,2,3\}\Longrightarrow x$) can return the answer $\{x\mapsto 1\}$, and RequestAll(elem${:}{:}\{1,2,3\}\Longrightarrow x$) returns $\{\{x\mapsto 1\},\{x\mapsto 2\},\{x\mapsto 3\}\}.$

• 3. To find all function symbols from a list L that occur in an expression E, we can submit the request ApplyRuleList(getF$(L),E$), where the parametric strategy getF is defined by the rule

  

  For example, {f,g} is the answer to the query

  

Sequence and context variables permit matching to descend to arbitrary depth and width in a tree-like term. The downside of using these kinds of variables in full generality is infinitary unification, and thus the impossibility to find a sound and complete calculus for $\rho$Log. To avoid this problem, we adopted a natural syntactic restriction, called determinism  [8], that ensures that all inference steps of our calculus can be performed by computing matchers instead of most general unifiers. The good news is that matching with sequence and context variables is finitary  [3].

2.2 The Operational Model of ABAC$_{\alpha }$

ABAC$_{\alpha }$ is a formal model of ABAC proposed by X. Jin in his Ph.D. thesis  [6] with a minimal set of features to configure the well-known access control models DAC, MAC, and RBAC. The core components of this operational model are: : users (U), subjects (S), objects (O), user attributes (UA), subject attributes (SA), object attributes (OA), permissions (P), authorization policy, creation and modification policy, and policy languages (Fig. 1).

Fig. 1

(adapted from [7])

The structure of ABAC$_{\alpha }$ model

Users represent human beings who create and modify subjects, and access resources through subjects. Subjects represent processes created by users to perform some actions in the system. Objects represent system entities that should be protected. Users, subjects and objects are mutually disjoint in ABAC$_{\alpha }$, and are collectively called entities. Each user, subject, object is associated with a finite set of user attributes (UA), subject attributes (SA) and object attributes (OA) respectively. Every attribute att has a type, scope, and range of possible values. The sets of attributes specific to each kind of entity, together with their corresponding type, scope, and range, are specified in a configuration type of ABAC$_{\alpha }$: there will be one configuration type for DAC, and others for MAC, RBAC, etc.

In ABAC$_{\alpha }$, the type of an attribute is either atomic or set. The scope of each attribute is a finite set of values $\mathrm{SCOPE}(at)$. If at is of atomic type, then at can assume any value from $\mathrm{SCOPE}(at)$, otherwise it can assume any subset of values from $\mathrm{SCOPE}(at)$. Formally, this means that the range $\mathrm{Range}(at)$ of possible values of an attribute at is either $\mathrm{SCOPE}(at)$ if at is atomic or $2^{\mathrm{SCOPE}(at)}$ if at is set, where each SCOPE(at) is either an unordered, a totally ordered, or a partially ordered finite set. There are six policies that control the operational behaviour of an ABAC$_{\alpha }$-based system, and each of them involves the interaction of two entities:

• authorization policies, which control the permissions that a user can hold on objects and exercise through subjects. Every configuration specifies a finite set P of permissions, and an authorization policy for every $p\in P$,

• policies to control the creation of a subject by a user, or of an object by a subject,

• policies for attribute value assignment: to a subject by the user who created it; or to an object by a subject,

• policies to control subject deletion by its creator.

All these policies grant/deny the corresponding operation based on the result of a boolean function which depends on the old and new attribute values of the interacting entities. According to  [1, 6], each of these six boolean functions can be specified as a boolean formula in an instance of a language scheme called Common Policy Language (CPL). In CPL, the syntax of any formula $\phi$ is of the form

$$\begin{array}{rrl} \phi &{}\text{::= }&{}\phi \wedge \phi \mid \phi \vee \phi \mid (\phi )\mid \lnot \phi \\ &{}\mid &{}\exists x\in set.\phi \mid \forall x\in set.\phi \mid set\mathop {\mathrm {setcompare}}set\\ &{}\mid &{} atomic\in set \mid atomic\mathop {\mathrm {atomiccompare}}atomic\\ {\mathrm {setcompare}}&{}\text{::= }&{}\subset \mid \subseteq \mid \nsubseteq \\ {\mathrm {atomiccompare}}&{}\text{::= }&{} <\mid =\mid \le \end{array}$$

where set is a finite set of values, and atomic are concrete values.

3 A Rule-Based Framework for ABAC$_{\alpha }$

Our rule-based tool for the specification and analysis of ABAC$_{\alpha }$ is built on top of the rule-based programming capabilities of $\rho$Log. The user can specify (1) any particular ABAC$_{\alpha }$ configuration via the commands DeclareCfgType and DeclareConfiguration, and (2) any specific policies compatible with the operational model of ABAC$_{\alpha }$ by declaring in $\rho$Log defining rules for the parametric strategies

$$\begin{aligned}&\mathtt{ConstrS(}{} { typeId}{} \mathtt{)}\quad \mathtt{ConstrO(}{} { typeId}{} \mathtt{)}\\&\mathtt{ConstrModS(}{} { typeId}{} \mathtt{)}\quad \mathtt{ConstrModO(}{} { typeId}{} \mathtt{)}\quad \mathtt{Auth(}{} { typeId,p}{} \mathtt{)}\\&\mathtt{createS(}{} { cId}{} \mathtt{)}\quad \mathtt{createO(}{} { cId}{} \mathtt{)}\quad \mathtt{modSA(}{} { cId}{} \mathtt{)}\quad \mathtt{modOA(}{} { cId}\mathtt{)} \end{aligned}$$

Afterwards, we can check whether it is safe to assume that a subject s can never obtain permission p on an object o in an ABAC$_{\alpha }$-configuration $\mathtt cId$ with the command $\mathtt{CheckSafety[}{} { cId,s, o, p}{]}$.

The meaning of these commands and parametric strategies is described in the remainder of this section.

Every entity (user, subject, or object) is completely described by its attribute values. Therefore, we chose to represent every entity as a term $K(at_1(v_1),\ldots ,at_m(v_m))$ where $K\in \mathtt \{U,S,O\}$ indicates the kind of entity, and every subterm $at_i(v_i)$ indicates that attribute $at_i$ has value $v_i$. Every user has a unique identifier given by the value of its attribute $\mathtt id$. Subjects are created by users and retain the identifier of their creator in the value of subject attribute $\mathtt id$. From now on, we will assume the existence of a function UId(e) which returns the value of attribute $\mathtt id$ for every entity $e\in U\cup S.$ Apart from this, the attribute names, their types and scope are characteristic to a particular configuration of ABAC$_{\alpha }$.

With our tool we can specify a configuration type for every configuration of interest, with the command

This declaration specifies a configuration type with identifier typeId, where

• $\{uAt_{1},\ldots ,uAt_{m}\}$ is the set of user attributes; $\{sAt_{1}$, ..., $sAt_{n}\}$ is the set of subject attributes, and $\{oAt_{1}$, ..., $oAt_{p}\}$ is the set of object attributes;

• the scope of every attribute $at_i$ is the set bound to identifier $sId_i$ in a particular configuration (see below), and its type is $\tau _i\in \{\text{ elem,subset }\}$, where elem stands for atomic and subset for set.

A configuration is an instance of a configuration type, which specifies (1) the configuration type which it instantiates; (2) the sets of values for the identifiers $sId_i$ from the specification of the configuration type, and (3) the initial sets U, S, and O of entities (users, subjects, objects) in the configuration. In our system, the declaration of a concrete configuration of ABAC$_{\alpha }$ has the syntax

Its side effect is to instantiate some globally visible entries:

CfgType(cId) with typeId,

Users(cId) with the set $\{u_1,$ ..., $u_m\}$ of terms for users,

every User(cId,$uId_i$) with the term $u_i$,

Subjects(cId) with the set $\{s_1,\ldots ,s_n\}$ of terms for subjects, and

Objects(cId) with the set $\{o_1,\ldots ,o_q\}$ of terms for objects.

To illustrate, consider the mandatory access control model (MAC). Users and subjects have a clearance attribute of type elem, whose value is a number from a finite set of integers $L=\{1,2,\ldots ,N\}$, which indicates the security level of the corresponding entity. Objects have a sensitivity attribute of type elem whose value is also from L, and represents the sensitivity degree of the information in that object. When read and write are the only permissions on objects, we can assume the set of permissions P to be {read, write}.

A configuration type for MAC can be defined as follows:

A particular MAC configuration can be defined by

3.1 Rules for the Policies of the Configuration Points

The constraint solving component of $\rho$Log allows to specify and interpret correctly all formulas written in instances of the CPL scheme. Therefore, for every configuration type typeId, we can use $\rho$Log to define parametric strategies for the policies of interaction between system entities:

• A user u can create a subject s if ConstrS(typeId)::$\{u,s\}\Longrightarrow \mathtt{true}$ holds, where the defining rule of strategy ConstrS is of the form

  

• A subject s can create an object o if ConstrO(typeId)::$\{s,o\}\Longrightarrow \mathtt{true}$ holds, where the defining rule of strategy ConstrO is of the form

  

• A user u can modify a subject s to become a subject $s'$ if the reducibility formula ConstrModS(typeId)::$\{u,s,s'\}\Longrightarrow \mathtt{true}$ holds, where the defining rule of strategy ConstrModS is of the form

  

• A subject s can modify an object o to become an object $o'$ if the reducibility formula ConstrModO(typeId)::$\{s,o,o'\}\Longrightarrow \mathtt{true}$ holds, where the defining rule of strategy ConstrModO is of the form

  

• A subject s is authorized to hold permission ${{\underline{\mathtt{{p}}}}}\in P$ on an object o if the reducibility formula Auth(typeId,p)::$\{s,o\}\Longrightarrow \mathtt{true}$ holds, where the defining rule of strategy Auth is of the form

  

In these rule-based specifications, $\phi _i$ and $\phi _{5,p}$ are formulas written in the instance of the CPL scheme for the values of the attributes of the interacting entities mentioned in the left-hand side of the corresponding rule.

For example, the mandatory access control (MAC) configuration type with read and write permissions can have the following rule-based specifications

These policies do not allow to modify the attribute values of subjects and objects.

3.2 Rules for the Operational Model

3.2.1 Subject and Object Creation

These are nondeterministic operations: at any time, a user can create any subject whose attribute values satisfy the CPL-formula for the subject creation policy; similarly, a subject can create any object whose attribute values satisfy the CPL-formula for the object creation policy. These operations are implemented in two steps:

• 1. We use the auxiliary functions sSeed(cId) to compute the term

  $\mathtt{S}(sAt_{1}(\mathrm{{SCOPE}}(sAt_{1}),\tau _{1}),\ldots ,sAt_{n}(\mathrm{{SCOPE}}(sAt_{n}),\tau _{n}))$

  and oSeed(cId) which computes the term

  $\mathtt{O}(oAt_{1}(\mathrm{{SCOPE}}(oAt_{1}),\tau _{1}),\ldots ,oAt_{p}(\mathrm{{SCOPE}}(oAt_{p}),\tau _{p}))$,

  where $\tau _i$ is the corresponding attribute type.

  For example, for the MAC configuration MAC-Cfg01 illustrated before, the terms computed by sSeed(MAC-Cfg01) and oSeed(MAC-Cfg01) are S(id({u1, u2}, elem), clearance({1, 2, 3, 4, 5}, elem)) and O(sensitivity({1, 2, 3, 4, 5}, elem)).

• 2. We use the terms computed by sSeed(cId) and oSeed(cId) as “seeds” to create any entity allowed by the creation policies. In rule-based thinking, an entity (subject or object) $K(att_1(v_1),\ldots ,att_k(v_k))$ can be generated from the “seed” term $K(att_{1}(scope_{1},\tau _{1}),\ldots ,att_{k}(scope_{k},\tau _{k}))$ if and only if the reducibility formulas $scope_i\rightarrow _{\tau _i}v_i$ hold. If we define the auxiliary strategy

  

  then the set of entities that can be generated from a seed term st is the set of all e for which the reducibility formula fmap(setAt)${:}{:}st\Longrightarrow e$ holds. Therefore, for a given ABAC$_{\alpha }$ configuration cId:

  • (1) a user u can create a subject s if createS(cId)${:}{:}u\Longrightarrow s$ holds, where the defining rule of the parametric strategy createS is

    

  • (2) a subject s can create an object o if createO(cId)${:}{:}s\Longrightarrow o$ holds, where the defining rule of the parametric strategy createO is

    

3.2.2 Modification of Entity Attributes

Users can try to modify the attributes of subjects created by them, and subjects can try to modify the attributes of objects. A simple way to model these operations for an ABAC$_{\alpha }$ configuration cId of type typeId is as follows:

• (1) Modification of the attribute values of a subject s by a user u can be viewed as generating a subject $s'$ for which ConstrModS(typeId)${:}{:}\{u,s,s'\}\Longrightarrow$true holds. The outcome of changing the attribute values of s is $s'$. We define

  

  and note that modSA(cId)${:}{:}s\Longrightarrow s'$ holds if and only if the user u who created subject s is allowed to modify the attribute values of s to become $s'$.

• (2) Modification of the attribute values of an object o by a subject s can be viewed as generating an object $o'$ for which ConstrModO(typeId)${:}{:}\{s,o,o'\}\Longrightarrow$ true holds. The outcome of changing the attribute values of o is $o'$. We define

  

3.2.3 State Transitions

A system with an ABAC$_{\alpha }$ access control model can be viewed as a state transition system whose states are triples $\{U,S,O\}$ consisting of the existing users (U), subjects (S), and objects (O), and whose transitions correspond to the six operations controlled by the policies of ABAC$_{\alpha }$.

Except for authorized access, the other five operations from the functional specification of ABAC$_{\alpha }$ determine state transitions. Their rule-based specifications are:

In the state transitions defined by these rules, the entities matched by $x_u,x_s,x_o$ are those who interact during rule application.

3.3 Safety Analysis

Safety is a fundamental problem for any protection system. The safety problem for ABAC$_{\alpha }$ asks whether a subject s can obtain permission p for an object o. Recently, it has been shown that this problem is decidable  [1], by identifying a state-matching reduction from ABAC$_{\alpha }$ to the pre-authorization usage control model with finite attribute domains (UCON$^{\text {finite}}_{\text {preA}}$). The result follows from the facts that (1) the safety problem of UCON$^{\text {finite}}_{\text {preA}}$ is decidable  [11], and (2) state-matching reductions, like the one defined in  [1], preserve security properties including safety. It provides an indirect way to implement an algorithm to decide the safety problem of ABAC$_{\alpha }$. In [10] we noticed that this indirection can be avoided: a direct analysis of the operational model of ABAC$_{\alpha }$ revealed the main reasons when a configuration is unsafe. In this section we recall the theoretical results reported in  [10], and illustrate how to use $\rho$Log to turn our theoretical findings into rule-based specifications that can be directly executed. We claim that our approach is a natural and effective way to solve the safety problem for any configuration of ABAC$_{\alpha }$.

3.3.1 Properties of ABAC$_{\alpha }$ Derivations

We start from the state transition view of the operational model described in Sect. 3.2.3. If $e\in S\cup O$ then a derivation $\varPi :St=\{U,S,O\}\Longrightarrow \ldots \Longrightarrow \{U,S',O'\}$ whose transition steps do not delete e may modify the attributes values of e. To analyze the possible changes of the attribute values of e in ABAC$_{\alpha }$, we introduce the auxiliary notion of descendant of e in $\varPi$: $desc_\varPi (e)$ is the entity $e'\in S'\cup O'$ which represents e after performing the operations $op_1,\ldots ,op_n$ in this order. Another useful auxiliary notion is $Desc^{St}(e)=\{desc_\varPi (e)\mid \varPi :St\Longrightarrow ^* \{U,S',O'\}\}.$

With these preparations, the safety problem for ABAC$_{\alpha }$ is

Given:

an ABAC$_{\alpha }$ configuration cId with initial state $St=\{U,S,O\}$, a subject $s\in S$, an object $o\in O$, and a permission $p\in P$,

Decide:

if there is a derivation $\varPi :St \Longrightarrow \ldots \Longrightarrow \{U,S',O'\}$ whose transitions steps do not delete the descendants of s, such that subject $desc_\varPi (s)$ can be authorized to obtain permission p on object $desc_\varPi (o)$. Formally, this means that the formula Auth(typeId$,p){:}{:}\{desc_\varPi (s),desc_\varPi (o)\}\Longrightarrow \mathtt{true}$ holds, where typeId is the configuration type of cId.

In this state transition system, objects can only participate at changing their own attributes. Therefore, objects from $O-\{o\}$ do not affect the truth value of the formula Auth(typeId$,p){:}{:}\{desc_\varPi (s),desc_\varPi (o)\}\Longrightarrow \mathtt{true}.$ Hence it is harmless to assume that the initial state is $\{U,S,\{o\})$ and $\varPi$ has no object creation steps. Also, if $\{U,S,O\}\Longrightarrow \{U,S',O'\}{} {\;\rm then\;}\{U,S\cup S'',O'\}\Longrightarrow \{U,S\cup S'',O'\}{}$ holds too, because we can choose the same participating entities to perform the transition. Therefore, we can assume that $\varPi$ has no subject deletion steps.

Thus, we can assume without loss of generality that the safety problem is

Given:

an ABAC$_{\alpha }$ configuration cId with initial state $St_0=\{U,S,\{o\}\}{} {\;\rm with\;}s\in S,\,{\;\rm and \;\rm a \;\rm permission\;}p\in P$,

Decide:

UNSAFE if there is a derivation $\varPi :St\rightarrow ^* (U,S',\{o'\})$ without subject deletion and object creation steps, such that the reducibility formula

$$ \texttt {Auth(}\mathrm{CfgType}{} \mathtt{(}{{\underline{\mathtt{{cId}}}}}{} \mathtt{)},p\mathtt{)}{:}{:}\{desc_\varPi (s),o'\}\Longrightarrow \texttt {true} $$

holds, and SAFE otherwise.

By [10, Theorem 1], the answer is UNSAFE if and only if there exist $s'\in Desc^{St}(s){\; \rm and\;}o'\in Desc^{St}(o){\; \rm such \;\rm that\;}{} \texttt {Auth(}{{\underline{\mathtt{{typeId}}}}}, p$ $\mathtt{)}{:}{:}\{s',o'\}\Longrightarrow \texttt {true}{}$ holds. In ABAC$_{\alpha }$, all attributes assume values from finite sets specified for cId, therefore $Desc^{St}(s){\; \rm and\;}Desc^{St}(o)$ are finite sets that can be computed. Based on this observation, we designed a safety decision algorithm that computes incrementally the finite sets $Desc^{St}(s){\;\rm and\;}Desc^{St}(o)$, and interleaves their computation with testing if $\mathtt{Auth(}{{\underline{\mathtt{{typeId}}}}}, p\mathtt{)}{:}{:}\{s',o'\}\Longrightarrow \mathtt{true}{} {\;\rm holds \;\rm for \;\rm some\;}s'\in Desc^{St}(s){\; \rm and\;}o'\in Desc^{St}(o)$.

3.3.2 A Rule-Based Safety Decision Algorithm

Suppose $u{\; \rm is \;\rm the \;\rm creator \;\rm of\;}s.{\; \rm If\;}u\not \in U{\; \rm then\;}Desc^{St}(s)=\{s\},\,{ \rm otherwise\;}Desc^{St}(s)=\bigcup _{k=1}^\infty S_k{\; \rm where\;}S_1=\{s\}{}$ and

$$ S_{n+1}=\left\{ s''\not \in \bigcup _{k=1}^n S_k \mid \exists s'\in \bigcup _{k=1}^n S_k .(\mathtt{ModSA(}{} \texttt {cId}\mathtt{)}{{:}{:}}\{u,s'\}\Longrightarrow s'')\right\} \quad \text {if }n\ge 1. $$

Because $Desc^{St}(s){\; \rm is \;\rm finite},\,Desc^{St}(s)=\bigcup _{k=1}^{n_0}S_k{\; \rm where\;}n_0=\min \{n\in \mathbb {N}\mid S_n=\emptyset \}.{\; \rm The \;\rm partition\;}\{S_k\mid 1\le k\le n_0\}{} {\; \rm of\;}Desc^{St}(s){\; \rm can \;\rm be \;\rm computed \;\rm iteratively}\,:\,S_1=\{s\},\,{ \rm and\;}S_{k+1}=\mathrm{ApplyRuleList}(\mathtt{nextS}({{\underline{\mathtt{{cId}}}}},\bigcup _{i=1}^k S_i),\{U,S_k\})$ where the parametric strategy nextS is defined by the rule

We can speed up the safety decision algorithm by interleaving the computation of every $S_k$ with testing if Auth $(\mathrm{CfgType}({{\underline{\mathtt{{cId}}}}}),p){:}{:}\{s',o\}\Longrightarrow \mathtt{true}{} {\;\rm holds \;\rm for \;\rm some\;}s'\in S_k$. We can do this test by checking if ApplyRule(auth?($p,{{\underline{\mathtt{{cId}}}}}),\{S_k,\{o\}\})$ yields true, where the parametric strategy auth? is defined by the rule

As soon as any of these tests yields true, the decision algorithm stops by returning UNSAFE. Otherwise, we end up computing the set $Desc^{St}(s){\;\rm and\;\rm will\;\rm start\;\rm computing\;}Desc^{St}(o)$. The computation of this set can proceed in two steps:

• 1. First, we compute the set_all of all subjects that can show up in the system:$\,S_{all}=\bigcup _{k=1}^\infty S_k{\;\rm where\;}S_1=S,\,S_2$is the set of all subjects that can be created by users in U, and

  $$ S_{n+1}=\left\{ s''\not \in \bigcup _{k=1}^n S_k \mid \exists u\in U.\exists s'\in \bigcup _{k=1}^n S_k.(\mathtt{ModSA(}{{\underline{\mathtt{{cId}}}}}{} \mathtt{)}{{:}{:}}\{u,s'\}\Longrightarrow s'')\right\} $$

  If $n\ge 2.{\;\rm Because\;}S_{all}{} {\;\rm is \;\rm finite},\,S_{all}=\bigcup _{k=1}^{n_1}S_k{\;\rm where\;}n_1=\min \{ n\ge 2\mid \wedge S_n=\emptyset \}.{\;\rm The \;\rm partition\;}\{S_k\mid 1\le k\le n_1\}{} {\;\rm of\;}S_{all}{}$ can be computed incrementally:

  $$\begin{aligned} S_2&=\bigcup _{u\in U}\mathrm{ApplyRuleList}(\mathtt{createS(}{{\underline{\mathtt{{cId}}}}}{} \mathtt{)},u)\\ S_{n+1}&=\mathrm{ApplyRuleList}(\mathtt{nextS}({{\underline{\mathtt{{cId}}}}},\bigcup _{k=1}^nS_k),\{U,S_{k}\})&\text {if }n\ge 2. \end{aligned}$$

• 2. $Desc^{st}(o)=\bigcup _{k=1}^\infty O_k{\;\rm where\;}O_1=\{o\}{}$ and

  $$O_{n+1}=\left\{ o''\not \in \bigcup _{k=1}^n o_k \mid \exists s'\in S_{all}.\exists o'\in \bigcup _{k=1}^n O_k .(\mathtt{ModOA(}{{{\underline{\mathtt{{cId}}}}}}{} \mathtt{)}{{:}{:}}\{s',o'\}\Longrightarrow o'')\right\} $$

  if $n\ge 1.{\;\rm Since\;}Desc^{st}(o){\;\rm is \;\rm finite},\,Desc^{st}(o)=\bigcup _{k=1}^{n_2}O_k{\;\rm where\;}n_2=\min \{n\in \mathbb {N}\mid O_n=\emptyset \}{}$.

With $\rho$Log, it is easy to compute incrementally the partition $\{O_k\mid 1\le k\le n_2\}{} {\;\rm of\;}Desc^{st}(o)\,:\,{\rm for \;\rm every\;}k\ge 1$ we have

$$O_{k+1}=\mathrm{ApplyRuleList}(\mathtt{nextO(}{{{\underline{\mathtt{{cId}}}}}}{} \mathtt{)},\bigcup _{i=1}^k O_i),\{S_{all},O_k\})$$

where the parametric strategy nextO is defined by the rule

Here, again, we can speed up the safety decision algorithm by interleaving the computation of every $O_k$ with testing if Auth $(\mathrm{CfgType}({{\underline{\mathtt{{cId}}}}}),p){:}{:}\{s',o'\}\Longrightarrow \mathtt{true}{} {\;\rm holds \;\rm for \;\rm some\;}s'\in S_{all}{} {\;\rm and\;}o'\in O_k.{\;\rm We \;\rm can \;\rm do \;\rm this \;\rm test \;by \;\rm checking \;\rm if \;\rm the \;\rm request \;\rm ApplyRule}(\mathtt{auth?}(p,{{\underline{\mathtt{{cId}}}}}),S_{all},O_k)$ yields true. As soon as this happens, the algorithm stops by returning UNSAFE. Otherwise, we stop and return SAFE.

This decision algorithm is implemented in the method CheckSafety$\mathtt [{ cId,s, o, p}]$, which returns SAFE if, in configuration $\mathtt cIt,\,{ subject\;}s{\;\rm cannot \;\rm get \;\rm permission\;}p{\;\rm on \;\rm object\;}o$, and UNSAFE otherwise.

For example, the command

returns SAFE because the clearance of subject S(id(u1),clearance(3)) is too high to grant write permission to object O(sensitivity(1)).

4 Conclusion

State-matching reduction [14] is a powerful technique to prove security properties (including safety) of state transition systems. This indirect way to define an algorithm for the safety problem of ABAC$_{\alpha }$ configurations makes hard to observe some important properties that can be used to improve its performance. The direct rule-based analysis performed by us has the following advantages:

• 1. It provides a unified framework to specify policies for ABAC$_{\alpha }$ configurations, the operational model, execute them, and verify some security properties, including safety.

• 2. It allowed us to detect some useful properties of the transition model, that simplified significantly the design of our decision algorithm for safety. In particular, it allowed us to reduce the safety problem of to a simpler one: check if Auth $(\mathrm{CfgType}({{\underline{\mathtt{{cId}}}}}),p){:}{:}\{s',o'\}\Longrightarrow \mathtt{true}{} {\;\rm holds \;\rm for \;\rm some\;}s'\in Desc^{St}(s){\;\rm and\;}o'\in Desc^{St}(o)$. We solved it by identifying rule-based algorithms that interleave detection of unsafety with the incremental computation of $Desc^{St}(s){\;\rm and\;}Desc^{St}(o)$.

• 3. With $\rho$Log, we turned such a rule-based specification into executable code and obtained a practical tool to check the safety of any configuration of interest. The rule-based specification is parametric with respect to the configuration types of ABAC$_{\alpha }$. Therefore, whenever we want to check that, for a given configuration, a subject $s{\;\rm never \;\rm gets \;\rm permission\;}p{ \;\rm on \;\rm an \;\rm object\;}o$, it is enough to do the following:

  • a. specify the configuration and its type, as indicated in Sect. 3.

  • b. call the method CheckSafety(${{\underline{\mathtt{{cfgId}}}}},s, o,p$) which runs our safety-check algorithm. It returns SAFE if $s{\;\rm never \;\rm gets \;\rm permission\;}p$ on o, and UNSAFE otherwise.

There are many other rule-based systems with support for strategic programming, that can be used to formalize state transition systems and study their properties. But $\rho$Log has some outstanding capabilities for this purpose:

• 1. It has four kinds of variables which give the user flexible control to select the components of the term which is transformed. The code is usually quite short and declaratively clear, as witnessed by the rule-based specification of ABAC$_{\alpha }$.

• 2. It inherits from the Wolfram language of Mathematica a rich variety of constraints that can be used in requests and the conditional parts of rules. In particular, the boolean formulas that constrain the operations of ABAC$_{\alpha }$ have direct translations as constraints in the CLP component of $\rho$Log.

• 3. It can generate human-readable traces of the reductions that yield an answer. For the safety problems of ABAC$_{\alpha }$, this capability could be used to produce scenarios that indicate the sequence of transitions that yield a state where a subject $s{\;\rm can \;\rm exercise \;\rm a \;\rm permission\;}p{\;\rm on \;\rm an \;\rm object\;}o$. This capability could become a useful tool to detect security holes of ABAC$_{\alpha }$ configurations, and to fix them. We leave the extension of our a tool with this capability as a direction of future work.