Information Technology Reference
In-Depth Information
and delegations. However, this logic lacks the capability for specifying and rea-
soning about role-based access control (RBAC) [4,6]. RBAC policies are par-
ticularly well-suited for large-scale computing systems, because they reduce the
administrative complexity of associating users with permissions by decoupling
the two: users are authorized for
roles
, and permissions are assigned to roles.
RBAC also supports a decentralized view of access control.
Our objective is to unify within a single logic the ability to describe and
reason about access-control requests and decisions based on the relationships
between principals, statements, and trusted authorities while accounting for cre-
dentials, delegation, and RBAC roles. We therefore extend the access-control
logic of Abadi to encompass three major RBAC components: (1) user-role asso-
ciations, (2) role-permission associations, and (3) role-inheritance relations. We
express user-role associations as delegations (roles delegate their authority to
users to act on their behalf); role-permission associations and role-inheritance
relations are expressed as relations among principals and sets of statements by
which certain statements of one principal may be attributed to another principal.
With these extensions, we can (1) model RBAC policies within the access-control
logic, and (2) reason about RBAC-based access-control decisions.
Other researchers have used modal logic for describing security policies and
properties [8,2]. Those frameworks are more general than ours, but require a
high level of sophistication on the part of users. Our objective was to identify
a simple logic accessible to engineers that nonetheless could describe a wide
variety of access-control concerns. Our experiences teaching the Abadi logic to
computer science and engineering Master's students indicate that the logic meets
those criteria [12,13].
To verify the soundness of the access-control logic and its extensions, we
use the HOL (Higher Order Logic version 4) theorem prover [7,10]. Defining
the access-control logic within HOL serves several purposes. First, HOL is used
to verify the soundness of the access-control logic. Second, because HOL is an
open system, all of our proofs can be easily checked by third parties. Finally,
the existence of an executable and verifiable access-control logic implemented
in HOL makes both the access-control logic and a means for formal verification
available to design and verification engineers.
In addition to user-role associations, role-permission associations, and role
hierarchies, RBAC allows the specification of constraints that prevent users from
(1) being assigned to roles that are in conflict (static separation of duty), and
(2) activating certain roles simultaneously (dynamic separation of duty). These
constraints are outside the direct scope of the access-control logic, which focuses
on access-control decisions for a specific policy. In contrast, the separation of
duty constraints impose limits on what should be considered a well-defined or
consistent policy in the first place. However, like the access-control logic, these
constraints can be described and verified within the higher-order logic of HOL.
Hence, we are able to use higher-order logic to verify the consistency of a specific
RBAC policy prior to using the access-control logic to reason about access-
control decisions based on that policy.
