Software Engineering Research Group PhD Thesis Defence

2011 Sep 23 at 08:30

DC 1331

Access Control Models and Policies for Pattern-based Business Processes

Vahid Karimi, PhD candidate, David R. Cheriton School of Comp. Sci., Univ. Waterloo

Access control represents an important aspect of security in software systems, since access control policies determine which users of a software system have access to what objects and operations and under what constraints. However, the process of creating access control models, basing rules in access control policies and policy sets explicitly on these models, and then integrating these policies into a business software system has not been defined systematically. A common modeling representation for this entire process has not been used, and for this reason such integration can be quite complex and error prone.

One can view access control models as providing the structure of rules for access control. Further, an access control policy can be seen as a combination of one or more rules, and one or more policies can be combined into a set of access control policies that control access to an entire system. The rules and resulting policies can be combined in many different ways, and the combination of rules is included in some policy languages. However, access control models and policies are often defined using different models and languages, and thus there is no clear relationship between the rules expressed in the policies and the underlying access control models. For this reason, composed policies may fail to exhibit the intended behaviour in many cases, especially when non-trivial conditions are involved.

This thesis describes a common modeling representation for access control models, rules derived from these models, policies produced from combinations of rules, and business processes incorporating access control policies. More specifically, this thesis contains the description of a model that allows the representation and verification of access control policies both separately and when integrated with business processes. The common representation is based on the Resource-Event-Agent (REA) model, new combinations of access control and business patterns, and state machines. Access control models based on REA are more expressive than traditional access control models since they can describe rules incorporating types and a specific kind of aggregation. As a consequence, the resulting policies and their combination into policy sets are also more expressive. The use of a state machine to combine rules and policies supports composition beyond that described in the literature because of the use of conditional policy expressions and history of policy outcomes.

Although REA has been used to describe business processes, this thesis presents for the first time a common representation based on REA and state machines that can be used to produce a general description of business processes, all existing general forms of access control models and their integration. This notation can be expressed in UML thereby providing a basis for its syntax and semantics.

An extensive survey of the access control literature indicates that there is no common modeling representation that systematically links access control models with policies expressed in policy languages. The work described in this thesis bridges this gap and uses the rules, based on REA, created from the models as a component of each policy in a policy set thereby creating a more systematic approach to access control. The approach in this thesis starts from an access model, proceeds to rule declaration and then uses these along with state machines to define policies and their combination in policy sets. The approach supports an access control model that can provide the vocabulary and underlying structure for rules that guide the formation of policies and policy sets.

This model that incorporates both structure and sequence can be used to describe access control policies for related business systems and then be used to verify various properties. A structured approach is developed to express these properties in linear temporal logic (LTL). First, the properties are expressed based on REA primitives using structured prose and then categorized making the properties more amenable to reuse. Then, the prose expressions are translated into UML diagrams that include state machines, which are then converted into LTL. This step is a prelude to the formal verification of properties using the SPIN model checker.

Finally, the approach is applied to the conference management system, a well-known example from the literature, to illustrate the expressiveness advantage of the common representation and the rule and policy-related reasoning capability. Several properties, whose verification was not possible by prior approaches, such as ones involving conditional policy expressions and history of policy outcomes are verified in this thesis.

More succinctly, the main contributions of this thesis are

1. a common representation for business processes, general access control models, rules, and policies;

2. the use of the common representation to produce an integrated description of access control and business processes for uniform modeling, and uniform property specification and verification;

3. the use of the common representation to demonstrate a coherent approach to access control by supporting the combination of rules into policies and sets of policies and the order of application of the rules and policies;

4. formal specification of rule and policy combination of access control policies and verification of properties, such as consistency and separation of duties; and

5. a case study, taken from the literature, that demonstrates the approach just described and illustrates the expressiveness advantage of the common representation, and the rule and policy-related reasoning capability.