Constants used in the test cases

These constants were used as synonyms to abbreviate the description of each test case. They are considered global identifiers, denoting the string they identify.

All constants denote strings. The symbols appearing in the definition of a constant must have been defined beforehand (i.e., their types must have been indicated). Constants are global in relation with the entire document, that is, they can be used in every operation. At the same time, it is not possible to have two constants with the same identifier.

CONSTANT u (U), u₁ (U), u₂ (U), u₃ (U), u₄ (U), root (U), secofr (U): SUBJECT

CONSTANT p_o (U), p_o1 (U), p_o2 (U), p_o3 (U), / (U): OBJNAME

CONSTANT OBJECT

(U) o	::=	(po, File)
(U) o1	::=	(po1, File)
(U) o2	::=	(po2, File)
(U) o3	::=	(po3, File)
(U) barra	::=	(/, Directory)

CONSTANT g (U), g₁ (U), g₂ (U), g₃ (U), AG (U), RG (U), SAG (U): GRPNAME

CONSTANT GRPNAME -> (set SUBJECT)

(U) G	::=	{g1 :-> {u}, RG :-> {root}, \linebreak SAG :-> {secofr}, AG :-> {u, root, secofr}}

CONSTANT SUBJECT -> GRPNAME

(U) PG

::=

{u :-> g1, root :-> RG, secofr :-> SAG}

CONSTANT nat

(U) M	::=	3
(U) N	::=	5

CONSTANT ADMIN (U), NETWORK (U), NATO (U), NUCLEAR (U): CATEGORY

CONSTANT FBI (U), SECOFR (U), ROOT (U), CIA (U), MENEM (U): CATEGORY

CONSTANT (set CATEGORY)

CAT ::= {NATO, NUCLEAR, FBI}

CONSTANT SUBJECT*SecClass

(U) rSC	::=	root :-> [level := 0, categs := {ROOT}]
(U) soSC	::=	secofr :-> [level := 0, categs := {SECOFR}]
(U) uSC	::=	u :-> [level := N, categs := {FBI, NATO}]
(U) userSC	::=	user :-> [level := M, categs := {NATO}]

CONSTANT (set SUBJECT*SecClass)

(U) SSC	::=	{rSC, soSC, uSC, userSC}

CONSTANT OBJECT*SecClass

bSC ::= barra :-> [level := 0, categs := {}]

CONSTANT (set OBJECT*SecClass)

(U) OSC1	::=	{o1 :-> [level := M, categs := {FBI, NATO}], bSC}
(U) OSC	::=	{o :-> [level := M, categs := {FBI, NATO}], bSC}

CONSTANT AccessCtrlListData

(U) aclo	::=	[owner := u, group := g1, UserReaders := {u}, GroupReaders := {}, UserWriters := {u}, GroupWriters := {}, UserOwners := {u}, GroupOwners := {RG}]
(U) acl/	::=	[owner := root, group := RG, UserReaders := {root}, GroupReaders := {AG}, UserWriters := {root}, GroupWriters := {}, UserOwners := {root}, GroupOwners := {RG}]
(U) acl1	::=	[owner := u1, group := g1, UserReaders := {u}, GroupReaders := {}, UserWriters := {u}, GroupWriters := {}, UserOwners := {u1}, GroupOwners := {RG}]

CONSTANT (set OBJECT*AccessCtrlListData)

(U) ACL	::=	{o :-> aclo, barra :-> acl/}
(U) ACL1	::=	{o1 :-> aclo, barra :-> acl/}

CONSTANT x (U): BYTE

CONSTANT FILECONT

fc1 ::= < x >

CONSTANT (set OBJECT*FILECONT)

(U) F	::=	{o :-> fc1}
(U) F1	::=	{o1 :-> fc1}

CONSTANT (set OBJECT*DIRCONT)

(U) D	::=	{barra :-> < o.1 > }
(U) D1	::=	{barra :-> < o1.1 > }

CONSTANT ru (U), wu (U), pu (U): SUBJECT

CONSTANT rg (U), wg (U), pg (U): GRPNAME

CONSTANT GRPNAME -> (set SUBJECT)

(U) G3	::=	{g :-> {u}, g1 :-> {u1}, g2 :-> {u2}, g3 :-> {u3}, RG :-> {root}, SAG :-> {secofr}, AG :-> {u, u1, u2, u3, root, secofr}}

CONSTANT SUBJECT -> GRPNAME

(U) PG3	::=	{u :-> g, u1 :-> g1, u2 :-> g2, u3 :-> g3, root :-> RG, secofr :-> SAG}

CONSTANT (set OBJECT*ReadersWriters)

(U) SM2	::=	{o1 :-> [ActReaders := {u1}, ActWriters := {}], o2 :-> [ActReaders := {}, ActWriters := {u1}], o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}
(U) SM	::=	{o1 :-> [ActReaders := {u1}, ActWriters := {}]}
(U) SM3	::=	{o :-> [ActReaders := {u1}, ActWriters := {}], o2 :-> [ActReaders := {}, ActWriters := {u1}], o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}

CONSTANT (set OBJECT*SecClass)

(U) OSCSM	::=	{o :-> [level := N, categs := {FBI, NATO}], o1 :-> [level := N, categs := {FBI, NATO}], bSC}
(U) OSC2	::=	{o :-> [level := N, categs := {FBI, NATO}], o1 :-> [level := N, categs := {FBI, NATO}], o2 :-> [level := N, categs := {FBI, NATO}], o3 \ bSC}
(U) OSC3	::=	{o1 :-> [level := N, categs := {FBI, NATO}], o2 :-> [level := N, categs := {FBI, NATO}], o3 \ bSC}

CONSTANT OBJECT*AccessCtrlListData

(U) aclo1	::= [owner := u1, group := g1, UserReaders := {u1}, GroupReaders := {AG}, UserWriters := {u}, GroupWriters := {}, UserOwners := {u1}, GroupOwners := {RG}]
(U) aclo2	::= [owner := u2, group := g2, UserReaders := {u2}, GroupReaders := {AG}, UserWriters := {u1}, GroupWriters := {}, UserOwners := {u2}, GroupOwners := {RG}]
(U) aclo3	::= [owner := u3, group := g3, UserReaders := {u1}, GroupReaders := {AG}, UserWriters := {u}, GroupWriters := {AG}, UserOwners := {u3}, GroupOwners := {RG}]

CONSTANT (set SUBJECT*SecClass)

(U) SSC2

::=

{u :-> [level := N, categs := {FBI, NATO}], u1 :-> [level := N, categs := {FBI, NATO}], u2 :-> [level := N, categs := {FBI, NATO}], u3 :-> [level := N, categs := {FBI, NATO}], rSC, soSC}

CONSTANT (set OBJECT*FILECONT)

(U) F2	::=	{o :-> fc1, o1 :-> fc1, o2 :-> fc1, o3 :-> fc1, }
(U) F3	::=	{o1 :-> fc1, o2 :-> fc1, o3 :-> fc1, }

CONSTANT (set OBJECT*DIRCONT)

(U) D2	::=	{barra :-> < o.1, o1.1, o2.1, o3.1> }
(U) D3	::=	{barra :-> < o1.1, o2.1, o3.1> }

CONSTANT RIGHTS

(U) ff	::=	[read_right := false, write_right := false]
(U) rf	::=	[read_right := true, write_right := false]
(U) rw	::=	[read_right := true, write_right := true]
(U) fw	::=	[read_right := false, write_right := true]

CONSTANT PERMS

Sólo se consideran las configuraciones más habituales; podrían considerarse todas las configuraciones posibles y generar un caso para cada una.

(U) perms1	::=	[ownerp := rf, groupp := ff, otherp := ff]
(U) perms2	::=	[ownerp := rw, groupp := ff, otherp := ff]
(U) perms3	::=	[ownerp := rw, groupp := rf, otherp := ff]
(U) perms4	::=	[ownerp := rw, groupp := rw, otherp := ff]
(U) perms5	::=	[ownerp := rw, groupp := rw, otherp := rf]
(U) perms6	::=	[ownerp := rw, groupp := rw, otherp := rw]

CONSTANT SecClass

sc

:=

[level := M, categs := {FBI, NATO, CIA, MENEM}]

CONSTANT ACL₂ (U): (set OBJECT*AccessCtrlListData)

{o	:->	aclo,
o1	:->	aclo1,
o2	:->	aclo2,
o3	:->	aclo3,
barra	:->	acl/}

CONSTANT GRPNAME -> (set SUBJECT)

G4	:=	{g :-> {u}, g1 :-> {u1}, g2 :-> {u2}, g3 :-> {u3}, RG :-> {root}, SAG :-> {secofr, u3}, AG :-> {u, u1, u2, u3, root, secofr}}

CONSTANT (set OBJECT*ReadersWriters)

SM4	:=	{o1 :-> [ActReaders := {u}, ActWriters := {}], o2 :-> [ActReaders := {}, ActWriters := {u1}], o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}

SM5	:=	{o1 :-> [ActReaders := {u1}, ActWriters := {}], o2 :-> [ActReaders := {}, ActWriters := {u,u1}], o3 :-> [ActReaders := {u1}, ActWriters := {u1}]}

CONSTANT p (U), p₁ (U): OBJNAME

CONSTANT p_d (U), p_f (U): OBJNAME

CONSTANT OBJECT

(U) od	::=	(pd, Directory)
(U) of	::=	(pf, File)

CONSTANT (set OBJECT*FILECONT)

(U) Fof	::=	{of :-> fc1, o1 :-> fc1, o2 :-> fc1, o3 :-> fc1, }

CONSTANT (set OBJECT*DIRCONT)

(U) Dof	::=	{barra :-> < of.1, o1.1, o2.1, o3.1> }
(U) Dod	::=	{barra :-> < od.1, o1.1, o2.1, o3.1>, od :-> < >}

CONSTANT (set OBJECT*SecClass)

(U) OSCod	::=	{od :-> [level := N, categs := {FBI, NATO}], o :-> [level := N, categs := {FBI, NATO}], o1 :-> [level := N, categs := {FBI, NATO}], o2 :-> [level := N, categs := {FBI, NATO}], o3 :-> [level := N, categs := {FBI, NATO}], bSC }

CONSTANT AccessCtrlListData

(U) acl/2	::=	[owner := root, group := RG, UserReaders := {root}, GroupReaders := {AG}, UserWriters := {root}, GroupWriters := {AG}, UserOwners := {root}, GroupOwners := {RG}]

CONSTANT (set OBJECT*AccessCtrlListData)

(U) ACLod	::=	{od :-> aclo, o :-> aclo, o1 :-> aclo1, o2 :-> aclo2, o3 :-> aclo3, barra :-> acl/2}

CONSTANT GRPNAME -> (set SUBJECT)

(U) G2	::=	{g1 :-> {u, user}, RG :-> {root}, SAG :-> {secofr}, AG :-> {u, user, root, secofr}}

CONSTANT SUBJECT -> GRPNAME

(U) PG2

::=

{u :-> g1, user :-> g1, root :-> RG, secofr :-> SAG}

CONSTANT AccessCtrlListData

(U) acl2o	::=	[owner := u, group := g1, UserReaders := {root}, GroupReaders := {g1}, UserWriters := {u}, GroupWriters := {}, UserOwners := {u}, GroupOwners := {RG}]

CONSTANT (set OBJECT*AccessCtrlListData)

(U) ACL2	::=	{o :-> acl2o, barra :-> acl/}

CONSTANT (set OBJECT*AccessCtrlListData)

(U) ACL/2	::=	{o :-> aclo, o1 :-> aclo1, o2 :-> aclo2, o3 :-> aclo3, barra :-> acl/2}