Information Technology Reference
In-Depth Information
we must consider both when determining whether a particular RBAC policy
is consistent with its separation-of-duty constraints. The predicate
isConsistent
verifies that a given user assignment
UA
and role hierarchy (given as a Hasse
diagram
HSD
and a set of
ROLES
) do not violate the
SSD
constraints:
∀
UA SSD HSD ROLES. isConsistent UA SSD HSD ROLES
=
∀
rs n.
(
rs
⊆
ROLES
)
⊃
(
FINITE rs
)
⊃
(
n
≥
2)
⊃
(
rs, n
)
∈
SSD
⊃
(
∀
t.
(
t
⊆
rs
)
⊃
(
CARD t
≥
n
)
⊃
(
¬∃
U.
∀
r.
(
r
∈
t
)
⊃
(
U
∈
authorized users r UA HSD ROLES
)))
,
where
CARD t
returns the number of elements in the finite set
t
and
FINITE
s
returns true if the set
s
is a finite set.
[4] identifies several properties that should hold of consistent RBAC policies,
such as that if two roles are mutually exclusive, then no nonempty role can
possibly inherit both of them. We have verified that these properties do hold
in our HOL implementation, which provides additional assurance that we have
accurately captured the definitions.
5.2
Dynamic Separation of Duty
Dynamic separation of duty imposes constraints on the roles that a user can have
activated
at any given instant. Like static separation of duty, these constraints
are expressed as a set
DSD
: each pair (
rs, n
)
DSD
represents a constraint that
prevents a user from activating
n
or more roles in
rs
simultaneously.
In other words, if the set of roles associated with a user's session
s
is a subset
of
rs
,thenumberofrolesin
session roles
(
s
)mustbelessthan
n
. The predicate
SessionSatisfies
verifies that a session
s
satisfies the
DSD
constraints:
∈
∀
s DSD ROLES. SessionSatisfies s DSD ROLES
=
∀
rs n.
(
rs
⊆
ROLES
)
∧
(
FINITE rs
)
∧
(
n
≥
2)
∧
(
CARD rs
≥
n
)
∧
((
rs, n
)
∈
DSD
)
⊃
(
∀
t.
(
t
⊆
rs
)
∧
(
t
⊆
session roles
(
s
))
⊃
(
CARD t<n
))
.
As with static separation of duty, [4] also identified necessary consequences for
dynamic separation of duty constraints, such as that, if two roles are mutually
exclusive for activation, no session may involve both roles. We have verified that
these properties hold of our HOL implementation.
6
Conclusions
Building information systems correctly is dicult—assuring information systems
are secure is even more dicult. As the size, scope, and complexity of information
systems is ever increasing, designers and verifiers of information systems face
an ever more challenging task when assuring security. Many have observed that
engineers must design security into systems from the start and that designs must
