Abstract
We introduce a new class of analysis problems, called Scenario Finding Problems (SFPs), for security-sensitive business processes that – besides execution constraints on tasks – define access control policies (constraining which users can execute which tasks) and authorization constraints (such as Separation of Duty). The solutions to SFPs are concrete execution scenarios that assist customers in the reuse and deployment of security-sensitive workflows. We study the relationship of SFPs to well-known properties of security-sensitive processes such as Workflow Satisfiability and Resiliency together with their complexity. Finally, we present a symbolic approach to solving SFPs and describe our experience with a prototype implementation on real-world business process models taken from an on-line library.
Introduction
Organizations rely on Business Process Management (BPM) [37] to achieve certain business objectives by orchestrating workflows, which are collections of sequences of tasks executed by human or software agents. An increasingly important class of workflows is that of security-sensitive workflows [2], in which task execution constraints are complemented with an authorization policy (defining which users can execute which tasks) and a set of authorization constraints (further restricting which users can execute some sub-sets of the tasks). One of the most important problems for security-sensitive workflows is the Workflow Satisfiability Problem (WSP) [10], which consists of checking if there exists an assignment of users to tasks such that at least one task execution sequence in a workflow successfully terminates while satisfying all authorization constraints and the authorization policy.
Several papers (see, e.g., [10,15,16,36]) have provided solutions to the WSP, which are becoming less and less satisfactory because of the recent trend in BPM of collecting and reusing large numbers of business process models [18,35,39]. For instance, SAP HANA Workflow1
Techniques for solving the WSP can also be used to solve SFPs; unfortunately, this has a very high computational cost because of two reasons. First, WSP is NP-hard already in the presence of one SoD constraint [36]. Second, techniques for the WSP are not able to exploit the fact that execution and authorization constraints are fixed and only the authorization policy changes at deployment time. To overcome these limitations, the paper makes the following contributions.
We give precise statements of four SFPs together with a discussion of their relationships with the WSP (Section 3). We describe methods to automatically solve the four SFPs by adapting the technique for the synthesis of run-time monitors for the WSP developed in [6] (Section 4). We validate our solutions on real-world examples from a library of reusable business process models (Section 5).
The idea underlying our approach can be summarized as follows. Model checking is a technique for determining whether a (formal) model of a system satisfies a given property. If the property is false in the model, model checkers typically produce a counterexample scenario, which is then used by developers to fix bugs in the design of the system. To solve a SFP, we use the capability of model checkers to return counterexamples as follows. We formally represent security-sensitive workflows as symbolic transition systems following [6]. The symbolic model checker is then asked to find a counterexample to the property that the system is not terminating. Indeed, the returned counterexample (if any) is precisely an execution scenario solving the SFP. Since we are interested in finding all execution scenarios, we modify the model checker in order to compute all counterexamples, not just one. We represent a set of counterexample scenarios by using a scenario graph, which allows us to compactly encode all possible interleavings of tasks in a workflow.
The crux of our approach is that the model of the security-sensitive workflow in input to the symbolic model checker only contains the constraints on the control flow and the authorization constraints while it abstracts away from the authorization policy. In this way, the scenario graphs computed by the model checker can then be refined with respect to an authorization policy associated to a particular deployment context. The refinement is performed by a depth-first search of the scenario graph to prune those scenarios that do not satisfy the authorization policy used in the deployment context under consideration. When considering resiliency, this is combined with a (heuristic) method to generate subsets of users not containing k users (by adapting a result from [24]) in order to find scenarios guaranteeing the termination of a workflow despite the absence of k users.
This paper is an extended version of [19], with the main additions being the definition of two new SFPs (involving resiliency and constrained scenarios) in Sections 3.3 and 3.4; an expanded description of the solution to the WSP in Section 4.2; new experiments in Section 5; an extensive comparison with related work in Section 6.1; and a description of future work in Section 6.2.
Let T be a finite set of tasks and U a finite set of users. An execution scenario (or, simply, a scenario) is a finite sequence of pairs of the form
Given a workflow
The notions of eligible and authorized scenarios were adapted from [15].
There are various ways to specify security-sensitive workflows; we illustrate one of the most used methods by means of an example.
A typical example of a security-sensitive workflow has the goal of requesting trips for employees in an organization. It is composed of five tasks: Trip request (
It is also required that each task is executed under the responsibility of a user who has the right to execute it according to some authorization policy. To prevent frauds, five authorization constraints – called Separation of Duty (SoD) in the literature; see, e.g., [10] – must also be enforced: each one of the following pairs of tasks must be executed by distinct users in any sequence of task executions of the workflow:
TRW in (extended) BPM notation.
This workflow can be modeled in a graphical notation such as BPMN [30] as shown in Fig. 1: the circle on the left represents the start event (triggering the execution of the workflow), whereas that on the right the end event (terminating the execution of the workflow), tasks are depicted by labeled boxes, the constraints on the execution of tasks are shown as solid arrows (for sequence flows) and diamonds labeled by + (for parallel flows), the fact that a task must be executed under the responsibility of a user is indicated by the man icon inside a box, and the SoD constraints as dashed lines labeled by ≠.
We use the TRW introduced in the example above to illustrate the main notions in the paper.
Given a workflow
We use Example 2.2 to show an instance of this problem and the solution. A simple situation in which the TRW in Example 2.1 can be deployed is a tiny organization with a set
Reuse in Business Process Management has been an important topic of research and industrial application; see, e.g., [17,22]. The reuse of business process models increases the productivity of designers and the quality of the models. A crucial step in reusing process templates is their deployment. Helping customers to assess whether the process instance is suitable to their needs is indeed fundamental. For example, checking the existence of execution scenarios for a deployed security-sensitive workflow – i.e. after adding a particular authorization policy – can reassure customers about the business continuity of the process. Automating the identification of such scenarios is of particular importance when a library of process templates are available and are to be re-used in different organizations adopting different authorization policies. As mentioned above, it is possible to pre-compute – once and for all – the set E of eligible scenarios, i.e. those scenarios satisfying the authorization constraints, associated to a security-sensitive workflow in a library (we will describe how to compute and compactly represent this set in Section 4 below). We are then left with the problem of finding those scenarios in E that are still computable as soon as an authorization policy becomes available (and possibly satisfying some additional properties).
Basic scenarios
We begin by defining a basic version of our scenario finding problems, whose definition (and solution) will help us in understanding (and solving) more complex problems.
(Basic Scenario Finding Problem (B-SFP)).
Given the finite set E of eligible scenarios according to a set C of authorization constraints in a workflow
Let us consider the TRW. If
A scenario η solving the B-SFP is also a solution of the WSP and vice versa. So, in principle, to solve the B-SFP for a workflow
A better approach to solve the B-SFP is to consider each eligible scenario
A refinement of B-SFP is to search for (eligible and) authorized scenarios in which a “minimal” set of users occurs. Formally, let η be a scenario in a workflow
(Minimal User-Base Scenario Finding Problem (MUB-SFP)).
Given the set E of eligible scenarios according to a set C of authorization constraints in a workflow
Let us consider again the TRW together with the set U of users, the set E of eligible scenarios, and the authorization relation
An approach derived from that of solving the B-SFP can also solve the MUB-SFP. We consider each eligible scenario
Resiliency in workflow systems concerns the question of whether a workflow is still satisfiable even if a number of users is absent for an instance execution. It is an important property of workflows and authorization relations, since it indicates the likelihood of the workflow terminating even in adverse conditions.
There are several possible definitions of resiliency. The most obvious one is to fix a set
(Statically k-resilient set of scenarios).
Given a workflow
Notice that resiliency is defined up to k since a k-resilient set of scenarios is clearly also
We are now ready to introduce the problem of finding sets of resilient scenarios.
(Statically k-Resilient Scenario Finding Problem (SkR-SFP)).
Given the set E of eligible scenarios according to a set C of authorization constraints in a workflow
Let us consider again the TRW together with the set U of users, the set E of eligible scenarios, and the authorization relation
To solve the SkR-SFP, an obvious strategy is to initialize the set H of k-resilient execution scenarios to the empty set, generate all subsets of users with size
Another interesting problem is to find the maximal value
Another problem extension is how to achieve k-resiliency while minimally changing the authorization policy, i.e. adding as few
The three problems (B-SFP, MUB-SFP, and SkR-SFP) introduced above accept as solutions unconstrained scenarios, i.e. scenarios where any authorized user can execute any task and any allowed control path can be taken (e.g., any interleaving of parallel tasks is possible and any branch of a conditional is equally likely to be executed). Sometimes, policy designers may be interested in finding scenarios satisfying certain properties, e.g., scenarios in which only certain authorized users can execute certain tasks or some control-flows can be executed. For instance, the designer may want to investigate scenarios in which the test of a conditional evaluates to true or in which only certain users perform some tasks. We use constraints to specify the properties that scenarios must additionally satisfy in the constrained versions of the three problems above. The constraints specified by the designer are represented as predicates and are collected in a set Γ.
We are now in the position to generalize the B-SFP problem by defining its constrained version as follows.
(Constrained Scenario Finding Problem (C-SFP)).
Given the set E of eligible scenarios according to a set C of authorization constraints in a workflow
Let us consider again the TRW together with the set U of users, the set E of eligible scenarios, and the authorization relation
Similar generalizations of the MUB-SFP and the SkR-SFP are possible, thereby obtaining their constrained versions that we call C-MUB-SFP and C-SkR-SFP, respectively. More precisely, a solution to the C-MUB-SFP is a scenario that uses a minimal number of users and makes all the predicates in the set of constraints evaluate to true. A solution to the C-SkR-SFP is a k-resilient set H of scenarios such that each scenario in H makes all the predicates in the set of constraints evaluate to true.
As we will see in Section 4.2, the procedures used to solve the unconstrained versions of the scenario finding problems can be lifted to solve also their constrained version.
We now explain our approach to solve the three problems (B-SFP, MUB-SFP, and SkR-SFP) introduced in Section 3. The procedure to solve the B-SFP (Section 4.2) is used as a sub-procedure in those tackling the MUB-SFP (see again Section 4.2) and the SkR-SFP (Section 4.3). Preliminarily (Section 4.1), we recall the technique in [6] to synthesize run-time monitors for the WSP. Besides creating monitors for the WSP, this procedure is based on a (symbolic) model checking algorithm capable of generating a compact data structure representing scenario graphs (recall the discussion in the Introduction) which allow us to compactly encode all possible interleavings of tasks in a workflow. Both the run-time monitors and the data structure representing scenario graphs are used by the procedure to solve the B-SFP.
The procedures to solve the constrained versions of the three scenario finding problems are illustrated in Section 4.4.
Synthesizing monitors for the WSP
The technique in [6] is key to our approach as it provides us with a compact data structure to represent the set of all eligible scenarios in a workflow, which is crucial for the design of an efficient solution to SFPs. It takes as input the specification of a security-sensitive workflow (e.g., the BPMN in Fig. 1 for the TRW) together with the specification of an authorization policy (such as the relation
Fig. 2 shows the (extended) Petri net corresponding to the BPM Fig. 1 and the corresponding derived transition system
TRW as an extended Petri net (top) and as a transition system (bottom).
The transitions in
The core of the off-line step of the technique in [6] is the computation of the data structure representing scenario graphs. The symbolic transition system S is taken as input to a model checking procedure which generates a (symbolic) reachability graph
The details of the construction of
A sequence
The crucial property of
Three observations are in order. First, μ is extended to symbolic execution scenarios in the obvious way, i.e. by applying it to each user variable occurring in them. Second, since
An excerpt of the symbolic reachability graph for the TRW is depicted in Fig. 3.
An excerpt of the symbolic reachability graph for the TRW.
The graph is not complete and the formulae labeling the nodes are not shown in the figure for the sake of simplicity.
The graph in the figure is constructed as follows. First, the procedure creates node 1, labels it with the formula
Concerning the labels on the edges of the symbolic reachability graph, in Fig. 3, a task-user pair
To conclude the off-line step, the technique derives a non-recursive Datalog program M (with negation) from the symbolic reachability graph
To illustrate, consider again node 3 in the graph as done in Example 4.2. The Datalog program M will contain the following clause:
We now describe the on-line step which consists of building a run-time monitor for the WSP by taking into account the authorization policy Fig. 4 depicts the monitor program M for the TRW (obtained in the off-line step) combined (in the on-line step) with an authorization policy P specified in Datalog (from a user-task relation
Monitor for the TRW combined with an authorization policy and an execution history. Let us consider again the set of users and the authorization policy discussed in Example 2.2. The relation A run of the monitor program for the TRW
An example run of the monitor derived from the symbolic reachability graph in Fig. 3 combined with the RBAC policy above is shown in Table 1: column ‘History’ shows which facts are added to the set H and column ‘Answer’ reports grant (deny, respectively) when the query in column ‘Query’ can (cannot, respectively) be derived from
Preliminarily, we need to decide how the set E of eligible scenarios and the authorization policy
Two observations are important. First, there are several different sets
Let us consider the TRW with a set U of 6 users. The graph in Fig. 3 is, for the sake of readability, an excerpt of the full symbolic reachability graph showing only a small sub-set of all well-formed paths. The full graph has 46 nodes, 81 edges, and 61 well-formed paths of which 21, 34, and 6 contain 3, 4, and 5, respectively, symbolic users. For instance, notice how the sub-sequence

Solving the B-SFP

Solving the MUB-SFP
We are now ready to describe our technique, depicted in Algorithm 1, to solve the B-SFP. For the time being, let us ignore the additional input set Γ (by setting it to ∅); it will be explained in Section 4.4 below. The main idea underlying Algorithm 1 is to adapt a standard Depth-First Search (DFS) search to explore all well-formed paths in the reachability graph
It is possible to modify Algorithm 1 following the idea discussed after Example 3.2 in order to solve the MUB-SFP. This requires to avoid returning the authorized scenario as soon as we find one (removing the condition
Complexity of Algorithms 1 and 2
The complexity of both algorithms can be derived from that of the standard DFS algorithm, which is
As discussed in Section 3.3, a naive solution to the SkR-SFP requires the enumeration of all sub-sets of the set of users of a given size. Indeed, this is very expensive from a computational point of view. To alleviate this, it is possible to adapt an heuristic proposed in [24] and reduce the number of sets of a given size to be considered. The idea is based on the notion of “dominance” which is defined in terms of which tasks a given set of users can execute. If a set
(Absent set domination).
A user
We are now in the position to adapt the result (Lemma 7) in [24] to avoid the enumeration of all sub-sets of a given size while solving the SkR-SFP.
Let E be a set of eligible scenarios according to a set C of authorization constraints containing only SoD (i.e. ρ is ≠ for each
(Sketch) Assume that
By (1), it is possible to show that if (2) holds (i.e. the problem is solvable after the removal of
Unfortunately, it is not possible to show for an arbitrary set C of constraints that (3) implies (3) with
Lemma 4.1 allows us to avoid enumerating all possible sub-sets of a given size when solving the SkR-SFP by exploiting the dominance relation among sets of absent users in presence of SoD constraints only. (Finding a generalization of the notion of dominance for arbitrary authorization constraints is left as future work.) How this is done is shown in Algorithm 3. In line 1, the variable H which stores the scenarios to be returned is initialized to the empty set. In line 2, the function

Solving the SkR-SFP
So far, we have assumed that the set Γ of constraints taken as input of Algorithm 1 is empty. Here, we consider the situation in which this is no more the case and show how Algorithms 1, 2, and 3 also solve the constrained versions of the B-SFP, MUB-SFP, and the SkR-SFP.
Let us consider Algorithm 1 and how it solves a C-SFP by taking as input a non-empty set Γ of facts, that can be used to drive the search for a scenario with particular characteristics. For instance, one can be interested in authorized scenarios in which a certain user only, say
A more interesting approach is to develop an interactive algorithm where after each step in the search for a solution, the user of the algorithm is asked to enter his or her preferences to which user executes which task and which is the next task to be executed. If he or she does not specify anything, the algorithm picks an arbitrary user and task; otherwise the algorithm checks if the corresponding instance of the WSP is solvable and, if the case, would allow the user to proceed with the exploration.
Since Algorithms 2 and 3 (i.e. the procedures to find the solutions to the MUB-SFP and to the SkR-SFP) use Algorithm 1 as a sub-procedure, they straightforwardly inherit the capability to solve the constrained versions of B-SFP and MUB-SFP.

ITIL 2011 – IT Financial Reporting (abbreviated ITIL).

ISO9000 – Budgeting for Quality Management (abbreviated ISO).
We consider two real-world examples – called ITIL and ISO, shown in Figs 5 and 6 – derived from business processes available in an on-line library provided by Signavio,3
Available at
The goal of this workflow is to report costs and revenues of an IT Service. It is composed of 7 tasks and 2 SoD constraints. Tasks
ISO
The goal of this workflow is to plan for enough financial resources to fulfill some quality requirement. It is composed of 9 tasks and 3 SoD constraints. Tasks
Although none of the workflows comes with an authorization policy, swimlanes (not shown in Figs 5 and 6) suggest that a controlling manager executes tasks
Before invoking our algorithms for solving the SFPs, we need to build the symbolic reachability graph (and the run-time monitor) for each example. We did this by running the implementation of the off-line step (described in Section 4) from [6]. For TRW, the symbolic reachability graph is computed in around a second and contains 46 nodes with 81 edges. For ITIL, the graph is computed in around 3.5 seconds and has 78 nodes with 72 edges. For ISO, graph building takes around 10.5 seconds and has 171 nodes with 669 edges. These timings, as well as all those that follow below, have been obtained by using a MacBook Air 2014 with Mac OS X v10.10.2. The time for deriving the monitor M from the symbolic reachability graph of each example is negligible and thus omitted.
We have implemented Algorithms 1, 2, and 3 (described in Section 4.2) in Python v2.7. The invocation to the Datalog engine at line 13 in Algorithm 1 (and reused in the other algorithms) is implemented with the Datalog engine pyDatalog v0.15.2.
Experiments for the B-SFP, MUB-SFP, and C-SFP
Experiments for the B-SFP, MUB-SFP, and C-SFP
Table 2 shows the findings of our experiments for the B-SFP, MUB-SFP, and C-SFP. Each entry in column ‘Instance,’ describing the input to Algorithm 1 (or its modification to solve the MUB-SFP), is of the form
We report the performance of the implementation of Algorithm 3, to solve instances of the SkR-SFP on the TRW, ITIL, and ISO workflows in Table 3. Column ‘Instance’ shows the workflows used in the experiments. Each one of the columns ‘Time’ reports the time taken (in seconds) to find a solution for
Experiments for the SkR-SFP
Our experiments indicate that the SFPs, their constrained versions, and the algorithms for solving them introduced in this paper fit well with emerging practices for BPM reuse. Whenever a customer wants to deploy a business process by reusing a workflow template, some SFP is solved (if possible) to provide him or her with an authorized scenario showing that a template business process can be successfully instantiated by his or her authorization policy. The efficiency of the proposed approach exploits the fact that the eligible scenarios (resulting from execution and authorization constraints) can be computed once and reused with every authorization policy. In this way, multiple changes to a policy, which are well-known to be costly [25], become much less problematic to handle and customers can even explore and evaluate the suitability of variants of a policy. This is in sharp contrast to the approach discussed in Section 3 (after Example 3.1) that consists of re-invoking an available algorithm for solving the WSP on every task-user pair in a scenario. To illustrate, consider the instance at line 4 of Table 2. Recall that the off-line step for ITIL takes around 3.5 seconds and observe that this is computed once and for all. If, instead, we use the technique to solve the WSP in [6] as a black-box (i.e. without being able to retrieve the symbolic reachability graph computed during the off-line phase), which is common to (almost) all techniques available in the literature, solving the same B-SFP would require almost 30 seconds resulting from re-computing 7 times (corresponding to the 7 task-user pairs in the returned scenario) the same symbolic reachability graph (compare this with the timing of 4.561 seconds reported in the table). This is a significant performance gain despite the small size of the example.
For each workflow, the times shown in Table 3 grow with the number of users (
Discussion
We have introduced four SFPs, discussed their relationships with the WSP, and argued that solving them supports the deployment of business processes in the activity of model reuse. Then, we have described algorithms to solve the four SFPs, based on a previously proposed technique [6] for the synthesis of monitors for the WSP. An experimental evaluation on real-world examples has shown that our techniques can be used in practice at deployment time since they perform the computationally heaviest part (namely, computing the set of eligible scenarios) once and for all when the workflow is designed (and possibly added to a library of business processes) and reuse it with arbitrary authorization policies.
Related work
WSP and scenario finding
Bertino et al. [5] were the first to present a method capable of computing execution scenarios by using logic programming techniques. The practical feasibility of the approach was not assessed as we did for our technique in Section 5. Kohler and Schaad [21] introduced the notion of policy deadlocks (corresponding to situations in which the WSP is unsolvable) and proposed a graph-based technique to compute minimal user bases to help policy designers to avoid such situations. There are some similarities with our approach such as the use of symbolic users, but our work is not limited to RBAC policies as theirs and focuses on business process reuse, which was not considered in [21]. Solworth [34] used an approvability graph to describe sequences of actions defining the termination of a workflow. His technique focused on linear workflows, whereas we support constructs for parallel executions and conditionals.
Many other works provided solutions to the WSP. Crampton [10] considered workflows as partial orders and showed an algorithm to determine whether there is an execution scenario. Wang and Li [36] reduced the WSP to SAT and showed that it is NP-hard even in the presence of simple constraints. Crampton et al. [15] improved the complexity bounds for the WSP and generalized the constraints supported by their solution. Crampton et al. [16] used model checking on a fragment of linear temporal logic to compute execution scenarios, minimal user bases, and a safe bound on resiliency. Yang et al. [38] studied the complexity of the WSP with different control-flow patterns and showed that, in general, the problem is intractable. Basin et al. [4] defined and solved the problem of choosing authorization policies that allow a successful workflow execution and an optimal balance between system protection and user empowerment. As discussed above, most of these solutions cannot be used to solve the SFPs without an unacceptable decrease in performances because they are not able to pre-compute the set of eligible scenarios.
The works in [3,8] separated between an off-line and on-line phase as done in this work and [6] but it was not exploited for business process reuse as we did.
Resiliency
Li et al. [24] introduced the notion of resiliency policies in the context of access control systems, i.e. policies that require the access control system to be resilient to the absence of users. Their work was inspired by the need of forming teams that, even in emergency situations, are able to access all resources in a common pool. They also defined the Resiliency Checking Problem (RCP), which amounts to checking if an access control state satisfies a given resiliency policy. Wang and Li [36] then studied resiliency in workflow systems by identifying three types: static, when users can become absent only before the beginning of the execution of a workflow and stay available during execution; decremental, when users may become absent before or during the workflow instance execution but they cannot become available until the workflow execution is terminated; and dynamic, when users can become absent and available at any given time before and during the execution of the workflow. In [36], Wang and Li studied the relationship between these notions of resiliency and the WSP and showed that checking static workflow resiliency is in NP, whereas checking decremental and dynamic resiliency is in PSPACE. The authors of [36] observed that there are other possible formulations of resiliency that can be of interest. For instance, Mace et al. [26] defined quantitative workflow resiliency, whereby a user wants to know how likely a workflow instance is to terminate. They used specific user availability models based on Markov Decision Processes (MDPs) in which probabilities measure the likelihood that users are available or absent. Mace et al. proposed a method to solve the problem of finding optimal execution scenarios guaranteeing the termination of workflows. Additionally, in [29], the same authors discussed the effects of alternative execution paths on resiliency. This leads to the possibility of a different resiliency value for each path. They defined resiliency variance as a metric to indicate volatility from the resiliency average, claiming that a higher variance increases the likelihood of workflow failure. User availability models were discussed in more details in [27], categorized into non-deterministic, probabilistic and bounded and with several encodings for the PRISM (probabilistic) model checker.4
Crampton et al. [14] reduced the RCP to the WSP and showed how to solve it using a fixed-parameter tractable algorithm for the latter. The RCP differs from the problem of workflow resiliency by considering more parameters (see [36] for details). On the other hand, the RCP is always static, whereas workflow resiliency can be static, decremental, or dynamic. The basic solution in the original paper about RCP [24] is to enumerate all subsets of s users and check for satisfiability (using a solution for
As a first step, we intend to study how to support other forms of resiliency (namely, decremental and dynamic) by extending our approach. We also intend to design new heuristics to support other classes of constraints efficiently in the solution to the SkR-SFP. Afterwards, we identify the following ideas to stimulate further work on the topic of scenario finding techniques to support the deployment of security-sensitive workflows.
Tool integration
Currently, the implementation used to produce the experimental results reported in Section 5 uses a command-line interface where users can run each of the problems on a given workflow specification and policy file. We have developed a tool to generate enforcement monitors for workflow management systems and store them in a repository (along with the reachability graph). The tool was integrated with one of SAP’s platforms for BPM [9]. We would like to integrate the solution to the SFPs into this tool by providing a graphical user interface allowing users to retrieve the workflow and associated reachability graph from the repository, specify a policy, select the desired problems and visualize the solutions in an intuitive way.
Policy synthesis
Another interesting problem to consider is how to automatically synthesize, or suggest changes to existing, authorization policies so that solutions of an SFP are optimal with respect to some criteria, e.g., least privilege [20] or cost/risk [4]. This is related to the Bi-Objective WSP introduced in [13] and briefly discussed above. Using our approach, weights could be associated with each edge in the reachability graph and then instantiate symbolic users in all possible ways (i.e. according to injective functions) so that standard graph search algorithms for finding minimum weight paths can compute optimal solutions. Unfortunately, this naive approach does not scale to medium or large number n of users as the injective functions to be considered grow as the factorial of n. It would thus be interesting to study situations in which the graph can be pruned to achieve sub-optimal solutions.
Run-time adaptation
Two assumptions are very common in the workflow satisfiability and resiliency literature. First, that the control-flow and authorization constraints do not change at run-time. Second, that only humans can be absent during the execution of a workflow, whereas external applications for automated tasks are always available. These are abstractions from real-world executions and we intend to investigate how to solve the SFPs on weaker versions of these assumptions. Considering arbitrary changes to control-flow at run-time is not feasible, but we would like to allow “controlled” deviations, as in [1] and pre-compute eligible scenarios for each of the allowed deviations. User availability models [27] could be adapted to model the availability of external applications and consider resiliency to other kinds of failures.
Footnotes
Acknowledgment
This work has been partly supported by the EU under grant 317387 SECENTIS (FP7-PEOPLE-2012-ITN).
