In case of collaborative modeling, complex systems are developed by different stakeholders, in offline submissions or online sessions. To guarantee security, access control policies need to be enforced during the collaboration.
As levels of required confidentiality and integrity may vary across model parts, we have previously proposed fine-grained rule-based access control, and shown how to consistently interpret flexible access control policies.
Now we present an improvement on the previous results allowing for incremental recomputation, which is vital for online collaboration scenarios. Our approach is illustrated using a case study of the MONDO EU project.
Model-based systems engineering has become an increasingly popular approach [32] in critical cyber-physical systems followed by many system integrators like airframers or car manufacturers to simultaneously enhance quality and productivity. An emerging industrial practice of such system integrators is to outsource the development of various components to subcontractors in an architecture-driven supply chain. Distributed teams of different stakeholders (system integrators, software engineers of component providers/suppliers, hardware engineers, specialists, certification authorities, etc.) may collaborate using models.
In an offline collaboration scenario, collaborators check out an artifact from a version control system (VCS) and commit local changes to the repository in an asynchronous long transaction. In online collaboration, engineers may simultaneously edit a model in short synchronous transactions which are immediately propagated to all other users (similarly to online collaborative tools like Google Docs). Several collaborative modeling frameworks exist [23], but security management is unfortunately still in a preliminary phase.
In fact, collaborative scenarios introduce significant challenges for security management, both in terms of confidentiality and integrity. For instance, the detailed internal design This paper is partially supported by the MTA-BME Lendület 2015 Research Group on Cyber-Physical Systems. The first author was supported by the János Bolyai Research Scholarship of the Hungarian Academy of Sciences. of a specific component needs to be revealed to certification authorities to obtain certification credit but they need to be hidden from competitors who might supply a different component in the system. Furthermore, there may be critical aspects of the system model that may only be modified by domain experts having the appropriate qualifications.
Capturing security policies on the storage (file) level instead of the model level results in inflexible fragmentation of models in collaborative scenarios (although flexibility is key [25]); this can be solved by fine-grained access control, where each model element and its features can have its own set of permissions. On the other hand, large industrial models can have millions of model elements, thus explicitly assigning permissions for each of them, as well as maintaining the permissions after changes to the model, would be laborintensive and error-prone, and would make it difficult to understand the system of privileges.
A rule-based approach for concisely defining fine-grained model access control policies has been proposed in [6]. A single rule may grant or deny nominal permissions for many elements in a model. Due to this implicit nature, it is possible that several rules would be in direct conflict with each other, assigning contradictory permissions for some model element. Indirect conflicts are also possible, if the fragment of the model revealed to a user is not consistent with itself, or with the write permissions. In [10], we resolve conflicts in a deterministic and customizable way to present a consistent and secure updateable view to each user.
The solution in [10] relies on an algorithm that can be executed for a given state of the model to derive the effective permissions from the nominal ones. However, this strategy might not scale up to larger system models in case of online collaboration, as the algorithm would have to re-process the permissions of all model elements after each small editing operation, leading to unacceptable response times.
In this paper, we investigate a possible way to incrementalize the conflict resolution schema, so that small changes within large models would incur a small maintenance com- [6], (b) inherit the beneficial features (flexibility, consistency, determinism) of the non-incremental resolver algorithm [10], and (c) complement the incremental policy rule evaluation and enforcement techniques presented in [6] to guarantee acceptable performance for online in addition to offline collaboration.
We achieve this goal by reformulating the original algorithm of [10] as a recursive Datalog [16] query on the system model (technically recursive VIATRA [5] graph patterns), for which incremental evaluation algorithms are known. We point out subtle difficulties with the evaluation of the resulting patterns, and suggest solutions for dealing with them.
Several concepts will be illustrated using a simplified version of a modeling language for system integrators of offshore wind turbine controllers, which is one of the case studies of the MONDO EU FP7 project. The metamodel, defined in EMF [29] and depicted by Fig. 1, describes how the system is modeled as modules organized in a containment hierarchy of composite modules. Composite modules may express protected IP and they can ultimately contain control unit modules that are responsible for a given type of physical device (such as pumps, heaters or fans).
We assume that each control unit type (Pump, etc. . . ) is associated with a specific person (referred to as specialist) who is responsible for maintaining the model of control unit modules of that specific type. Each such user is able to modify the control units that belong to them, they cannot access to any control unit contained directly or indirectly by composite module that express protected IP. For instance, the user responsible for pump controllers (the Pump Control Engineer) can modify the controller ctrl1 but cannot see the object ctrl4 as it is contained c2 which describe that its content is protected. Finally, there is a principal engineer 2) Online Usage Scenario: The system integrator company is hosting the wind turbine control model on their collaboration server, where it is stored, versioned, etc. A group of users may participate in online collaboration, where they are continuously connected to the central repository via an appropriate client (e.g. web browser). Through their client, each user sees a live view of those parts of the model that they are allowed to access. The users can modify the model through their client, which will directly forward the change to the collaboration server. Then the server will decide whether the change is permitted under write access restrictions. If it is allowed, then the views of all connected users with appropriate read permissions will be updated transparently and immediately. However, changes introduced by a user may influence the accessibility of model parts for other users. Hence, the access control policy has to be reevaluated when the model is changed.
Example 2. After the Principal Engineer changes the pro-tectedIP attribute of the composite module c2 from true to false, the Pump Control Engineer shall be able to access the contained pump control module ctrl4.
Here we briefly introduce a vocabulary for fine-grained access control; a more detailed treatment can be found in our previous work [6] and especially [10].
In order to provide fine-grained access control, models have to be decomposed into smaller assets that can be separately protected. For simplicity, we will consider models as a set of elementary model facts. For example, EMF models (ignoring the multi-resource case) consist of the following kinds of model facts: Object facts are pairs formed of a model element (EObject) with its exact type (EClass), for each model element object; e.g. obj(c1,Composite). Attribute facts are triples formed of a source EObject, an attribute name (EAttribute) and the attribute value, for each (non-default) attribute value assignment; e.g. attr(ctrl3, cycle,::low).
Reference facts are triples formed of a source EObject, a reference type (EReference) and the referenced EObject, for each containment link and cross-link between objects; e.g. ref(c1,submodules,ctrl2). Note that for multi-valued attributes and references, each of the multiple entries at a source EObject will be represented by a separate attribute or reference fact.
In the following, we will focus on object facts, but the same formal framework applies to all assets.
The above mentioned model facts are the assets that the access control policy will protect against operations (typically read and write) that can be performed by the user. The goal of interpreting the security policy is to come up with an effective permission function that assigns a permission level to each combination of asset, user and operation.
The assigned permission level takes its value from a permission lattice characteristic to the operation. In the simplest case, this is the two-valued lattice {deny < allow}; in general it is possible to use a more refined lattice instead. In the rest of the paper, we will restrict ourselves to the case where the lattice is a total order, i.e. from any two levels, one is considered strictly more restrictive than the other.
For instance, it was previously suggested [10] to use {deny < obfuscate < allow} as read permission levels, to express the case where an attribute of an otherwise visible object conveys confidential information that shall not be revealed to the given user, but the attribute can not be completely hidden (since it is used as e.g. an identifier or visual label).
A sample refinement of the write permission levels could be {deny < dangle < allow}, where cross-references with write permission level dangle can not be normally modified by the user, but they can be removed as the side effect of deleting the target object of the reference (if that deletion is permitted), even if the cross-link is not visible to the user. Imagine a traceability link that points from a hidden part of the model to a visible object; the difference between assigning deny or dangle is that the target object can not be deleted by the user in the former case, while its deletion would be allowed (with an invisible side-effect of removing the traceability link) in the latter case.
The view presented to a user consists of the set of assets for which they have read permissions (modulo obfuscation, see above). However, an arbitrary set of model facts does not necessarily constitute a valid model; there may be internal consistency constraints (also called referential integrity constraints) imposed on the facts by the modeling platform to ensure the integrity of the model representation and the ability to persist, read, and traverse models. A major goal stated in [6], [10] requires that secure models must be synthesized as a set of model facts compatible with all internal consistency rules.
Note that we distinguish these low-level internal consistency rules from high-level, language-specific well-formedness constraints. Violating the latter kind does not prevent a model Internal consistency of the filtered view implies that the effective permissions must satisfy a some constraints that are expressed as a strong dependency relationship between two values of the effective permission function: a dependant and a dependee. According to the formalization in [10], this relationship is a Galois connection. This means that if a lower bound is known for the permission level of the dependant, then a lower bound on the permission level of the dependee is inferred; and conversely, an upper bound on the dependee puts an upper bound on the dependant. For instance, (a) if an asset is writable (write permission level allow), then it must also be visible (at least on the read permission level allow); (b) if an object is readable at least on the level obfuscate, then its containing object (if any) must also be visible (at least on the level obfuscate). All of these constraints have a converse, e.g. if an object is not visible (read permission level is at most deny), then any contained objects have their read permission level at deny as well.
Apart from the strong dependencies discussed above, the concept of weak consequences were also introduced in [10], to express defaults rather than strict implications. For example, all contained elements and attributes of a visible object should also be made visible by default -unless there is another reason to deny the read permission. Also, if the read permission for an object is known to be at most obfuscate, its write permission must be at most dangle as a strong consequence, but (weak consequence) it should be deny by default, unless specifically overridden.
Example 3. Fig. 3 depicts the effective permissions of the running example for the Pump Control Engineer. As c2 expresses protected IP, read and write operations are denied for the composite c2 and its contents, visualized by dashed borders in case of objects and dashed edges in case of references. On the other hand, the control module ctrl1 needs to be modifiable, therefor also visible (strong dependency) denoted by RW in a square. As ctrl1 needs to be visible, its container c1 and also the root module root need to be visible at least in an obfuscated way (strong dependency)
Listing 1 Queries for Access Control Rules denoted by O in squares. There are no explicit restrictions related to the attributes of control module ctrl1, so they inherit visibility from the object asset (weak consequence).
Using the vocabulary introduced in Sec. III, we now briefly revisit the rule-based access control solution and the nonincremental conflict resolver introduced by [10]. More detailed descriptions with concrete examples can be found in the referenced paper.
The design goals were to allow the policy engineer to declaratively, concisely but also flexibly express permissions for a large number of assets in the form of rules. This was achieved by providing a (terminating, deterministic) algorithm that interprets these rules and resolves conflicts among them (also taking into account the defaults), yielding an effective permission function that meets the intentions of the policy engineer and satisfies the dependencies among assets.
In [6], we introduced a rule-based access control approach, where the rules are defined by graph queries (model queries). Such a query is essentially a formula that can be evaluated on the model. When a query is evaluated, the results consist of a set of pattern matches. Rules grant or deny read and write permissions to the assets identified by the pattern matches of a query. Of course, a rule may only affect a subset of users, so a selection of users/groups is given as well. Finally, a priority class π ∈ Π is given as well, according to which conflicts are resolved: the higher priority rule overrides the lower priority one according to the total order of Π. To unburden the author, the order of rules in the policy may be taken as a default assignment of priority classes.
To summarize, an access control rule in the policy consists of a set of affected users/groups, a model query to identify affected assets, a priority class π ∈ Π, an affected operation, and an upper or lower bound on the permission level of that operation.
We allow for compound rules as concise syntactic sugar, where the policy engineer can specify more than one rule (corresponding to the above structure) in one go. For instance, it shall be possible to set both read and write permissions to deny, or to set the upper and lower bound of a read permission to obfuscate simultaneously.
The conflict resolution process of one user is independent from any other users. Therefore in the following sections, we consider permissions from the perspective of a single user only, and omit the user identity from the subsequently introduced structures. Example 4. Lst. 1 specifies the graph queries for access control rules in VIATRA syntax. Pattern pumpControlPattern selects all control module of type ::Pump while pattern propectedIPPattern queries the composite modules where the protectedIP is to true.
The policy described in Lst. 2 using the syntax introduced in [10] refers these graph pattern to specify access control rules. Rule accessModule allows the write operation of modules identified by pattern pumpControlPattern and rule hideModule denies the read operation of modules selected by pattern propectedIPPattern. Priorities of the rules are 1 and 2, respectively.
The policy specifies the global default that all the assets are unreadable and unmodifiable. Rule accessModule assigns read permissions to objects ctr1 and ctrl2 which is the result set of pattern pumpControlPattern) while rule hideModule denies the read permission of c2 the result set of pattern propectedIPPattern.
During the process of conflict resolution, the algorithm maintains a set of (typically conflicting) direct and indirect consequences of the access control rules.
We define a permission set as a set of judgments, where each judgment j is a tuple j = a, o, p, ψ, π , where a ∈ Assets is an asset, o ∈ {R, W } is an operation (read or write) to be performed on the asset, p ∈ Levels o is a permission level associated with the operation, ψ ∈ Ψ = {>, <} indicates whether the judgment puts that permission level as an upper respectively lower bound for the final permission decision, and π ∈ Π is a priority class.
A valid permission set is complete, i.e. for each asset and operation, it must contain at least one upper bound and one lower bound judgment, and by the ordering of permission levels, the lowest (strictest) upper bound must not be higher than the highest (strictest) lower bound.
The initial permission set is obtained from rules and defaults. For all assets and operations, default permissions are included as a pair of judgments (one upper bound, one lower bound, both with the same permission level), with a priority class that is lower than the priority of any query-based rule; this ensures completeness. For each match of the queries of security rules that apply for the user, an upper or lower bound judgment is added; the asset is given by the pattern maftch, and the operation, priority class and permission level are determined by the rule header.
The goal is to derive the resolved permission set, where the highest (most permissive) lower bound is equal to the lowest Table I: Initial Judgments of the example Rules obj(ctrl1,Control), W, allow, <, 1 obj(ctrl4,Control), W, allow, <, 1 obj(c2,Composite), R, deny, >, 2
Table II: Global Defaults on Control Module ctrl1 obj(ctrl1,Control), R, deny, <, 0 obj(ctrl1,Control), R, deny, >, 0 obj(ctrl1,Control), W, deny, <, 0 obj(ctrl1,Control), W, deny, >, 0 upper bound for each asset and operation (thereby identifying a single permission level as the effective permission), and there are no conflicts (neither directly nor indirectly though dependencies) between the judgments.
Example 5. The initial permission set obtained from the evaluation of access control rules accessModule and hideModule is collected in Table I. Global defaults deny all access with 4 judgments per asset (both bounds (>, <) and operations (R,W) set to deny), e.g. the default judgments of the control module ctrl1 are listed in Table II.
In Sec. III-C we discussed how the requirement of internal consistency introduces dependencies between the permission levels of different assets and operations.
As a judgment may impose dependency constraints on other assets or operations, its consequences can be propagated and directly represented as additional judgments on foreign asset/operation pairs. Using the propagated consequence judgments, all indirect conflicts can be transformed into local conflicts. The latter means that the conflict is expressed as two directly contradicting judgments for the same asset and operation, as opposed to dependency-driven indirect conflicts between judgments at different assets of operations. It was discussed in [10] how consequence propagation makes focusing on local conflicts sufficient.
For judgment j = a, o, p, ψ, π of bound ψ ∈ Ψ = {>, <}, with a dependency on asset and operation a , o , the propagated strong consequence judgment is denoted as j a ,o := a , o , l, ψ, π where l is the bound associated with p by the Galois connection described in Sec. III-C.
Extending the above notion, is also possible to propagate weak consequences that encapsulate a default effect of a given judgment, not a necessary condition. Unlike its strong counterpart, a weak consequence does not inherit the priority of the original judgment, but is assigned a lower priority instead, and may be overridden by more dominant judgments without conflicting with the original judgment. It can be formally captured as j * a ,o := a , o , l * , ψ, π * . It was proposed in [10] to assign a priority class to these weak consequences that is lower than the priority of any user-specified rule, but higher than the priority of global defaults that such a weak consequence may override.
Example 6. The judgment obj(c2,Composite), R, deny, >, 2 obtained from the rule hideModule needs to be propagated to the contained objects of composite c2 as strong dependency. Hence, new judgments appear with exactly the same priority, operation, permission level and bound, namely the judgments obj(ctrl3,Control), R, deny, >, 2 and obj(ctrl4,Control), R, deny, >, 2 . However, the new judgment obj(ctrl4,Control), R, deny, >, 2 is in local conflict with the judgment obj(ctrl4,Control), R, allow, <, 1 obtained from the rule accessModule (see Table I) as they refer to the same asset and operation and contradict on the permission bound (at least allow vs. at most deny).
Take any two judgments that are in conflict. Without loss of generality, we may assume that one must dominate the other via its higher priority class (see [10] for the unimportant nuance of conflicts within the same priority class). Due to the consequence propagation introduced in Sec. IV-C, it is enough to consider local conflicts, as any conflict will manifest itself somewhere as a local conflict. Therefore we consider pairs of judgments on the same asset and operation, where one is an upper bound judgment, and the other is an incompatible lower bound judgment with different priority.
A resolution step takes two judgments that are in a local conflict, and modifies the dominated judgment to make it compatible with the dominant judgment. For locally conflicting judgments j = a, o, p, ψ, π and j = a, o, p , ψ , π with π > π the conflict resolution replaces j with j = a, o, p, ψ , π . Executing such a step transforms a permission set to a different one.
Observations on the resolution step: (a) j relaxes j , i.e. upper bounds are raised when replaced, while lower bounds are lowered. (b) j is guaranteed by the construction to be non-conflicting with j. (c) The resolution step upholds the completeness of the permission set.
Example 7. In Ex. 6 , a local conflict is introduced by propagation of strong dependency. Due to domination, the judgment obj(ctrl4,Control), R, deny, >, 2 with higher priority relaxes the judgment obj(ctrl4,Control), R, allow, <, 1 to obj(ctrl4,Control), R, deny, <, 1 .
The non-incremental resolution process (see Alg. 1) proposed in [10] iterates over judgments in the order of dominance (i.e. highest priority first), to propagate their consequences (also the weak consequences, unless contradicted by a previously processed judgment) and resolve any local conflicts that are detected.
The analysis in [10] shows that this process always terminates, yields a deterministic (confluent) result regardless of the choice of unprocessed dominant judgment, and the result is a complete and consistent effective permission set.
Algorithm 1 The resolution process of [10]
In Sec. IV, we presented the algorithm of [10] for obtaining the effective permissions from the nominal permissions explicitly assigned by the access control rules of the policy. The algorithm can be run on a state of the model to produce the effective permissions of all model elements. This is an adequate solution for the offline collaboration scenario, which is characterized by infrequent commit actions at the end of long transactions, which may change an arbitrarily large part of the model. And even if the change themselves turn out to be relatively small, the complexity of processing the commit is at least proportional to the size of the model anyway, unless a sophisticated fine-grained diff solution is applied.
On the other hand, online collaboration is characterized by frequent and short transactions, each of which change only a small part of the model. In case of larger models, response times would suffer greatly if the entire model had to be re-processed upon each small change. Therefore, we aim to obtain the effective permission function by an incremental computation.
The evaluation of access control queries and the actual enforcement of permissions is also performed incrementally [6]. It would seem natural to try to express the conflict resolution and derivation of effective permissions as model queries, and use the same technology [31], [5] that already provides the incremental evaluation of access control queries.
In the following, we describe our efforts to reformulate the algorithmic conflict resolution process into a declarative computation. We use the formalism of recursive graph queries (Datalog [16]), specifically the VIATRA syntax.
For the sake of simplicity, the following discussion will focus on object assets only. The conflict resolver takes the following inputs (extensional relations in Datalog parlance):
• The explicit judgments that are immediately obtained by evaluating the access control rules in the policy; as mentioned above, each match of the associated model query of the rule will yield a judgment (in the initial permission set). • Low-priority judgments corresponding to global defaults (can be merged with the former). • Relations describing the connections between assets, in order to enable the propagation of consequent judgments. For instance, in case of object facts, a binary relation describing the containment hierarchy is necessary. From these extensional relations, the following incrementally maintained queries (intensional relations) are derived (see also Lst. 3): judgment matches all inferred judgments j = a, o, p, ψ, π , computed as the union of explicit judgments, the strong and weak consequent judgments, and the relaxed forms of dominated judgments. relaxedJudgment identifies judgments that are dominated (see next query), and computes their relaxed form (inheriting the bound of the dominant judgment). domination identifies the judgments in local conflict (sufficient as per Sec. IV-C) and the dominant one among them; this query matches pairs of dominating and dominated judgments in local conflict, respectively j = a, o, p, ψ, π and j = a, o, p , ψ , π , that are defined on the same asset and operation, with the dominating judgment having higher priority (π > π ) and the dominated bound contradicting it (p ψp for ψ ∈ Ψ = {>, <}, as expressed by helper pattern permissionOutOfBound). For efficiency, only effective judgments (see next query) are considered for the role of the dominating judgment. effectiveJudgment matches any judgment that is not dominated at all by any judgment, i.e. there is no corresponding match of the domination query. Note that this is a negative composition. strongConsequence computes the propagated consequences of effective judgments; it matches pairs of judgments j = a, o, p, ψ, π and j = a , o , p , ψ , π where j is an effectiveJudgment and j = j a ,o . For strong consequences, π = π is also required. The results are computed as a union of cases, two for each kinds of dependency; one where a dominant lower bound on a dependant propagates a lower bound consequent judgment to the dependee asset, and one where a dominant upper bound on a dependee propagates an upper bound consequent judgment to the dependant asset. In case of object assets, such dependencies are found between the read and write operations of the same asset, and between contained and container objects (see Sec. III-C). weakConsequence is constructed similarly, except the consequent has a constant, low priority.
Note that for a given asset and operation, in addition to the strictest effective upper or lower bound, there can additionally occur less strict, superfluous judgments. It is possible to eliminate based on subsumption by stricter effective judgments. If subsumed judgments are then eliminated from the essential judgements, then their consequences won't be propagated, and some computational cost can be saved. The simplest solution is probably to adjust domination so that it does not check whether the bound direction of the dominated judgment is opposite to the dominant one (i.e. remove the last line of domination in Lst. 3), then in addition to actual dominations, it will also match most such subsumed judgments (except for the case where a judgment is subsumed by another one in the same priority class).
The effective permission function is finally obtained as the result set of the effectiveJudgment query, where the strictest lower and upper bounds will coincide (see proof in [10]). Let us now investigate the correctness of this solution.
Proposition: This group of queries yield the same effective permission set as Alg. 1.
Proof sketch: One has to consider the way of determining the set of effective judgments, as the rest follows fairly trivially. The original algorithm iteratively selected the highestpriority yet-unprocessed judgment and designated it as an effective judgment (by putting it into the processed set). By contrast, here judgments are considered effective when they are not dominated by any other judgment. It takes some thinking to see that the two conditions yield the same results. We use downwards induction by priority class; assume that the two versions of the effective permission set are equivalent above priority class π. When the original algorithm selects a dominant judgment j of priority π as the new effective judgment, the priority-based ordering ensures that there are Figure 4: Dependency Graph of the Naive Queries no unprocessed judgments in the permission set that could dominate it, and of course already processed judgments are not in conflict with j and thus do not dominate it (otherwise j would have been relaxed and removed earlier when they were processed); consequently, the effectiveJudgment query would match j. Conversely, if the effectiveJudgment query matches the judgment j of priority π, that means no other higher-priority effective judgment dominates it, therefore (by the induction hypothesis) the original algorithm never eliminates it from the permission set, and it is eventually selected as an effective judgment.
A significant flaw of the naive reformulation in Sec. V-B is revealed when we consider how the results of these queries are derived from each other.
Not counting extensional relations, the query judgment derives from relaxedJudgment, strongConsequence and weakConsequence as depicted in Fig. 4. The latter two also derive their results from effectiveJudgment. The relaxedJudgment references domination, while domination uses judgment and effectiveJudgment. Finally, effectiveJudgment is computed from judgment, permissionOutOfBound a negation of domination.
It is immediately obvious that this is a recursive query structure, e.g. judgment refers indirectly to domination which refers to judgment again. Fortunately, it is possible to evaluate recursive queries (there are even multiple incremental strategies [17]).
However, these strategies require a property of the query structure called stratification [16], which the reformulated conflict resolver does not exhibit. Informally, a Datalog program is stratified if there are no negations used in the cyclic references between predicates (i.e. relations or patterns). In our case, a counterexample would be effectiveJudgment negatively referring domination, which in turn uses effectiveJudgment.
Typical query engines only handle stratified query structures, as non-stratified ones do not even have a single accepted semantics [16], and 2-valued semantics are often not possible. See for instance the famous example of a non-stratified Datalog program "this sentence is a lie".
Fortunately, there are a few relaxations of the criteria for stratifiability. Recursions can still have definite (2-valued) semantics (and evaluation algorithms) if they are locally [21], modularly or at least weakly [24] stratifiable. Informally, these relaxed notions of stratification investigate the dependencies between individual tuples (so-called ground atoms) as opposed to whole relations; it is sufficient if there is no negation in circular references between tuples (in the ground Datalog program). The subtle differences between local, modular and weak stratification manifest themselves in the ways how already known facts are used to cull unnecessary (e.g. unsatisfiable) references before cycles are evaluated to be negationfree; the formal details are not explored here.
Although the query structure of Sec. V-B is neither stratifiable nor locally stratifiable, it is weakly and even modularly stratifiable. The reason is that the only occurrence of negation is between predicates effectiveJudgment and domination; however, a judgment may only be dominated by higher-priority judgments. After eliminating judgment pairs from domination for which the priority comparison constraints fail (which is allowed in modular, but not in local stratification), we are left with no tuple-level negative cycles.
Although modular stratifiability shows the existence of 2valued semantics, it is not necessarily compatible with all evaluation strategies, especially incremental ones. Even if a given strategy is guaranteed to yield correct results, concrete tools such as VIATRA may pessimistically refuse to evaluate a query structure that is not stratifiable (as detecting e.g. local stratification may be undecidable [21]).
Beyond the question of stratification, the recursive query structure also introduces performance challenges.
Imagine a single-root containment hierarchy consisting of n objects altogether. Suppose we define k separate access control rules in k different priority classes, each of which applies to the root object, such that every other rule (those in even priority classes) sets the read permission to allow, while the rest of the rules set it to deny. In this case, query evaluation performance depends greatly in the order of computations, even if the end result is guaranteed to be the same.
If the query engine happens to propagate tuples in the ascending order of the priorities of corresponding judgments, then first all n objects are set to invisible by the lowest priority rule, then the next rule is found to dominate the previous one and all n objects are made visible again, etc., until finally the effective permissions are obtained in O(n * k) steps.
If, on the other hand, the query engine propagates tuples in the order of descending priority, then the final read permissions are set immediately in the highest priority class , and then the rest of the rules are merely dominated, but never propagated. This leads to O(n + k) steps of computation.
Altogether, if the evaluation follows the original procedure in Alg. 1 and processes high-priority rules first, then (strong) consequences are never overruled, minimizing the amount of work to be done. Unfortunately, declarative queries can be executed with an arbitrary computation order chosen by the query engine. Ordering by rule priority is a highly applicationspecific optimization, and there is no standard way to make a query engine such as VIATRA aware of it.
The previous sections identified two significant issues with the naive reformulation of the access control conflict resolution problem, stratifiability and performance. Still, we do not give up on using a general-purpose query tool to provide incremental evaluation; instead, we propose a way to modify the query structure such that it avoids both problems.
Fortunately, the solutions to both issues involve the same weak ordering of tuples based on priority class. We therefore propose to apply partial grounding, where given a policy of k priority classes, we substitute all k values into each priority variable of the query, blowing up each predicate into k disjoint shard predicates (k 2 in case of domination where two judgments of different priority are involved). Priority comparisons can be statically evaluated in this case.
There is one corner case where negative recursion still persists, despite sharding the predicated according to priority: the effectiveJudgment query for a given priority class negatively calls the domination relation for the same priority (of the dominated judgment), which is in turn derived from dominated judgment matches of that priority, that on one branch rely on strongConsequence matches, which call effectiveJudgment, all of the same priority level. We propose the following solution: we replace domination with dominationBy that will no longer imply that a dominated judgment exists; it merely asserts that an effective judgment exists at a given priority, that would dominate any lowerpriority judgment at the given asset and the given permission bound. This way the negative recursion is averted.
For priority class π, we define the following predicates (see also Lst. 4): judgment π matches all inferred judgments j = a, o, p, ψ, π of priority class π, computed as the union of explicit judgments in class π, the strong and weak consequent judgments in class π, and the relaxed forms of dominated judgments in class π. relaxedJudgment π identifies judgments of priority class π that are dominated (see next query) by any priority π > π, and computes their relaxed form (inheriting the bound of the dominant judgment). dominationBy π will match (independently of the existence of any dominated judgments) all effective judgments j = a, o, p, ψ, π ∈ effectiveJudgment π of priority π and all potential bounds p for the corresponding asset and operation that would be dominated by it in local conflict (p ψp for ψ ∈ Ψ = {>, <}). effectiveJudgment π filters judgment π to those judgments that are not dominated, i.e. there is no corresponding match of dominationBy π for any π > π. strongConsequence π computes the propagated consequences of effective judgments at class π.
weakConsequence π analogously.
In the above queries, the priority class comparisons "π > π" are statically evaluated, and the generated disjunctions only include the clauses where the result is true.
With this solution, the query structure is now stratifiable, addressing the concerns of Sec. V-C. Also, a query engine evaluating (or updating, in case of incrementality) it can process individual predicates in their topological order, which addresses the issue raised in Sec. V-D.
Once stratification is achieved, let us take a look at what forms of (positive) recursion remain, keeping in mind that these no longer pose an obstacle to incremental matching. First, relaxedJudgment π contributes to judgment π and vice versa. Note that there is no circularity on the tuple level, as the original dominated judgments (as well as subsumed ones) are always farther from the effective judgment than their relaxed versions. Moreover, judgment π is partially expressed from strongConsequence π , which finds consequences of effectiveJudgment π that of course uses judgment π ; in this case it depends on our internal consistency constraints whether consequences can cyclically justify each other (in the simple cases described in this paper, they can't). In application scenarios where we know that there are no tuple-level cycles, the fast default algorithm suffices to efficiently evaluate recursive queries; for other cases, VIATRA provides the more complex DRed algorithm [17] as well, guaranteeing correct incremental maintenance for any stratified query structure.
Listing 4 Refined solution in VIATRA syntax (extracts) Finally, a note on space and time cost: a straightforward upper bound on the size of the match sets can be obtained by taking the Cartesian product of the domains of query variables. In our example, there are 3 priority classes, 2 controlled operations, 3 permissions levels (both for read and write), etc.; in the end, for a fixed security policy, the upper bound is proportional to both the model size (number of assets) and the number of active (e.g. simultaneously connected) users. In the non-recursive case, incrementally maintaining the result of queries has time complexity proportional to the size of the change (in the inputs, in the results, and also in any internal cache structure), regardless of the size of the unchanged parts. For recursive queries, such a straightforward linear relationship can not always be established; performance analysis and improvements (beyond the considerations of Sec. V-D) are left as future work.
File-based Access Control. Off-the-shelf file systems typically require resources (files and folders) to be explicitly labeled with permissions that take the form of an Access Control List (ACL), or the simplified form user/group/others. An ACL consists of entries (judgments) regarding which user/subject is granted or denied permission for a given operation. Conflict resolution is usually priority-based (first entry applies) within the access control list, and restrictive among type II and type III conflicts (e.g. contents of a hidden folder cannot be seen, regardless of ACLs inside).
File-based solutions can be directly applied to MDE, but cannot provide fine-grained access control, where different parts of a model file have different permissions. Our policies are fine-grained, use implicit rules (so that model elements do not have to be explicitly annotated with judgments, which is difficult to manually maintain as the model evolves), and respect the modeling-specific challenges of consistency (such as permission dependencies of cross-references); all the while being more flexible in the conflict resolution method.
Access Control for XML Documents. A number of standards such as XACML [15] (OASIS standard) provide fine-grained access control for XML documents. These type of documents are similar to models in a way, that they consists of nodes with attributes that may contain other nodes. XACML provides several combining algorithms to select from contradicting policies. Similarly to our solution, it may use external and internal priorities together (ordered-(deny/permit)-overrides) or only internal priorities (unordered-(deny/permit)-overrides). In [12], fine-grained access control is formalized using XPath for XML documents, which claims that the visibility of a node depends on its ancestors, thus when a node is granted access, then access is also granted to its descendants. However, other dependencies are not discussed related to XML Documents, while our approach [10] also considers e.g. cross-references.
Context-aware Access Control RDF Stores. Models can be persisted into triples to store them in triple or quad stores (Neo4EMF [4], EMF Triple). Graph-based access control is a popular strategy for many RDF stores (4store [14], Virtuoso , IBM DB2) developed for storing large RDF data. In case of RDF, fine-grained specification of access control permissions are defined at triple level. In [1], a graph-based policy specification language proposed over SPARQL [22], but resolution of contradicting rules are not discussed. Amit Jain et. al. [18] propose an access control model for RDF and a two-level conflict resolution strategy that also takes inconsistencies into account similar to our solution. But, it uses only restrictive resolution without any configuration of default values or priorities between rules.
Collaborative Modeling Environments. Currently, finegrained access control is not considered in the state of the art tools of MDE such as MetaEdit+ [30], VirtualEMF [8],
WebGME [19], EMFStore [28], GenMyModel [2], Obeo Designer Team [20], MDEForge [3] or the tools developed according to [13]. See also the broader survey in [23].
The generic framework CDO [27] (used e.g. in [20]) provides both online collaboration and role-based access control with type-specific (class, package and resource-level) permissions, but no facility for instance level access control policy specifications. However, there is a pluggable access control mechanism that can specify access on the object level; it should be possible to integrate fine-grained solutions such as the currently proposed system.
The collaborative hardware design platform VehicleFORGE stores their model in graph-based databases and has an access control scheme TrustForge [9] that uses an implementation of KeyNote [7] trust management system. This system is responsible for evaluating the request addressed to the database, which can be configured in various ways. It supports unlimited permission levels and it is also able to handle consistency constraints by adding them as assertions. Conflict resolution strategies are not discussed. AToMPM [26] provides finegrained role-based access control for online collaboration; no offline scenario or query-based security is supported, though. Access control is provided at elementary manipulation level (RESTful services) in the online collaboration solution of [11].
To support rule-based fine-grained access control under internal consistency constraints, we have taken a significant step towards efficient online collaboration by reformulating the permission assignment problem into a special class of Datalog programs that can be incrementally evaluated (taking advantage of the priority hierarchy). We have also sketched a proof of correctness for the reformulation. As a quick proof of concept 1 , we have implemented and evaluated queries according to this scheme for an example policy.
In the future, we plan to (a) implement an automated translation from an arbitrary policy to such a query structure, (b) set up benchmarks to study (and, if necessary, improve) the performance of the solution in practice, (c) investigate incrementality with respect to policy changes.