A safety-checker for the ABAC_α model

Access control is a fundamental security requirement for computing environments: It controls the ability of a subject to use an object in some specific manner. A subject represents a user and any system process or entity that acts on behalf of a user. Users represent individuals who interact directly or indirectly with a system and have been authenticated and established their identities. Objects are the protected entities, and can represent either system abstractions (e.g., processes, files, or ports) or system resources (e.g., printers).

1 ABAC and ABAC_α

Attribute-based access control (ABAC) is a logical access control with great flexibility to specify access control policies as rules which get evaluated against the attributes of participating entities (user/subject or subject/object), operations, and the environment relevant to a request. Considerable work has been done and a number of formal models have been proposed recently for ABAC [Jin14, JKS12, PS04]. Among them, ABAC_α became popular because of its minimal set of features that make it powerful enough to configure the dominant traditional access control models DAC, MAC and RBAC.

A fundamental security problem in the design of ABAC models is safety. According to [HRU76], the safety problem for protection systems is to determine in a given situation whether a subject can acquire a particular right to an object. Recently, it was shown that safety of ABAC_αis decidable [AS17]. The proof was based on state-matching reduction of safety of ABAC_α to safety of the preauthorization model UCON${}_{\mathrm{preA}}{}^{}{}_{}{}^{\mathrm{finite}}$, which is known to be decidable [RS16].

ABAC_α is 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).

This problem can be solved nicely in a rule-based framework based on the $\rho$Log calculus. We have developed a tool built on top of the rule-based capabilities of RhoLog, which allows us to do the following:

1. specify a configuration of interest for ABAC_α

2. call the method

   CheckSafety[cId,$s,o,p$]
   

   to check if the configuration guarantees that subject s never gets authorization to exercise permission $p$ on an object $o$. If yes, the method returns SAFE, otherwise it returns UNSAFE.

2 Preliminaries

ABAC_α is a formal model of ABAC with a minimal set of features to configure the traditional models DAC, MAC, and RBAC. Its core components are entities of three kinds: users, subjects, and objects. 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.

Every kind of entity has a fixed set of attributes. Every attribute has a type, scope, and range of possible values. The sets of attributes specific to each kind of entity, together with their type, scope, and range, are specified in a configuration type of ABAC_α: there will be one configuration type for DAC, and others for MAC, RBAC, etc.

In ABAC_α, the type of an attribute is either atomic or set. The scope of each attribute $at$ is a finite set of values SCOPE$(at)$. If $at$ is of atomic type then it can assume any value from SCOPE$(at)$, otherwise it can assume any subset of values from SCOPE$(at)$. Formally, this means that the range Range$(at)$ of possible values of $at$ is SCOPE$(at)$ if $at$ is of atomic type, and $2^{\mathrm{SCOPE}(at)}$ otherwise.

User creation, attribute value assignment of user at creation time, user deletion and modification of a user’s attribute values are operations done by the security administrator and are outside the scope of ABAC_α. Therefore, in a running configuration of ABAC_α, the set $U$ of existing users is fixed, but the sets $S$ of existing subjects and $O$ of existing objects may change. The identity of every user is specified by the value of a special attribute "id" of atomic type. In our system, configuration types are declared as follows:

DeclareCfgType[typeId,{"SA"$\to \{sA{t}_1,\mathrm{\dots },sA{t}_n\}$,"OA"$\to \{oA{t}_1,\mathrm{\dots },oA{t}_p\}$,
    "Scope"$\to \{a{t}_1\to \bullet [sI{d}_1,{\tau }_1],\mathrm{\dots },a{t}_r\to \bullet [sI{d}_r,{\tau }_r]\}$}]

Such a declaration specifies a configuration type with unique identifier typeId (a string), where: $\{uA{t}_1,\mathrm{\dots },uA{t}_m\}$, $\$sA{t}_1,\mathrm{\dots },sA{t}_n$, and $\{oA{t}_1,\mathrm{\dots },oA{t}_p\}$ are the sets of attributes for users, subjects, and objects, respectively; $\{a{t}_1,\mathrm{\dots },a{t}_r\}$ is their union; the scope of every attribute $a{t}_i$ (a string) is the set bound to identifier $sI{d}_i$ in a particular configuration (see below), and its type is , where "Elem" stands for atomic and "Subset" for set.

For example, the configuration type of the discretionary access models DAC (discretionary), MAC (mandatory) and RBAC (role-based) are given by

DeclareCfgType["DAC",{"UA"$\to${"id"},"SA"$\to${"id"},"OA"$\to${"id","r","w"},
  "Scope"$\to${"id"$\to \bullet$["UId","Elem"],
    "r"$\to \bullet$["UId","Subset"],
    "w"$\to \bullet$["UId","Subset"]}}]

DeclareCfgType["MAC",{"UA"$\to${"id","clearance"},
    "SA"$\to${"id","clearance"},"OA"$\to${"sensitivity"},
  "Scope"$\to${"id"$\to \bullet$["UId","Elem"],
    "clearance"$\to \bullet$["level","Elem"],
    "sensitivity"$\to \bullet$["UId","Elem"]}}]

DeclareCfgType["RBAC",{"UA"$\to${"id","role"},
    "SA"$\to${"id","role"},"OA"$\to${"rrole","wrole"},
  "Scope"$\to${"id"$\to \bullet$["UId","Elem"],
    "role"$\to \bullet$["roleId","Subset"],
    "rrole"$\to \bullet$["roleId","Subset"],
    "wrole"$\to \bullet$["roleId","Subset"]}}]

We represent the system entities as first-order terms of the form

• $\bullet 𝚄[uA{t}_1[v_1],\mathrm{\dots },uA{t}_m[v_m]]$

• $\bullet 𝚂[sA{t}_1[v_1],\mathrm{\dots },sA{t}_n[v_n]]$

• $\bullet 𝙾[oA{t}_1[v_1],\mathrm{\dots },oA{t}_p[v_p]]$

where $v_i$ are the corresponding attribute values.

Every user has a unique ID, which is the string value of its "id" attribute. Subjects keep track of the ID of their creator in the value of their "id" attribute. We will assume without loss of generality that , and that there is a function $\mathrm{𝚄𝙸𝚍}[e]$ which returns the value of the attribute "id" of $e\in U\cup S$.

A configuration of ABAC_α is an instance of a configuration type which specifies (1) the configuration type which it instantiates; the sets of values for the identifiers $sI{d}_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 tool, the declaration of a concrete configuration of ABAC_α has the syntax

DeclareConfiguration[cId,
 {"CfgType"$\to$typeId,
  "Users"$\to \{uI{d}_1\to u_1,\mathrm{\dots },uI{d}_m\to u_m\}$,
  "Range"$\to \{$"UId"$\to \{uI{d}_1,\mathrm{\dots },uI{d}_m\}$,
             $sI{d}_1\to \mathrm{SCOPE}[a{t}_1],\mathrm{\dots },sI{d}_r\to \mathrm{SCOPE}[a{t}_r]$,
  "Subjects"$\to \{s_1,\mathrm{\dots },s_n\}$,"Objects"$\to \{o_1,\mathrm{\dots },o_q\}$}
]

Its side effect is to instantiate some globally visible entries:

• CfgType[cId] with typeId,

• Users[cId] with the set of users $\{u_1,\mathrm{\dots },u_m\}$,

• every User[cId,$uI{d}_i$] with user $u_i$, Subjects[cId] with the set of subjects $\{s1,\mathrm{\dots },s_n\}$,

• Objects[cId] with the set of objects $\{o_1,\mathrm{\dots },o_q\}$.

For example, the following is a declaration of a DAC configuration:

DeclareConfiguration["DAC-Cfg01",
  {"CfgType"->"DAC",
   "Users"$\to${"u1"$\to \bullet$U["id"["u1"]],"u2"$\to \bullet$U["id"["u2"]],
             "u3"$\to \bullet$U["id"["u3"]]},
   "Range"$\to${"UId"$\to${"u1","u2","u3"}},
   "Subjects"$\to \{\bullet$S["id"["u1"]],$\bullet$S["id"["u3"]]},
   "Objects"$\to \{\bullet$O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u1","u2"}]],
               $\bullet$O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u2","u3"}]]}}]

It specifies an initial system state with three users identified by strings "u1", "u2", "u3"; two subjects; and two objects. The first object grants read access to subjects created by users "u1", "u3" and write access to subjects created by users "u1", "u2". The second object grants read access to subjects created by users "u1", "u3" and write access to subjects created by users "u2", "u3".

The following declaration is for a MAC configuration with five access levels:

DeclareConfiguration["MAC-Cfg01",
  {"CfgType"->"MAC",
   "Users"$\to${"u1"$\to \bullet$U["id"["u1"],"clearance"[3]],
             "u2"$\to \bullet$U["id"["u2"],"clearance"[4]]},
   "Range"$\to${"UId"$\to${"u1","u2"},"level"->{1,2,3,4,5}},
   "Subjects"$\to \{\bullet$S["id"["u1"],"clearance"[3]],
                $\bullet$S["id"["u2"],"clearance"[4]]},
   "Objects"$\to \{\bullet$O["sensitivity"[1]],$\bullet$O["sensitivity"[4]]}}]

Feel free to download the notebook ABAC.nb from

staff.fmi.uvt.ro/~mircea.marin/rholog/ABAC.nb

which contains the implementation of our tool, together with some illustrated examples.

3 A state transition system for ABAC_α

A system with an initial configuration cId is a state transition system: states are triples $\{U,S,O\}$ consisting of the users ($U$), subjects ($S$), and objects ($O$) that exist at that moment in the system and are compatible with the specifications of cId and its configuration type (stored in CfgType[cId]); and transitions correspond to the operations from the functional specification of ABAC_α. The state components $U$, $S$, $O$ are assumed to be multisets because the entities of ABAC are identity-less: their behavior is uniquely determined by the values of their attributes. For this reason, different entities may assume the same term representation in our framework.

We take for granted the functional specification of ABAC_α given in [AS17]. It consists of six operations:

subject creation:

user $u\in U$ can create a new subject $s$ if formula $\mathrm{𝙲𝚘𝚗𝚜𝚝𝚛𝚂}[u,s]$ holds. This formula belongs to the instance of the common policy language (CPL) that makes use of the attribute values of $u$ and $s$.

subject deletion:

$u\in U$ is free to delete any subject $s\in S$ it created before, that is, a subject $s$ for which $\mathrm{𝚄𝙸𝚍}[u]=\mathrm{𝚄𝙸𝚍}[s]$.

object creation:

$s\in S$ can create a new object $o$ if boolean formula $\mathrm{𝙲𝚘𝚗𝚜𝚝𝚛𝙾}[s,o]$ holds. This formula belongs to the instance of CPL that uses the attribute values of entities $s$ and $o$.

subject modification:

$u\in U$ can change a subject $s\in S$ into $s^{\prime }$ if $\mathrm{𝚄𝙸𝚍}[u]=\mathrm{𝚄𝙸𝚍}[s]=\mathrm{𝚄𝙸𝚍}[s^{\prime }]$ and $\mathrm{𝙲𝚘𝚗𝚜𝚝𝚛𝙼𝚘𝚍𝚂}[u,s,s^{\prime }]$ holds. This formula belongs to the instance of CPL that uses the attribute values of $u$, $s$, and $s^{\prime }$.

object modification:

$s\in S$ can change $o\in O$ into $o^{\prime }$ if $\mathrm{𝙲𝚘𝚗𝚜𝚝𝚛𝙼𝚘𝚍𝙾}[s,o,o^{\prime }]$ holds. This formula belongs to the instance of CPL that uses the attribute values of $s$, $o$, and $o^{\prime }$.

authorized access:

$s\in S$ can exercise a permission $p\in P$ on $o\in O$ if $\mathrm{𝙰𝚞𝚝𝚑}[p,s,o]$ holds. $P$ is a finite set of permission IDs (strings) and, for every $p\in P$, formula $\mathrm{𝙰𝚞𝚝𝚑}[p,s,o]$ is from the instance of CPL that uses the attribute values of $s$ and $o$.

3.1 Configuration-specific rules

CPL [Jin14] is the common policy language part for the languages used to express the boolean formulas that constrain the operations of the functional specification of ABAC_α. CPL describes a fragment of first-order logic where quantified formulas must be of the form $\exists x\in \mathrm{𝑠𝑒𝑡}.\phi$ or $\forall x\in \mathrm{𝑠𝑒𝑡}.\phi$ with $set$ a finite set of values. The host language of RhoLog is Mathematica, which is rich enough to express and decide the quantifier-free constraints of CPL. Moreover, we can eliminate all variable occurrences by repeated applications of the following reductions:

$\exists x\in \mathrm{𝑠𝑒𝑡}.\phi ={\displaystyle \underset{v\in \mathrm{𝑠𝑒𝑡}}{\bigvee }}\phi [x\mapsto v]\forall x\in \mathrm{𝑠𝑒𝑡}.\phi ={\displaystyle \underset{v\in \mathrm{𝑠𝑒𝑡}}{\bigwedge }}\phi [x\mapsto v]$

Every configuration type typeId has its own formulas that constrain the functionality of ABAC_α. These formulas are expressed in instances of CPL. Therefore, we can write rule-based definitions of these conditions, which are specific to every typeId:

typeId::{$\bullet$U[…],$\bullet$S[…]} $\Leftarrow {\phi }_1$
typeId::{$\bullet$S[…],$\bullet$O[…]} $\Leftarrow {\phi }_2$
typeId::{$\bullet$U[…],$\bullet$S[…],$\bullet$S[…]} $\Leftarrow {\phi }_3$
typeId::{$\bullet$S[…],$\bullet$O[…],$\bullet$O[…]} $\Leftarrow {\phi }_4$
typeId::Auth[$p_1,\bullet 𝚂[\mathrm{\dots }],\bullet 𝙾[\mathrm{\dots }]$] $\Leftarrow {\phi }_{5,1}$
$\mathrm{\dots }$
typeId::Auth[$p_r,\bullet 𝚂[\mathrm{\dots }],\bullet 𝙾[\mathrm{\dots }]$] $\Leftarrow {\phi }_{5,r}$.

where ${\phi }_1,{\phi }_2,{\phi }_3,{\phi }_4,{\phi }_{5,1}$, …, ${\phi }_{5,r}$ are formulas expressed in CPL.

3.2 Auxiliary functions and strategies

Subject and object creation are nondeterministic operations: they can be implemented by guessing the entity, and then creating it if the condition described by the corresponding CPL-formula holds. This process can be implemented in two steps. First, we define the functions sSeed[cId] which yields

$\bullet$S[$sA{t}_1[\mathrm{SCOPE}(sA{t}_1),{\tau }_1],\mathrm{\dots },sA{t}_n[\mathrm{SCOPE}(sA{t}_n),{\tau }_n]$]

and oSeed[cId] which yields the term

$\bullet$O[$oA{t}_1[\mathrm{SCOPE}(oA{t}_1),{\tau }_1],\mathrm{\dots },oA{t}_n[\mathrm{SCOPE}(oA{t}_p),{\tau }_p]$]

For example, sSeed["Cfg-01"] yields

$\bullet$S["id"[{"u1","u2","u3"},"Elem"]]

and oSeed["Cfg-01"] yields the term

$\bullet$O["id"[$S$,"Elem"],"r"[$S$,"Subset"],"w"[$S$,"Subset"]]

where $S$ is {"u1","u2","u3"}.

Next, we use these terms as seeds to produce any subject (resp. object) that may be created. In rule-based thinking, an entity $E[a{t}_1[v_1],\mathrm{\dots },a{t}_k[v_k]]$ can be produced from the seed term $E[a{t}_1[scop{e}_1,{\tau }_1],\mathrm{\dots },a{t}_k[scop{e}_k,{\tau }_k]]$ if and only if the reducibility formulas $scop{e}_i{\to }_{{\tau }_i}{v}_i$ hold. Incidentally, the attribute type identifiers , are also built-in atomic strategies of $\rho$Log which guarantee the correctness of this rule-based thinking. Its implementation in $\rho$Log is straightforward: If we define the strategy "setAt" with

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 holds. Continuing this line of reasoning, we can argue that:

• user u can create new subject s iff holds, where the strategy "createS"[cId] is defined by the rule

• subject s can modify its attribute values and become sN iff its user creator u is in set U of existing users and is capable to change s to sN. We express this as the validity of the reducibility formula , where this strategy is defined by the rule

  
    
    
    $(\mathrm{𝙲𝚏𝚐𝚃𝚢𝚙𝚎}[{\mathrm{𝚌𝙸𝚍}}^{𝚒}]::\{{𝚞}^{𝚒},{𝚜}^{𝚒},{\mathrm{𝚜𝙽}}^{𝚒}\}))$
  

• if the creator of s is an existing user, then the admissible changes of s into sN are defined by the rule

  
             
             $(\mathrm{𝙲𝚏𝚐𝚃𝚢𝚙𝚎}[{\mathrm{𝚌𝙸𝚍}}^{𝚒}]::\{{𝚞}^{𝚒},{𝚜}^{𝚒},{\mathrm{𝚜𝙽}}^{𝚒}\})$
  

• subject s can change the attributes of object o to become object oN iff holds, where

3.3 The transition system

Except for authorized access, the other five operations from the functional specification of ABAC_α determine state transitions in its model. Their rule-based specifications are:

    

    $(\mathrm{𝚄𝙸𝚍}[{𝚞}^{𝚒}]===\mathrm{𝚄𝙸𝚍}[{𝚜}^{𝚒}]))$

   

    

    

In the state transitions defined by these rules, the entity matched by ${𝚜}^{𝚒}$ is the selected subject, and the one matched by ${𝚘}^{𝚒}$ is the selected object. Subjects may be created, and selected subjects are deleted or modified. Objects may be created, and selected objects are modified. To keep track of the attribute values of a subject or object in a particular state, we define its descendant with respect to a sequence $\mathrm{\Pi }$ of state transitions.

Suppose $\{U,S,O\}$ is a state for a configuration identified by cId, and $s\in S,o\in O$. Also, let $\pi :\{U,S,O\}{\to }_{\mathrm{𝑠𝑡𝑔𝐼𝑑}[\text{cId}]}\{U,S^{\prime },O^{\prime }\}$ be a state transition step. The descendants $des{c}_{\pi }(s)$ and $des{c}_{\pi }(o)$ of $s$ and $o$ with respect to $\pi$ are defined as follows:

• $des{c}_{\pi }(s):=\perp$ if and the selected subject from $S$ is $s$

• $des{c}_{\pi }(s):=s^{\prime }$ if

• $des{c}_{\pi }(o):=o^{\prime }$ if

• In the unspecified situations we have $des{c}_{\pi }(e):=e.$

Let $\mathrm{\Pi }:\{U,S,O\}{\to }^{\ast }\{U,S^{\prime },O^{\prime }\}$ be a sequence of $n\ge 0$ transition steps and $s\in S$, $o\in O$. If $n=0$ then $des{c}_{\mathrm{\Pi }}(s):=s$ and $des{c}_{\mathrm{\Pi }}(o):=o$. Otherwise, let $\pi$ be the first transition step of $\mathrm{\Pi }$, and ${\mathrm{\Pi }}^{\prime }$ the sequence of remaining transition steps. In this case $des{c}_{\mathrm{\Pi }}(o):=des{c}_{{\mathrm{\Pi }}^{\prime }}(des{c}_{\pi }(o))$ and

More generally, we define the set of descendants of $e\in S\cup O$ from a state $\mathrm{\Sigma }:=\{U,S,O\}$ as follows:
$Des{c}^{\mathrm{\Sigma }}(e):=\{e^{\prime }\mid \begin{array}{c}{e}^{\prime }\ne \perp \text{ and }{e}^{\prime }=des{c}_{\mathrm{\Pi }}(e)\text{ for some sequence }\mathrm{\Pi }\text{ of state transitions starting with }\mathrm{\Sigma }\}.\hfill \end{array}$

4 Safety of ABAC_α

The safety problem for configurations of ABAC_α is:

Given

a state $\{U,S,O\}$ for an ABAC_α configuration identified by cId, entities $s\in S$, $o\in O$, and a permission $p\in P$,

Decide

if there exists a sequence of state transitions
$\mathrm{\Pi }:\{U,S,O\}{\to }_{{\mathrm{𝑠𝑡𝑔}}_1}\{U,S_1,O_1\}\mathrm{\dots }{\to }_{{\mathrm{𝑠𝑡𝑔}}_n}\{U,S_n,O_n\}$
abbreviated $\mathrm{\Pi }:\{U,S,O\}{\to }^{\ast }\{U,S_n,O_n\}$, such that $des{c}_{\mathrm{\Pi }}(s)\ne \perp$ and the reducibility formula CfgType[cId]::Auth[$p,des{c}_{\mathrm{\Pi }}(s),des{c}_{\mathrm{\Pi }}(o)$] holds.

We start by pointing out a few properties of ABAC_α that allow us to make some simplifying assumptions.

The five kinds of transitions are influenced only by the selected entities, at most two, and affect only one entity; the other entities of the system state are not affected. In particular:

1. Objects can only participate at changing their own attributes. Since the presence of objects from $O-\{o\}$ plays no role in deciding whether $\mathrm{𝙰𝚞𝚝𝚑}[p,des{c}_{\mathrm{\Pi }}(s),des{c}_{\mathrm{\Pi }}(o)]$ holds for some $\mathrm{\Pi }$, it is harmless to assume that the initial state is $\{U,S,\{o\})$ and $\mathrm{\Pi }$ has no object creation steps.

2. If $\{U,S,O\}{\to }_{\mathrm{𝑠𝑡𝑔}}\{U,S^{\prime },O^{\prime }\}$ then $\{U,S\cup S^{\prime \prime },O^{\prime }\}{\to }_{\mathrm{𝑠𝑡𝑔}}\{U,S\cup S^{\prime \prime },O^{\prime }\}$ holds too, because we can choose the same participating entities to perform the transition. Therefore, it is harmless to assume that $\mathrm{\Pi }$ has no subject deletion steps.

Thus, it is harmless to assume that (1) $\mathrm{\Pi }$ has no transition steps of the strategies "deleteSubj"[cId] and "createObj"[cId], and (2) the given state is of the form $\{U,S,\{o\}\}$.

From now on we assume that $\mathrm{\Sigma }:=\{U,S,\{o\}\}$ is a state for an ABAC_α configuration identified by cId, and that $s\in S$ and $p\in P$.

Theorem 4.1

Let $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ and $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$. There exists a derivation $\mathrm{\Pi }:\mathrm{\Sigma }{\to }^{\ast }\{U,S^{\prime },\{o^{\prime }\}\}$ such that $s^{\prime }=des{c}_{\mathrm{\Pi }}(s)$.

Proof

Let $u$ be the creator of $s$. $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$ implies the existence of ${\mathrm{\Pi }}_1:\mathrm{\Sigma }{\to }^{\ast }\{U,S^{\prime \prime },\{o^{\prime }\}\}.$ If $s^{\prime }\in S^{\prime \prime }$ then the lemma holds for $\mathrm{\Pi }={\mathrm{\Pi }}_1$. Note that, if $u\notin U$, then $s$ can not change its attribute values, thus $Des{c}^{\mathrm{\Sigma }}(s)=\{s\}\subseteq S^{\prime \prime }$ and the lemma holds for $\mathrm{\Pi }={\mathrm{\Pi }}_1$.

The only case left to analyse is when $u\in U$ and $s^{\prime }\notin S^{\prime \prime }.$ In this case, there exists a derivation $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ implies the existence of a derivation . By concatenating these two derivations we obtain

Therefore, if $s_0\notin S^{\prime \prime }$ then ${\mathrm{\Pi }}_1$ can be extended as follows:

Otherwise, $S^{\prime \prime }=\{s_0\}\uplus S^{\prime \prime \prime }$ and ${\mathrm{\Pi }}_1$ can be extended as follows:

Theorem 1

There is a derivation $\mathrm{\Pi }:\mathrm{\Sigma }{\to }^{\ast }\{U,S^{\prime },\{o^{\prime }\}\}$ such that $des{c}_{\mathrm{\Pi }}(s)\ne \perp$ and CFGType[cId]::Auth[$p,des{c}_{\mathrm{\Pi }}(s),o^{\prime }$] holds if and only if CFGType[cId]::Auth[$p,s^{\prime },o^{\prime }$] holds for some $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ and $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$.

Proof

If $\mathrm{\Pi }$ exists then $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$ and we can choose the subject $s^{\prime }:=des{c}_{\mathrm{\Pi }}(s)\in Des{c}^{\mathrm{\Sigma }}(s)$ such that CfgType[cId]::Auth[$p,s^{\prime },o^{\prime }$] holds.

Conversely, if CfgType[cId]::Auth[$p,s^{\prime },o^{\prime }$] holds for $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ and $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$ then, by Lemma 4.1, there exists a derivation $\mathrm{\Pi }:\mathrm{\Sigma }{\to }^{\ast }\{U,S^{\prime },\{o^{\prime }\}\}$ such that $s^{\prime }=desc{s}_{\mathrm{\Pi }}(s).$ Therefore, CfgType[cId]::Auth[$p,des{c}_{\mathrm{\Pi }}(s),o^{\prime }$] holds too.

According to Theorem 1, we can proceed in two steps:

1. look at all possible descendants $s^{\prime }$ of $s$; decide UNSAFE if any of them gets permission $p$ on $o$, otherwise compute $Des{c}^{\mathrm{\Sigma }}(s)$,

2. look at all possible descendants $o^{\prime }$ of $o$; decide UNSAFE if any $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ can exercise permission $p$ on some $o^{\prime }$, otherwise decide SAFE.

It remains to figure out how to compute $Des{c}^{\mathrm{\Sigma }}(s)$ and $Des{c}^{\mathrm{\Sigma }}(o)$, and how to check if Auth[$p,s^{\prime },o^{\prime }$]${\to }_{\text{CfgType[}\text{cId}\text{]}}\mathrm{𝚃𝚛𝚞𝚎}$ holds for some $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ and $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$. For this purpose, we define three strategies: For this purpose, we define three strategies:

If $S^{\prime },S^{\prime \prime }$ are sets of subjects and $O^{\prime },O^{\prime \prime }$ are sets of objects, then:
1) ApplyStg["auth?"[$p$,CfgType[cId]],$\{S^{\prime },O^{\prime }\}$] returns True iff some $s^{\prime }\in S^{\prime }$ can exercise permission $p$ on some $o^{\prime }\in O^{\prime }$.
2) ApplyStgList["newModS"[cId,$S^{\prime \prime }$], $S^{\prime }$] returns all descendants of elements from $S^{\prime }$ which are not in $S^{\prime \prime }$.
3) ApplyStgList["newModO"[cId,$O^{\prime \prime }$], $\{S^{\prime },O^{\prime }\}$] returns all descendants of elements from $O^{\prime }$ produced by some subject from $S^{\prime }$, which are not in $O^{\prime \prime }$.

Step 1

In this step we accumulate the value of $Des{c}^{\mathrm{\Sigma }}(s)$ in a variable sDESC while checking if some $s^{\prime }\in \mathrm{𝚜𝙳𝙴𝚂𝙲}$ has the authority to exercise permission $p$ on $o$. If the creator of $s$ is not a user in the given configuration then the only descendant of $s$ is $s$, and we only have to check if Auth[$p,s,o$]${\to }_{\mathrm{𝙲𝚏𝚐𝚃𝚢𝚙𝚎}\text{[}\text{cId}\text{]}}$True holds or not. If yes, we decide UNSAFE, otherwise we set $\mathrm{𝚜𝙳𝙴𝚂𝙲}:=\{s\}$.

Otherwise, the creator of $s$ is in $U$ and $Des{c}^{\mathrm{\Sigma }}(s)={\bigcup }_{k=0}^{\mathrm{\infty }}{S}_k$ where $S_1:=\{s\}$ and

Based on this observation, we can interleave the incremental accumulation in sDESC of the elements of $S_k$ with the detection of unsafety when $\mathrm{𝙰𝚞𝚝𝚑}[p,s^{\prime },o]$ holds for some $s^{\prime }\in S_k$:
Note that, before entering the $k$-th loop of while, the values of sDESC and sN are ${\bigcup }_{i=1}^k{S}_i$ and $S_{k+1}$. The while loop will terminate because sDESC is finite, therefore $S_n=\mathrm{\varnothing }$ for some $n\in \mathbb{N}.$

Step 2

In this step we accumulate the descendants of $o$ in a variable oDESC and report UNSAFE as soon as we detect the truth of the formula

"auth?"[p,CfgType[cId]]::{sDESC,oDESC}

First, we must figure out how to compute oDESC. The only subjects which may change the attribute values of (descendants) of $o$ from $\mathrm{\Sigma }$ are those from where sNew is the set of subjects that may be created by users from $U$. $\mathrm{𝚜𝙰𝙻𝙻}$ can be computed incrementally as follows:

;
$\mathrm{𝚜𝙰𝙻𝙻}:=\mathrm{\varnothing }$; $\mathrm{𝚜𝙽}:=S\cup \mathrm{𝚜𝙽𝚎𝚠}$;
wh	ile $\mathrm{𝚜𝙽}\ne \mathrm{\varnothing }$ do
	$\mathrm{𝚜𝙰𝙻𝙻}:=\mathrm{𝚜𝙰𝙻𝙻}\cup \mathrm{𝚜𝙽}$;
	$\mathrm{𝚜𝙽}:=\mathrm{𝙰𝚙}$	AplyStgList["newModS"[cId,sALL],sN];

In every loop of while we compute the elements of a nonempty subset $\mathrm{𝚜𝙽}\subseteq {\bigcup }_{S\cup \mathrm{𝚜𝙽𝚎𝚠}}Des{c}^{\mathrm{\Sigma }}(s)$ which are not yet accumulated in sDESC, and accumulate them in sDESC. The loop will terminate because the set ${\bigcup }_{S\cup \mathrm{𝚜𝙽𝚎𝚠}}Des{c}^{\mathrm{\Sigma }}(s)$ is finite.

It is easy to see that $Des{c}^{\mathrm{\Sigma }}(o)$ coincides with ${\bigcup }_{k=1}^{\mathrm{\infty }}{O}_k$ where $O_0:=\{o\}$ and

Based on this observation, we can iterate the computation of $O_k$ together with the test if Auth$[p,s^{\prime },o^{\prime }]$ holds for some $s^{\prime }\in \mathrm{𝚜𝙳𝙴𝚂𝙲}$ and $o^{\prime }\in O_k.$ This iterative process stops when we reach a $k$ with $O_k=\mathrm{\varnothing }$, and this will eventually happen because $Des{c}^{\mathrm{\Sigma }}(o)$ is finite.

The final algorithm

By putting together the rule-based algorithms for steps 1 and 2, we obtain the algorithm illustrated in Figure 1.

Figure 1: The safety check algorithm for ABAC_α.

5 Conclusions

We proved that the safety problem of ABAC_α can be reduced to checking if $\mathrm{𝙰𝚞𝚝𝚑}[p,s^{\prime },o^{\prime }]$ holds for some $s^{\prime }\in Des{c}^{\mathrm{\Sigma }}(s)$ and $o^{\prime }\in Des{c}^{\mathrm{\Sigma }}(o)$, and solved it by identifying a rule-based algorithm that interleaves the detection of unsafety with the incremental computation of $Des{c}^{\mathrm{\Sigma }}(s)$ and $Des{c}^{\mathrm{\Sigma }}(o)$.

Our algorithm is parametric with respect to the configuration types of ABAC_α. Therefore, whenever we want to check that, for a given configuration, a subject $s$ never gets authorization to exercise permission $p$ on an object $o$, it is enough to do the following: (1) specify the configuration and its type, and (2) call the method

CheckSafety[cId,$s,o,p$]

which runs our safety check algorithm. It returns SAFE if $s$ never gets authorization to exercise permission $p$ on $o$, and UNSAFE otherwise.