The SecureMOVA tool

Summary
Background
Installing the tool
Starting the tool
Initialising a session
Modeling a security policy
Querying the security model

Summary

The SecureMOVA tool is a prototype for analyzing SecureUML + ComponentUML models, which is directly based on the metamodel-based approach for analyzing security-design models presented in [BCDE:07]: queries about properties of the security policy modeled are expressed as formulas in the Object Constraint language (OCL) and evaluated on the metamodel of SecureUML + ComponentUML. The policy may include both declarative aspects, i.e., static access-control information such as the assignment of users and permissions to roles, and programmatic aspects, which depend on dynamic information, namely, the satisfaction of authorization constraints in the given scenario.

SecureMOVA is an extension of the MOVA tool, a modeling and validation for UML diagrams with OCL constraints. The MOVA tool provides commands for building class and object diagrams, validating OCL constraints, and evaluating OCL queries. With the exception of its graphical interface, the MOVA tool is written in Maude, a rewriting-based programming language that implements a very rich equational logic. SecureMOVA extends the MOVA tool with commands for building SecureUML + ComponentUML diagrams and for evaluating OCL queries.

Background

SecureUML is a modeling language for formalizing access control requirements that is based on Role-Based Access Control (RBAC). In RBAC one specifies access control policies in terms of static role assignments, however, it is not easily possible to specify policies that depend on dynamic properties of the system state. SecureUML extends RBAC with authorization constraints to overcome this limitation.

SecureUML provides a language for specifying access control policies for actions on protected resources. However, it leaves open what the protected resources are and which actions they offer to clients. These depend on the primitives for constructing models in the system design modeling language. A SecureUML dialect specifies how the modeling primitives of SecureUML are integrated with the primitives of the design modeling language in a way that allows the direct annotation of model elements with access control information.
The ComponentUML language is a simple language for modeling component-based systems. Essentially, it provides a subset of UML class models: Entities can be related by Associations and have Attributes and/or Methods. The dialect definition then specifies the following:

Entities, as well as their Attributes, Methods, and AssociationEnds (but not Associations as such) are protected resources.
the actions offered by these resources are:

Resource Actions

Entity create, read, update, delete, full access

Attribute read, update, full access

Method execute

Association end read, update, full access

The dialect definition also specifies the following action hierarchy:

EntityFullAccess:
create, read, update, and delete of the entity.
EntityRead:
read for all attributes and association ends of the entity, and execute for all side-effect free methods of the entity.
EntityUpdate:
update for all attributes of the entity, update for all association ends of the entity, and execute for all non-side-effect free methods of the entity.
AttributeFullAccess:
read and update of the attribute.
AssociationEndFullAccess:
read and update of the association end.
The precise definitions of the actions offered by the different resources and of the hierarchy among these actions is done adding OCL invariants to the metamodel.
The default access control policy is allow.

Resource	Actions
Entity	create, read, update, delete, full access
Attribute	read, update, full access
Method	execute
Association end	read, update, full access

Example

As a running example, consider a simplified system for administrating meetings. We later use this example to illustrate how one can mechanize the analysis of security policies using SecureMova. In this example, the system should maintain a list of users and records of meetings. A meeting has an owner, a list of participants, a time, and a place. Users may carry out standard operations on meetings, such as creating, reading, editing, and deleting them. A user may also cancel a meeting, which deletes the meeting and notifies all participants by email. The system should obey the following security policy:

All users of the system are allowed to create new meetings and read all meeting entries.
Only the owner of a meeting is allowed to change meeting data and cancel or delete the meeting.
A supervisor is allowed to cancel any meeting.
A system administrator is allowed to read meeting data, and administer the persons in the system.
A supervisor (but not a system administrator) is also a user of the system.

Example security policy

The following diagram models an example scenario of the above security policy. It contains two users, Bob and Alice with roles User and Scenario, respectively. It also contains one meeting, Kick-off, which has Alice as its owner.

Example scenario

Installing the tool

To run the tool you need to have installed the latest version of Maude, which you can download from http://maude.sip.ucm.es/securemova/maude-linux.tgz. You also need to have the latest version of the (non-graphical) MOVA tool, which you can download from http://maude.sip.ucm.es/securemova/ocl-tool-v31.tar.gz. To unzip-untar the file ocl-tool-v31.tar.gz type at your shell's prompt

> tar xvfz ocl-tool-vxxx.tar.gz

Your system will output

ocl-tool-v31/ ocl-tool-v31/sec-ocl-basic.maude ocl-tool-v31/sec-ocl-tool.maude ocl-tool-v31/sec-ocl-invariant-representation.maude ocl-tool-v31/sec-ocl-model-representation.maude ocl-tool-v31/sec-ocl-spec-creation.maude ocl-tool-v31/securemova.maude

`Starting the tool`


The (non-graphical) MOVA tool is a Maude program. To run the tool
you need to start the Maude interpreter.

Assuming that $MAUDE-PATH is the full-path to the directory
in which you have installed the Maude system, 
to start first the Maude interpreter type in at the shell's prompt

>$MAUDE-PATH/maude.linux


The Maude system outputs its prompt:

Maude>


Assuming that $MOVA-PATH is the full-path to the directory
in which you have stored the MOVA tool's modules,
to start the tool type in at the Maude's prompt

Maude> load $MOVA-PATH/sec-ocl-tool.maude

    
Initialising a session

To initialise a SecureMOVA session type in at the Maude's prompt
Maude> load $ITP-OCL-PATH/securemova.maude


The file securemova.maude includes:

the MOVA commands that create the class diagram SEC+COMP-META corresponding to the metamodel
of SecureUML + ComponentUML.

the MOVA commands that declare the invariants of the metamodel of
SecureUML + ComponentUML.

the MOVA commands that define a collection of  OCL query operations 
that are useful for analyzing security properties of SecureUML + ComponentUML models.



    Modeling a security policy along with an scenario
We list below all the commands that are used to build the security
policy SCHEDULER, along with the scenario
depicted above.  The SecureMOVA commands should be
self-explanatory: each command consists of a keyword, that indicates
the action to be taken, along with some parameters that provide the
additional information that is needed to perform the given action.
For example, the command (create-security-diagram SCHEDULER .)
creates a blank security-design diagram SCHEDULER, while the
commands (insert-role SCHEDULER : Supervisor .),
(insert-permission SCHEDULER : SupervisorCancel .), and
(insert-permission-assignment SCHEDULER : SupervisorCancel :
  Supervisor .)  insert first the role Supervisor and the
permission SupervisorCancel in the diagram SCHEDULER,
and then assign the latter to the former in the same diagram.





(create-security-diagram SCHEDULER .)

(insert-role SCHEDULER : SystemAdministrator .)

(insert-role SCHEDULER : Supervisor .)

(insert-role SCHEDULER : SystemUser .)

(insert-role-hierarchy SCHEDULER |  Supervisor <-> SystemUser .)

(insert-entity SCHEDULER : Meeting .)

(insert-entity SCHEDULER : Person .)

(insert-attribute SCHEDULER : Meeting : start : Integer .)

(insert-attribute SCHEDULER : Meeting : duration : Integer .)

(insert-attribute SCHEDULER : Person : name : String .)

(insert-association SCHEDULER : Meeting : meeting : < * > <-> < 1 > : owner : Person .)

(insert-non-query-method SCHEDULER : Meeting : cancel  .)

(insert-non-query-method SCHEDULER : Meeting : notify  .)

(insert-permission SCHEDULER : OwnerMeeting .)

(insert-permission SCHEDULER : UserMeeting .)

(insert-permission SCHEDULER : SupervisorCancel .)

(insert-permission SCHEDULER : UserManagement .)

(insert-permission SCHEDULER : ReadMeeting .)

(insert-permission-assignment SCHEDULER : OwnerMeeting : SystemUser .)

(insert-permission-assignment SCHEDULER : UserMeeting : SystemUser .)

(insert-permission-assignment SCHEDULER : SupervisorCancel : Supervisor .)

(insert-permission-assignment SCHEDULER : UserManagement : Supervisor .)

(insert-permission-assignment SCHEDULER : ReadMeeting : SystemAdministrator .)

(insert-entity-update SCHEDULER : OwnerMeeting : Meeting .)

(insert-entity-read SCHEDULER : UserMeeting : Meeting .)

(insert-atomic-delete SCHEDULER : OwnerMeeting : Meeting .)

(insert-atomic-create SCHEDULER : UserMeeting : Meeting .)

(insert-atomic-execute SCHEDULER : SupervisorCancel : Meeting : cancel .)

(insert-atomic-execute SCHEDULER : SupervisorCancel : Meeting : notify .)

(insert-entity-full-access SCHEDULER : UserManagement : Person .)

(insert-entity-read SCHEDULER : ReadMeeting : Meeting .)

(insert-authorization-constraint SCHEDULER : Auth1 : "equal[name[owner@[self:Class]], name[caller:Class]]" .)

(insert-authorization-constraint SCHEDULER : Auth2 : "true.Bool?" .)

(insert-authorization-constraint-assignment SCHEDULER : OwnerMeeting : Auth1 .)

(insert-authorization-constraint-assignment SCHEDULER : UserMeeting : Auth2 .)

(insert-authorization-constraint-assignment SCHEDULER : SupervisorCancel : Auth2 .)

(insert-authorization-constraint-assignment SCHEDULER : UserManagement : Auth2 .)

(insert-authorization-constraint-assignment SCHEDULER : ReadMeeting : Auth2 .)

(insert-entity-user SCHEDULER : Person .)

(insert-entity-instance SCHEDULER : Person : Alice .)

(insert-entity-instance SCHEDULER : Person : Bob .)

(insert-entity-instance SCHEDULER : Person : Charlie .)

(insert-entity-instance SCHEDULER : Meeting : Kick-Off .)

(insert-user-assignment SCHEDULER | Alice <-> Supervisor .)

(insert-user-assignment SCHEDULER | Bob <-> SystemUser .)

(insert-attr-value SCHEDULER : Person : Alice : name : String -> "Alice" .)

(insert-attr-value SCHEDULER : Person : Alice : name : String -> "Bob" .)

(insert-link SCHEDULER | Meeting : meeting <-> owner : Person | Kick-Off <-> Alice .)




   
Querying the security model


To query a security model built using the SecureMOVA commands, use the command
query-in with the OCL expression formalizing the query. You can use the operations
declared in the securemova.maude file, but you can also introduce your own operations
using the appropriate MOVA commands. Notice, however, that there are a few
syntactical differences with the standard OCL notation:


To use the contextualized variable self, write self 
along with its contextual class (separated by a semicolon).
 
To apply a role or an attribute to an object:

prefix the symbol # to the role's name or the attribute's name; in
  addition, if the role's multiplicity is <1>, postfix the symbol @ to the role's name; and
insert a blank space between the expression denoting the object and the role's name.

 
To apply a role to a collection of objects, use the collect iterator. 

To use an iterator-bounded variable, write the variable along with its iterator-based class (separated by a semicolon).
 
To apply an iterator with several iterator-bounded variables over a collection
of objects, write the iterator in nested form.

To apply the allInstances operator to a class (and, similarly, for the oclIsTypeOf, oclIsKindOf, oclAsType, and oclType operators):
- prefix the symbol # to the operator; and
- insert a blank space between the class' name and the operator.
To apply a defined operator to an object
- prefix the symbol # to the operator; and
- insert a blank space between the object' name and the operator.

The following are queries over the security model SCHEDULER, along with the scenario depicted above. The queries use the OCL operations defined in the securemova.maude file.

(query-in SEC+COMP-META : SCHEDULER : (Supervisor #haspermission) .)
(query-in SEC+COMP-META : SCHEDULER : (OwnerMeeting #accesses) .)
(query-in SEC+COMP-META : SCHEDULER : (Supervisor #superrolePlus) .)
(query-in SEC+COMP-META : SCHEDULER : (Supervisor #allPermissions) .)
(query-in SEC+COMP-META : SCHEDULER : (MeetingEntityUpdate #subactionPlus) .)
(query-in SEC+COMP-META : SCHEDULER : (OwnerMeeting #allActions) .)
(query-in SEC+COMP-META : SCHEDULER : (Bob #allAllowedActions) .)
(query-in SEC+COMP-META : SCHEDULER : (SystemAdministrator #allAtomics) .)
(query-in SEC+COMP-META : SCHEDULER : (MeetingAtomicDelete #allAssignedRoles) .)
(query-in SEC+COMP-META : SCHEDULER : (Supervisor #allAuthConstRole(MeetingcancelAtomicExecute)) .)
(query-in SEC+COMP-META : SCHEDULER : (duplicateRoles) .)
(query-in SEC+COMP-META : SCHEDULER : (MeetingstartAtomicRead #minimumRole) .)
(query-in SEC+COMP-META : SCHEDULER : (OwnerMeeting #overlapsWith(SupervisorCancel)) .)
(query-in SEC+COMP-META : SCHEDULER : (existOverlapping) .)
(query-in SEC+COMP-META : SCHEDULER : (accessAll) .)
(query-in SEC+COMP-META : SCHEDULER : (Alice #isAllowed(Kick-OffAtomicDelete)) .)
(query-in SEC+COMP-META : SCHEDULER : (Bob #allAllowedActionInstances) .)
(query-in SEC+COMP-META : SCHEDULER : (Kick-OffAtomicDelete #allUsers) .)

Manuel Clavel

Last modified: Mon Jun 11 18:56:23 CEST 2007

The SecureMOVA tool

Table of contents

Summary

Background

Example

Installing the tool

Starting the tool

Initialising a session

Modeling a security policy along with an scenario

Querying the security model

`Starting the tool`