<<RhoLog`

(Subscript[ABAC, α])

Clear[DeclareCfgType];
(* Cfg[cfgType]: UA/SA/OA/Scope *)
DeclareCfgType[cfgType_String,rs:{__Rule}]:=Module[{specs=Map[First,rs]},
If[!SubsetQ[specs,{"UA","SA","OA","Scope"}],
Return["Some configuration options are missing.\n"<>
"They should include:\"UA\",\"SA\",\"OA\",\"Scope\"."]];
If[!MemberQ[rs,"UA"->{___String}],
Return["Ill-formed specification of \"UA\" option"]];
If[!MemberQ[rs,"SA"->{___String}],
Return["Ill-formed specification of \"OA\" option"]];
If[!MemberQ[rs,"OA"->{___String}],
Return["Ill-formed specification of \"UA\" option"]];
If[!MemberQ[rs,"Scope"->{Repeated[_String->•[_String,"Elem"|"Subset"]]}],
Return["Ill-formed specification of \"Scope\" option"]];
Cfg[cfgType]=rs;
cfgType];

Clear[DeclareConfiguration];
(* Cfg[cfgId]: Users/Range/Subjects/Objects/CfgType *)
DeclareConfiguration[cfgId_String,rs:{__Rule}]:=Module[{specs=Map[First,rs],cfgType},
If[!SubsetQ[specs,{"Users","Range","Subjects","Objects","CfgType"}],
Return["Some configuration options are missing.\n"<>
"They should include:\"Users\",\"Range\",\"Subjects\",\"Objects\",\"CfgType\"."]];
If[!MemberQ[rs,"Users"->{Repeated[(_->•U["id"[_],___])?(#[[1]]==#[[2,1,1]]&)]}],
Return["Ill-formed specification of \"Users\" option"]];
If[!MemberQ[rs,"Range"->{"UId"->{___String},___}],
Return["Ill-formed specification of \"Range\" option"]];
If[!MemberQ[rs,"CfgType"->_String],
Return["Ill-formed specification of \"CfgType\" option"]];
cfgType=Replace["CfgType",rs];
If[!ListQ[Cfg[cfgType]],
Return["Undefined configuration type \""<>cfgType<>"\""]];
If[!MemberQ[rs,"Subjects"->{___•S}],
Return["Ill-formed specification of \"Subjects\" option"]];
If[!MemberQ[rs,"Objects"->{___•O}],
Return["Ill-formed specification of \"Objects\" option"]];
Cfg[cfgId]=rs;
Users[cfgId]=Last/@Replace["Users",rs];
Subjects[cfgId]=Replace["Subjects",rs];
Objects[cfgId]=Replace["Objects",rs];
CfgType[cfgId]=cfgType;
cfgId];

Clear[UId,User,Users];
UId[e:(_•U|_•S)]:=e[[1,1]];
User[cfgId_String,uId_String]:=Replace[uId,Replace["Users",Cfg[cfgId]]]

Clear[sSeed];
sSeed[cfgId_]:=Module[{rs=Cfg[CfgType[cfgId]]},
(Inner[Apply,#,#/.Replace["Scope",rs],•S]&@(Replace["SA",rs]))/.Replace["Range",Cfg[cfgId]]];

Clear[oSeed];
oSeed[cfgId_]:=Module[{rs=Cfg[CfgType[cfgId]]},
(Inner[Apply,#,#/.Replace["Scope",rs],•O]&@(Replace["OA",rs]))/.Replace["Range",Cfg[cfgId]]];

Auxiliary rules

DeclareRule[(attr^f)[(S^i),(stg^i)](Subscript[->, "setAttr"])(attr^f)[(v^i)]⟸((S^i)(Subscript[->, (stg^i)])(v^i))]

Rules of (Subscript[ABAC, α])

(* u ∈ Users[cId], s added to Subjects[cId];
relevant rule for safety analysis *)
DeclareRule[(u^i)/;(Head[u]===•U)(Subscript[->, "createS"[(cId^i)]])(s^i)⟸((sSeed[(cId^i)](Subscript[->, "Fmap"["setAttr"]])(s^i))&&(UId[(u^i)]===UId[(s^i)])&&CfgType[(cId^i)]∷{(u^i),(s^i)})]

(* s ∈ Subjects[cId], o added to Objects[cId]; 
irrelevant rule for safety analysis *)
DeclareRule[(s^i)/;(Head[s]===•S)(Subscript[->, "createO"[(cId^i)]])(o^i)⟸((oSeed[(cId^i)](Subscript[->, "Fmap"["setAttr"]])(o^i))&&(CfgType[(cId^i)]∷{(s^i),(o^i)}))]

(* s1 ∈ Subjects[cId], s2: modified version of s1;
relevant rule for safety analysis *)
DeclareRule[{(U^i),(s^i)}(Subscript[->, "modSA"[(cId^i)]])(sN^i)⟸((User[cId,UId[(s^i)]]≡(u^i))&&MemberQ[(U^i),(u^i)]&&(sSeed[(cId^i)](Subscript[->, "Fmap"["setAttr"]])(sN^i))&&(UId[(s^i)]===UId[(sN^i)])&&CfgType[(cId^i)]∷{(u^i),(s^i),(sN^i)})]

(* s ∈ Subjects[cId], o ∈ Objects[cId]; oN: modified version of o;
relevant rule for safety analysis *)
DeclareRule[{(s^i),(o^i)}(Subscript[->, "modOA"[(cId^i)]])(oN^i)⟸((oSeed[(cId^i)](Subscript[->, "fMap"["setAttr"]])(oN^i))&&(ConstrModO[s,o,oN](Subscript[->, CfgType[cId]])True))]

(* Transition rules *)
DeclareRules[{{(a^s),(u^i),(b^s)},(S^i),(O^i)}(Subscript[->, "createSubj"[(cId^i)]]){{(a^s),(u^i),(b^s)},Prepend[(S^i),(s^i)],(O^i)}⟸(((u^i)(Subscript[->, "createS"[(cId^i)]])(s^i))&&Not[MemberQ[(S^i),(s^i)]]),
{{(a^s),(u^i),(b^s)},{(x^s),(s^i),(y^s)},(O^i)}(Subscript[->, "deleteSubj"[(cId^i)]]){{(a^s),(u^i),(b^s)},{(x^s),(y^s)},(O^i)}⟸(UId[(u^i)]===UId[(s^i)]),
{(U^i),{(a^s),(s^i),(b^s)},(O^i)}(Subscript[->, "createObj"[(cId^i)]]){(U^i),{(a^s),(s^i),(b^s)},Prepend[(O^i),(o^i)]}⟸(((s^i)(Subscript[->, "createO"[(cId^i)]])(o^i))&&Not[MemberQ[(O^i),(o^i)]]),
{(U^i),{(a^s),(s^i),(b^s)},(O^i)}(Subscript[->, "modifySubj"[(cId^i)]]){(U^i),{(a^s),(sN^i),(b^s)},(O^i)}⟸({(U^i),(s^i)}(Subscript[->, "modSA"[(cId^i)]])(sN^i)),
{(U^i),{(a^s),(s^i),(b^s)},{(x^s),(o^i),(y^s)}}(Subscript[->, "modifyObj"[(cId^i)]]){(U^i),{(a^s),(s^i),(b^s)},{(x^s),(oN^i),(y^s)}}⟸({(s^i),(o^i)}(Subscript[->, "modOA"[(cId^i)]])(oN^i))]

Rules to check safety of (Subscript[ABAC, α])

DeclareRules[
"auth?"[(p^i),(ct^i)]∷{{((_)^s),(s^i),((_)^s)},{((_)^s),(o^i),((_)^s)}}⟸((ct^i)∷Auth[(p^i),(s^i),(o^i)]),
{((_)^s),(s^i),((_)^s)}(Subscript[->, "newModS"[(c^i),(U^i),(S^i)]])(sN^i)⟸(({(U^i),(s^i)}(Subscript[->, "modSA"[(c^i)]])(sN^i))&&Not[MemberQ[(S^i),(sN^i)]]),
{{((_)^s),(s^i),((_)^s)},{((_)^s),(o^i),((_)^s)}}(Subscript[->, "newModO"[(c^i),(O^i)]])(oN^i)⟸(({(s^i),(o^i)}(Subscript[->, "modOA"[(c^i)]])(oN^i))&&Not[MemberQ[(O^i),(oN^i)]])]

Safety queries

Clear[CheckSafety];
CheckSafety[cId_,s_,o_,p_]:=
Module[{ct=CfgType[cId],U,S,sDESC,sN,sNew,sALL,oDESC,oN},
U=Users[cId];S=Subjects[cId];
If[ApplyStg["auth?"[p,ct],{{s},{o}}]===True,
Return["UNSAFE"]];
(* Start accumulating the descendants of s in sDESC *)
sDESC={};sN={};
If[MemberQ[U,User[cId,UId[s]]],
sN=ApplyStgList["newModS"[cId,U,sDESC],{s}]];
While[sN=!={},
If[ApplyStg["auth?"[p,ct],{sN,{o}}]===True,
Return["UNSAFE"]];
sDESC=Join[sDESC,sN];
sN=ApplyStgList["newModS"[cId,U,sDESC],sN]];
sNew=Apply[Join,Map[ApplyStgList["createS"[cId],#]&,U]];
sALL={};
(* Accumulate in sALL all elements which may change the attributes of o *)
sN=Union[S,sNew];
While[sN=!={},
sALL=Join[sALL,sN];
sN=ApplyStgList["newModS"[cId,U,sALL],sN]];
oDESC={};oN={o};
While[oN=!={},
If[ApplyStg["auth?"[p,ct],{sDESC,oN}]===True,
Return["UNSAFE"]];
oDESC=Join[oDESC,oN];
oN=ApplyStgList["newModO"[cId,oDESC],{sALL,oN}]];
Return["SAFE"]];

Rule-based characterisations of various configurations of (Subscript[ABAC, α])

Discretionary access control model (DAC)

(* UA/SA/OA/Scope*)
DeclareCfgType["DAC",{
"UA"->{"id"},
"SA"->{"id"},
"OA"->{"id","r","w"},
"Scope"->{
"id"->•["UId","Elem"],
"r"->•["UId","Subset"],
"w"->•["UId","Subset"]}}]

(* CfgType/Users/Range/Subjects/Objects *)
DeclareConfiguration["DAC-Cfg01",{
"CfgType"->"DAC",
"Users"->{
"u1"->•U["id"["u1"]],
"u2"->•U["id"["u2"]],
"u3"->•U["id"["u3"]]},
"Range"->{"UId"->{"u1","u2","u3"}},
"Subjects"->{•S["id"["u1"]],•S["id"["u2"]]},
"Objects"->{
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u1","u2"}]],
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u3","u2"}]]}}]

(* CfgType/Users/Range/Subjects/Objects *)
DeclareConfiguration["DAC-Cfg02",{
"CfgType"->"DAC",
"Users"->{
"u2"->•U["id"["u2"]],
"u3"->•U["id"["u3"]]},
"Range"->{"UId"->{"u1","u2","u3"}},
"Subjects"->{•S["id"["u2"]]},
"Objects"->{
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u1","u2"}]],
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u3","u2"}]]}}]

DeclareRules[
(* "DAC"∷Auth[p,s,o] *)
"DAC"∷Auth["read",•S["id"[(x^i)]],•O[((_)^i),"r"[(R^i)],((_)^i)]]⟸MemberQ[(R^i),(x^i)],
"DAC"∷Auth["write",•S["id"[(x^i)]],•O[((_)^i),((_)^i),"w"[(W^i)]]]⟸MemberQ[(W^i),(x^i)],
(* "DAC"∷{u,s} *)
"DAC"∷{•U[((_)^s)],•S[((_)^s)]},
(* "DAC"∷{u,s,s'} *)
"DAC"∷{•U[((_)^s)],•S[((_)^s)],•S[((_)^s)]},
(* "DAC"∷{s,o} *)
"DAC"∷{•S[(x^i)],•O[(x^i),((_)^s)]},
(* "DAC"∷{s,o,o'} *)
"DAC"∷{•S[(x^i)],•O[(x^i),((_)^s)],•O[(x^i),((_)^s)]}]

Mandatory access control model (MAC)

(* UA/SA/OA/Scope*)
DeclareCfgType["MAC",{
"UA"->{"id","clearance"},
"SA"->{"id","clearance"},
"OA"->{"sensitivity"},
"Scope"->{
"id"->•["UId","Elem"],
"clearance"->•["level","Elem"],
"sensitivity"->•["level","Elem"]}}]

(* CfgType/Users/Range/Subjects/Objects *)
DeclareConfiguration["MAC-Cfg01",{
"CfgType"->"MAC",
"Users"->{
"u1"->•U["id"["u1"],"clearance"[3]],
"u2"->•U["id"["u2"],"clearance"[4]]},
"Range"->{"UId"->{"u1","u2"},"level"->{1,2,3,4,5}},
"Subjects"->{
•S["id"["u1"],"clearance"[3]],
•S["id"["u2"],"clearance"[4]]},
"Objects"->{•O["sensitivity"[1]],•O["sensitivity"[4]]}}]

DeclareRules[
(* Auth[p,s,o] *)
"MAC"∷Auth["read",•S[((_)^i),"clearance"[(x^i)]],•O["sensitivity"[(y^i)]]]⟸((y^i)≤(x^i)),
"MAC"∷Auth["write",•S[((_)^i),"clearance"[(x^i)]],•O["sensitivity"[(y^i)]]]⟸((x^i)≤(y^i)),
(* "MAC"∷{u,s} *)
"MAC"∷{•U[(x^i),"clearance"[(y^i)]],•S[(x^i),"clearance"[(z^i)]]}⟸((z^i)≤(y^i)),
(* "MAC"∷{u,s,s'} and "MAC"∷{s,o,o'} — missing, thus False *)
(* "MAC"∷{s,o} *)
"MAC"∷{•S[((_)^i),"clearance"[(x^i)]],•O["sensitivity"[(y^i)]]}⟸((y^i)≤(x^i))
]

Role-based access control model (RBAC)

(* UA/SA/OA/Scope*)
Map[DeclareCfgType[#,{
"UA"->{"id","role"},
"SA"->{"id","role"},
"OA"->{"rrole","wrole"},
"Scope"->{
"id"->•["UId","Elem"],
"role"->•["roleId","Subset"],
"rrole"->•["roleId","Subset"],
"wrole"->•["roleId","Subset"]}}]&,{"RBAC0","RBAC1"}];

DeclareRules[
(* "RBAC0"∷Auth[p,s,o] *)
"RBAC0"∷Auth["read",•S[((_)^i),"role"[{((_)^s),(x^i),((_)^s)}]],•O["rrole"[{((_)^s),(x^i),((_)^s)}],((_)^i)]],
"RBAC0"∷Auth["write",•S[((_)^i),"role"[{((_)^s),(x^i),((_)^s)}]],•O[((_)^i),"wrole"[{((_)^s),(x^i),((_)^s)}]]],
(* "RBAC0"∷{u,s} *)
"RBAC0"∷{•U[(x^i),"role"[(S1^i)]],•S[(x^i),"role"[(S2^i)]]}⟸ SubsetQ[(S1^i),(S2^i)],
(* "RBAC0"∷{u,s,s'} *)
"RBAC0"∷{((_)^i),•S[((_)^i),"role"[(S1^i)]],•S[((_)^i),"role"[(S2^i)]]}⟸ SubsetQ[(S1^i),(S2^i)]
(* "RBAC0"∷{s,o} and "RBAC0"∷{s,o,o'} — missing, thus False *)
]

DeclareRules[
(* "RBAC1"∷Auth[p,s,o] *)
"RBAC1"∷Auth["read",•S[((_)^i),"role"[{((_)^s),(x^i),((_)^s)}]],•O["rrole"[{((_)^s),(y^i),((_)^s)}],((_)^s)]]⟸((y^i)≤(x^i)),
"RBAC1"∷Auth["write",•S[((_)^i),"role"[{((_)^s),(x^i),((_)^s)}]],•O[((_)^i),"wrole"[{((_)^s),(y^i),((_)^s)}]]]⟸((y^i)≤(x^i)),
(* "RBAC1"∷{u,s} *)
"RBAC1"∷{•U[(x^i),"role"[(S1^i)]],•S[(x^i),"role"[(S2^i)]]}⟸ SubsetQ[(S1^i),(S2^i)],
(* "RBAC1"∷{u,s,s'} *)
"RBAC1"∷{((_)^i),•S[((_)^i),"role"[(S1^i)]],•S[((_)^i),"role"[(S2^i)]]}⟸ SubsetQ[(S1^i),(S2^i)]
(* "RBAC1"∷{s,o} and "RBAC1"∷{s,o,o'} — missing, thus False *)
]

Tests

(* UNSAFE *)
CheckSafety[
"DAC-Cfg01",
•S["id"["u2"]],
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u1","u2"}]],
"read"]

(* SAFE *)
CheckSafety[
"DAC-Cfg02",
•S["id"["u2"]],
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u1","u2"}]],
"read"]

(* UNSAFE *)
CheckSafety[
"DAC-Cfg01",
•S["id"["u2"]],
•O["id"["u1"],"r"[{"u1","u3"}],"w"[{"u1","u2"}]],
"write"]

(* UNSAFE *)
CheckSafety[
"MAC-Cfg01",
•S["id"["u1"],"clearance"[3]],
•O["sensitivity"[1]],
"read"]

(* SAFE *)
CheckSafety[
"MAC-Cfg01",
•S["id"["u1"],"clearance"[3]],
•O["sensitivity"[1]],
"write"]

(* SAFE *)
CheckSafety[
"MAC-Cfg01",
•S["id"["u1"],"clearance"[3]],
•O["sensitivity"[4]],
"read"]