Modeling Access Control Policy With The RW Language
Bradley Berg CS196-1 May 14, 2006
1. Introduction
The RW language [1, 2, 3] was developed to express access control policies that
can be checked for properties of correctness. In particular actions of agents
acting alone or collaborating with others can be checked for safety. Safety
assurances show that intruders can not have unauthorized access to resources.
Additionally, permitted users must be granted access authorization.
The RW language elegantly captures the core properties of access control
systems. That is it focuses solely on access control and cleanly separates
access from content and its usage at the application level. Higher level
policy issues are excluded from RW. For example the notation does not include
constructs to support distributed policies [4] or explain why permissions are
denied [5]. It might be desirable to include such aspects as part of a policy
as well. Still their safety properties could be analyzed using RW.
The notation is simple and expressive; making it suitable for performing a
thorough policy analysis (See Appendix A). When modeling using logic-based
languages, subtle errors are easily introduced due to incomplete case analysis
and omissions. Interactions become more difficult to understand in
semantically rich languages such as Alloy [6]. There are more ways for
features to interact and alternative ways to implement a given property of a
system.
A model of the Continue conference system was written in Alloy [7] and used as
a reference model. The reference model does not fully represent the current
software for Continue as it requires some extensions. A model of the Continue
access policy was then written using the RW language that is consistent with
the reference model (See Appendix B).
This paper considers issues encountered while rewriting the Continue policy
using the RW language. Plausible extensions to the Continue policy are then
proposed to explore a variety of representation issues in the RW language.
2. Modeling With RW
Each Class in an RW policy denotes a type of entity. For the purpose of model
checking the Run statement specifies how many entities of each type are to be
used in the check. When executing the model within an application there may be
any number of entities.
The state of a model can be implemented as a collection of single bit variables.
Each predicate in the RW language corresponds to a multi-dimensional array of
state bits with dimensions determined by its arguments. The state associated
with a predicate with 2 arguments can be represented with a two dimensional
array of bits. The depth of each dimension is the number of entities in the
Class of each predicate parameter.
Each transition either Reads a state bit, Writes true, or Writes false. Any
User Agent can invoke a transition and the transition will either be performed
or rejected due to an access violation. The Read and Write clauses in each
predicate determine whether a transition is permitted or denied when requested
by a particular user agent.
2.1 Access to State Values
Predicates and state are intertwined in RW models. They are not, as in some
other languages, statements about a separate global state space. Two
predicates can not commingle control over any shared state. Note too that
predicates must have at least one parameter as they determine the amount of
state that can be accessed within each predicate.
A Continue conference has several global settings that may be changed at will
by Administrators. The Alloy reference model for Continue uses the
changeConferenceInfo predicate to represent changes to these settings as a
group. Note that the content of resources is not part of an access model.
Only permission to access the values is modelled. There are several ways with
the RW language to represent access to a set of values.
The simplest strategy is to just use the isAdmin predicate since the access to
it happens to be the same. However, the knowledge that changeConferenceInfo
and isAdmin have the same access control would then be represented outside the
formal model. The syntax could accommodate this by supporting aliases for
predicates. As long as the access is the same then an alias suffices.
Predicate isAdmin(agent) Alias changeConferenceInfo, ...
If instead the access predicate is more complex a more general macro construct
is required. Repeated instances of compound expressions can also be
encapsulated using macros. A more general extension can combine predicate
references in a common expression to provide an external interface for
composite predicates. It acts as a syntactic macro to expand the boolean
expression wherever the function is referenced in a predicate.
Function changeConferenceInfo(agent)
{ isAdmin(agent) or isChair(agent);
}
Another way to model value access is to create parallel predicates. In this
case there would be separate isAdmin and changeConferenceInfo predicates.
Whenever an application performs a write to the isAdmin predicate, it must also
perform the same write to the changeConferenceInfo predicate. Knowledge about
this access relationship is then pushed into the application; disjoint from the
model. Also a check can not enforce that the parallel predicates are
transitioned atomically, so checks can not incorporate that fact.
changeConferenceInfo(agent)
{
// Anyone can read conference information.
read: true;
// Only Administrators can modify it.
write: isAdmin(agent);
}
An alternative technique uses a dummy argument to represent a single state bit.
This takes advantage of the two states returned upon access. One is the value
of the state bit and the other is whether or not access is granted. When write
access is allowed then the application interprets that as permission to modify
the values is granted. The actual value of the dummy state is not significant.
In this case the dummy argument needs to be limited to a single entity by the
Run command. During execution the value of the dummy argument is ignored.
changeConferenceInfo(dummy)
{
// Anyone can read conference information.
read: true;
// Only Administrators can write the info.
write: isAdmin(user);
}
2.2 Representing Enumerations
Enumerations can be represented in an RW model using a separate predicate for
each enumerated state. An ordered enumeration progresses through a fixed
sequence of states. In the Continue model the phases for a conference and
papers are ordered enumerations. Predicate signatures for conference phases
and the body of the inPreSubmission predicate are given below.
// There is a predicate for each phase, but only one phase element.
//
inInitialization(phase: Phase),
inPreSubmission( phase: Phase),
inSubmission( phase: Phase),
inBidding( phase: Phase),
inAssignment( phase: Phase),
inDiscussion( phase: Phase),
inNotification( phase: Phase),
inPublishing( phase: Phase);
inPreSubmission(phase)
{
// Authors are not allowed to find out the current phase.
read: ~isAuthors(user);
// Only administrators can progress the conference phase.
write: isAdmin(user) and
// The current phase must be Initialization.
~inPreSubmission(phase) and inInitialization(phase);
}
The Phase parameter for the predicates is a dummy argument and the model must
be run with one Phase entity. In this case the state in the model is
represented as eight bits, one per phase predicate.
Initially the state bit for inInitialization is set true; all others default to
false. To advance the phase to PreSubmission, true is written to the
inPreSubmission predicate by an administrator. It is constrained to avoid
rewriting the phase twice and to ensure the current phase is Initialization.
As the phases progress the state bit for the next phase is marked true.
Unordered enumerations can not be represented in this fashion. Changing from
one enumerated state to another requires clearing one state bit and setting
another in a single transition. The RW modeling language could be extended to
support enumerations. Examples suggesting a notation is:
Class Phase In Initialization,
PreSubmission,
Submission,
Bidding,
Assignment,
Discussion,
Notification,
Publishing;
The 'In' keyword represents an ordered enumeration and another keyword,
such as 'Any' could be used to designate an unordered enumeration.
Within the model predicate bodies would be much cleaner as enumerated states
could be directly referenced. Note that for Continue phases the read access
for the Notification phase is difference than the other phases.
phase Phase
{
// The phase can be read by authors except the notification phase.
//
read: ~(phase = notification) or
((phase = notification) and ~isAuthor(user));
// Only administrators can change the Conference phase.
write: isAdmin(user);
}
Instead of referencing a particular phase as:
inSubmission(phase) and ~inBidding(phase)
we could say: phase = Submission
2.3 Atomic States Using Global Constraints
In the conferencing example suppose we wanted to extend the model with a
conference Chair and allow only one Chair at a time. When changing Chairs the
state bit for the current Chair needs to be cleared and the new Chair's set.
One way to enforce a single Chair is to constrain all other predicates. A
global constraint is applied to all write clauses in other predicates. The
constraint keeps any other predicate transition from occurring until the chair
is set.
isAuthor(agent, phase)
{
read: true;
write: // Global constraint applied as part of the isChair predicate.
(E a: Agent [ isChair(a) ])
// The original constrains for isAuthor.
and (isAdmin(user) and ~isAuthor(agent, phase)
and inSubmission(phase) and ~inBidding(phase) );
}
This approach applies additional constraints to prevent any state changes until
isAdmin is assigned. Explicitly coding global constraints is cumbersome. They
need to be consitantly applied to each predicate as the model is written or
modified. To represent a global constraint in a model the syntax needs to be
extended. A possible syntax for global constraints is given below. Since the
constraint will be applied to any predicate except one then a reasonable place
to declare it is in the one exception.
isChair(agent)
{
// Conjoin this predicate with all other writes.
global: E a: Agent [ isChair(a) ];
// Anyone can see who is a chair.
read: true;
// Only the administrator can add new chairs.
write: isAdmin(user);
}
The global constraint also needs to be applied to the read predicate in the
isChair clause. In the event that an another clause references the isChair
clause when the predicate is in the intermediate state with no Chairs,
permission would be denied.
When access is denied due to a global constraint it differs in that it is
temporary and not a true denial. In the execution model referencing the
intermediate state needs to be avoided using serialized access to the model.
The serialization mechanism could implicitly perform the atomic write to
complete the transition.
When checking the model a temporary denial doesn't matter. Unlike model
execution, no actions are performed as side effects of the denial. The check
is looking for combinations of permitted states and the temporary denial would
be resolved as the atomic action would be forced to completion in the next step.
In the previous example note that the entities authorized to establish a Chair,
an Administrator, are disjoint entities from the Chair. If instead of a Chair
only a single Administrator was allowed, a global constraint would not suffice.
A transition to a new Administrator would not be possible since only an
Administrator is permitted to assign another Administrator. Once the previous
Administrator was removed there would be no entity that could establish the
next Administrator.
Performing atomic transitions using global constraints is also limited to
single predicates. Atomic transitions may need to be applied over multiple
predicates. To illustrate this, suppose the continue example is extended to
say, 'If an agent becomes a Reviewer they must be assigned at least one paper.'
That is when an agent becomes a reviewer they must also be assigned a paper as
an atomic transition. The check would ensure that all reviewers are assigned
to at least one paper.
In this case we need to write true to the predicates isReviewer and
assignPaper. Since papers can only be assigned to reviewers, first we have to
designate the new reviewer by writing true to the isReviewer predicate. If a
global constraint was used, it would need to force assignPaper. However, the
arguments needed for assignPaper are not available within isReviewer and
consequently can not be incorporated in the global constraint. we can't force
the next move by applying the constraint:
assignPaper(paper, reviewer, phase)
In order to work in any predicate global constraints must be fully qualified
and have no external references. This approach will work when checking for
empty or full sets, but not parameterized sets.
2.4 Independent Atomic transitions
While global predicates can be implemented without extending the check
algorithm, their limitations warrant investigation of alternatives to perform
atomic transitions. Atomic transitions can be expressed by using a
pre-condition and post-condition constructs. Pre-conditions and
post-conditions were used by Frias [8] to extend Alloy. This made the
resulting Alloy specifications more simple and clear; while creating
opportunities for optimization.
One approach is to model atomic transactions in a stateless composite function.
The pre-condition is checked first for access permission. If omitted access
checks implicitly required in the post conditions are used. The post-condition
is a conjunction of predicates denoting atomic transitions. False is written
to negated predicates and true is written to positive predicates. There is no
corresponding read transition for the Function.
Function changeAdmin(from, to)
{
pre: isAdmin(from);
post: ~isAdmin(from) and isAdmin(to);
}
This approach could also be used to transition ordered enumerations.
Function setBidding(phase)
{
pre: isSubmission(phase);
post: ~isSubmission(phase) and isBidding(phase);
}
Unordered enumerations require setting one predicate and clearing all others
in the enumeration.
Function setBidding(phase)
{
post: inBidding(phase)
and ~inInitialization(phase)
and ~inPreSubmission(phase)
and ~inSubmission(phase)
and ~inAssignment(phase)
and ~inDiscussion(phase)
and ~inNotification(phase)
and ~inPublishing(phase);
}
Rather than declaring a separate function, the post-condition could be embedded
within a predicate. The post-condition is expressed locally within an
initiating predicate so that a separate function doesn't need to be declared.
The limitation is that the parameters of predicates in a post-condition can
only be those of the initiating predicate. This limitation might in fact be
desirable as passing the composite parameters through a function might result
in unnecessarily complex models.
assignPaper(paper, reviewer, phase)
{
read: true;
write: // Only an administrator can assign papers to reviewers.
// Move isReviewer to the post condition.
isAdmin(user) // and isReviewer(reviewer)
// Must be in the paper assignment phase.
and paperAssignment(paper, phase) and ~paperReviewing(paper, phase);
post: isReviewer(reviewer);
}
The case where we want only one Administrator in a conference can be
represented with a post-condition as:
oneAdmin(agent)
{
// Anyone can see who is a chair.
read: true;
// Only the administrator can pass on the role.
write: oneAdmin(user);
// There may be only one chair; remove the original.
post: ~oneAdmin(user);
}
Ordered enumerations still require separate predicates for each state and a
dummy argument.
inPreSubmission(phase)
{
// Anyone can find out the current phase.
read: true;
// We don't need to check for ~inPreSubmission(phase);
write: isAdmin(user) and inInitialization(phase);
// The post condition clears the old phase.
post: ~inInitialization(phase);
}
Unordered enumerations also need separate predicates and a dummy argument.
inPreSubmission(phase)
{
// Anyone can find out the current phase.
read: true;
// Don't need to check the prior phase.
write: isAdmin(user);
// The post condition clears the prior phase by clearing
// all the other phases.
post: ~inInitialization(phase)
and ~inSubmission(phase)
and ~inBidding(phase)
and ~inAssignment(phase)
and ~inDiscussion(phase)
and ~inNotification(phase)
and ~inPublishing(phase);
}
3.0 Conclusion
The Continue conference system can be fully expressed using the RW modeling
language. For such a simple notation the resulting model was surprisingly
clean. Overall the RW model was easier to write and understand than the Alloy
model. The only awkward representations were the conference phase (ordered
enumeration) and the introduction of dummy arguments.
On the other hand, a low level language like RW might make it more difficult to
compose more complex policies. The policy writer may have to employ artifacts
not relevant to the model. RW has no provision for expressing common idioms
and higher level abstractions. It might be more appropriate to write policies
using higher notations. A front-end language for RW requires a semantic
equivalent of a check. It might be possible to automatically generate common
checks from a higher level language.
Syntactic extensions can be easily added to the RW language. Still it might
be better to incorporate them in a higher level policy language rather than
extend RW itself.
Ordered enumerations can be supported by a front end to clean up the model. In
the case of Continue this was the most awkward thing to represent. Extending
the RW parser might make experimenting with RW models easier.
Unordered enumerations could be added, but they could not be checked without
extending the check algorithm. If they were not checked an agent could set
multiple conflicting states or set no state. Even without explicit checking
this might be useful. Intermittent cases could never be explicitly checked and
the application programmer interface for the execution model could exclude any
case that would permit it.
Macro functions could be added to avoid repetitous patterns. They could also
be used to represent unchecked atomic actions with the same limitations as
described above for unchecked unordered enumerations.
The RW modeling language is an effective tool for experimenting with access
control policy. Since it is very difficult to manually check policies, the
ability to automate policy checks is essential for testing their safety. With
extensions or a high level front-end RW provides a sound basis for implementing
production quality access policies. As a core policy mechanism it may be
adapted in a wide variety of access control systems.
BIBLIOGRAPHY
[1] Nan Shang, Mark Ryan and Dimitar P. Guelev. Synthesising Verified Access
Control Systems through Model Checking. Pre-publication April 19, 2006.
[2] Dimitar P. Guelev, Mark Ryan, Pierr Yves Schobbens. Model-checking Access
Control Policies. Seventh Information Security Conference (ISC '04),
Computer Science, Springer-Verlag, 2004.
[3] Nan Zhang, Mark Ryan, Dimitar P. Guelev. Evaluating Access Control
Policies Through Model Checking. Eighth Information Security Conference
(ISC `05). Computer Science, Springer-Verlag, 2005.
[4] Apu Kapadia, Geetanjali Sampemane, and Roy H. Campbell. Know Why Your
Access was Denied: Regulating Feedback for Usable Security. CSS '04, 2004.
[5] Blaze, Feigenbaum, and Lacy. Decentralized Trust Management.
Proceedings of the 1996 IEEE Symposium on Security and Privacy.
[6] D. Jackson., Alloy: a lightweight object modeling notation.
ACM Transactions on Software Engineering and Methodology, 2002.
[7] Reference Model for Continue in Alloy. Jay McCarthy. 2006.
Only available through the internal Brown network.
http://web-int.cs.brown.edu/courses/cs296-1/2006/continue.als
[8] M. F. Frias, J. P. Galeotti, C. G. Lopez Pombo, N. M. Aguirre. DynAlloy:
upgrading alloy with actions. Proceedings of the 27th international
conference on Software engineering, 2005, pp. 442-451.