OLive-M: A SecANet  Use Case for Model-Based Obstruction Solving

Abstract

The OLive-M approach in this chapter and the OLive-L approach in Chapter 5 will illustrate how the SecANet approach presented in Chapter 3 can be applied to handle and resolve obstructions based on a process model or a process log, respectively. In order to complete the workflow in that context, based on indicators captured as costs, a certain yet still compliant degree of violation of safety properties is tolerated. The solutions allow for additional, eventually live, process execution sequences because they widen the behavioral framework restricted by classic IT security in a security-sensitive way. In order to address the requirements for specification-based completability (as identified in Chapter 2), this chapter proposes a model-based technique to complete obstructions based on the SecANet encoding. Thereby, the OLive-M approach will interpret the question how to complete an obstructed process as an optimization problem. Based on the examination of suitable methods, an integer linear programming model that optimizes the SecANet marking equation and its security-sensitive costs will realize the OLive-M approach as a way to deal with obstructions. For evaluation, a set of example models will be generated using sample models with different degrees of complexity. Experiments based on these inputs will empirically show characteristics and functionality of the proposed approach. In contrast to the exhaustive exploration of all possible markings (i.e., computing the marking graph), the experimental evaluation will underline the “lightness” of this technique to resolve obstructions. The discussion will then indicate how the approach can be used to also analyze satisfiability or resilience.

If it is not possible to avoid an obstruction, and given that early process termination is not an option and that the business goal encoded by the process is still to be achieved, a method for completing an obstructed execution must be provided. This chapter introduces an approach called OLive-M  to show that, on the basis of a SecANet, it is not only possible to capture obstructions but also to show how it can be applied to provide ways to resolve them. Thereby, to restore the liveness of an obstructed workflow execution caused by access control enforcement, a security-sensitive partial plan that completes the execution must be found. This approach will act within the general framework for requirements set up in Chapter 2; namely, on the basis of the captured state of an obstruction (GR-1), the obstruction is supposed to be resolved in a security-sensitive way based on indicators (GR-2), which are captured as costs. In the course of the approach, it will be depicted how all inputs that occur during the process lifecycle (i.e., model, policy, and log) are integrable (GR-3). This chapter presents a use case that demonstrates how, on the basis of a SecANet  encoding, Petri net-related analysis techniques can be applied or “tweaked” to resolve obstructions.

Figure 4.1 shows the OLive-M  approach. Here, an obstructed execution is supposed to live again based on a SecANet  model. The requirements for such model- or specification-based solutions have been subsumed in “Requirements for specification-based completability (RSC)” in Chapter 2. To allow for obstruction-resolving enforcement (RSC-1), partial plans that resolve obstructions must be generated. Therefore, the idea is to first “revive” the obstructed marking to escape the deadlock situation and obtain those plans. More specifically, to make the obstructed marking live again, tokens are supposed to be added to the places to enable transitions. Based on a marking that enables transitions; i.e., a live marking, a sequence of transitions that can complete the obstructed execution is to be found. Thereby, security-sensitive overrides (RSC-2) may take violations of the policy into account. The costs assigned to the considered places and transitions of the SecANet  can be used to assess security-sensitivity. A minimal cost is assumed to provide the most security-sensitive solution. In a nutshell, the OLive-M  approach involves two aspects: On one hand, adding tokens and computing the completion sequence from there, and on the other hand, determining the token addition and sequence with minimal cost. Such a completion sequence then represents a plan suitable for delegating the remaining tasks to users automatically (RSC-3). The obstruction is encoded using a SecANet, which can fully capture all specification-based information of relevance for the obstruction; i.e., the workflow, authorizations, constraints, users, and costs. Therefore, the solution can also be based on all relevant information to allow for an obstruction-aware completion (RSC-4).

Figure 4.1

Overall OLive-M  approach to resolve obstructions

A straightforward way to resolve an obstructed marking according to the described OLive-M  approach would be to try out where an added token or tokens would lead to a live marking. Then a reachability graph could determine whether there is a reachable marking that contains the desired final marking. Thereby, the resulting costs of the added tokens and the transitions involved in the sequence of completion could be determined. However, for more extensive nets, because this method may face the problem of a state-space explosion, the “small” example SecANet  can be resolved manually. Figure 4.2 shows a DMV SecANet  with annotated costs and how the OLive-M  approach can be applied. The highlighted costs are required to revive the obstructed marking and to complete the workflow. For example, on the basis of the obstruction marking $\{p_2, p_{t_2-}\}$, adding a token to the SoD place as depicted in the net would allow escaping the obstruction marking because the resulting marking would then enable the transition $t_{u_1t_2}$. However, adding a token to the SoD place would violate the SoD constraint, which is associated with a cost of $c=5.0$. After firing $t_{u_1t_2}$ ($c=1.0$) and $t_2$ ($c=1.0$), this would result in a total cost of 7.0. This is obviously the only option to resolve the obstructed marking and reach the final marking $\{p_o\}$ that makes sense here. For larger nets with a comprehensive workflow structure, multiple SoD places, more transitions, and differing costs, it can be assumed that more than one solution may exist. Here (one of) the least costly; i.e., the most security-sensitive solution, is then to be chosen. The examples, moreover, stress that interpreting the states of a SecANet  is crucial here again. For example, adding a token to a constraint place that has already been in effect represents a violation. Also, adding a token in $p_{t_2+}$ instead would contradict the overall interpretation of a SecANet. More specifically, an added token in $p_{t_2+}$ would enable $t_2$. Firing $t_2$ would skip the user-task assignment $t_{u_1t_2}$ and directly lead to the terminal marking $\{p_{t_2-}, p_o\}$. Hence, the place would indicate a user assignment even though no user has been assigned. The reductio ad absurdum of adding a token in $p_o$ and claiming process completion would result in the marking $\{p_{t_2-}, p_2, p_o\}$. It can be seen that in both cases, the leftover tokens in the terminal markings apart from $p_o$ indicate an improper process completion. Therefore, the final marking that must be reached to complete the process must be defined in a way that excludes such unwanted solutions. In the example, the final marking $\{p_o\}$ would take care of this. Based on these considerations, the following implications will be the keys to achieving the OLive-M  approach.

Figure 4.2

DMV SecANet  with annotated costs and an added token in $p_{SoD}$ to escape the obstructed state

• Reaching proper final markings: Solutions that resolve obstructions are supposed to be reasonable; i.e., the completion sequence must complete the obstructed execution from where the obstruction has happened. Hence, all unassigned WF tasks necessary to complete the workflow are supposed to be assigned to a user. Adding tokens to places that would allow skipping pending user-task assignments or tasks is not allowed. The definition of the final marking, which encodes process completion, is supposed to exclude such simple undesired solutions. Based on the further observation that obstructions may occur due to tokens missing in either SoD or BoD places, the addition of tokens must take these constrained places into consideration. Hence, given an obstructed marking, the question is which tokens must be added to reach a proper final marking that encodes the completion of the process.

• Security-sensitive optimization: The decision of which tokens to add to escape an obstruction, together with the decision of which path to choose that allows the execution to complete, must be optimized. Such an optimal security-sensitive solution represents an optimization problem, where the objective function is supposed to be a minimization that considers both the violations required to escape from the obstruction and the length of the task sequences required to complete the workflow. To solve such constrained optimization problems, local search, heuristics, or genetic approaches, and in particular, integer linear programming (ILP) are some of the most common methods.

This chapter first introduces the structural theory of Petri nets and then the context of ILP. That way, the setting of the approach can be described as a system of linear equations. Based on the theory that resolves such a system and finds a security-sensitive optimum, an ILP model that optimizes a marking equation and the costs associated with the SecANet  will realize the OLive-M  approach as a way to deal with obstructions. In contrast to computing a marking graph, this realization represents a “light technique” to resolve obstructions. The implementation of the approach will use experiments and discuss the results. Finally, in the course of the overall discussion of the approach, it will indicate how the OLive-M  approach can be used to analyze satisfiability or resilience as well, which will show the versatility of the approach.

4.1 Methods and Realization of the OLive-M  Approach

This section elaborates on the selection of Petri net analysis techniques to realize the OLive-M  approach. These techniques should be capable of both determining how a certain final marking can be reached and of optimizing the solution. To illustrate their application, the selected techniques will be directly adapted and applied to the OLive-M  context. The subsequent notation and terminology related to linear equalities or inequalities and (integer) linear programming (LP) are based on Schrijver [184].

4.1.1 Structural Theory of Petri nets

A Petri net system consists of both a net structure; i.e., the state variables (places) and their transformers (transitions), and a marking that represents a distributed overall state on the structure. The dynamics of the system or behavior are given by the evolution rules for the marking. On the basis of these two components, net-based models can be analyzed at two different levels: structural and behavioral. Structural reasoning allows the derivation of some “fast” conclusions about the possible behavior of the modeled system. Purely behavioral reasoning can be more conclusive but may require costly computations or may not even be feasible [186]. The three groups into which Petri net analysis is typically divided [155] are (1) the reachability (or also coverability) graph method, which explores the behavior, (2) the matrix-equation approach, and typically also (3) the reduction or decomposition techniques concern the net structure. The computation of the reachability graph involves essentially the enumeration of all reachable markings and applies to all classes of Petri net classes; however, it is limited to “small” nets due to the growing complexity of the state space. Particularly in light of this state-space explosion problem in behavioral analysis, structural methods are more appropriate for deducing whether a specific marking can be reached. Therefore, structural reasoning can be regarded as an abstraction of behavioral reasoning. For instance, instead of studying whether a given system, e.g., a net structure with an initial marking, has a finite state space, the system can be investigated to determine whether the state space is finite for every possible initial marking. Moreover, it can be investigated to determine whether there exists an initial marking that guarantees infinite activity rather than deciding this for a given marking [186]. Analogously, the main question of this chapter is not what markings could be reached, but whether a proper final marking is reachable from an obstructed state. Although structural reduction techniques and matrix equations are powerful, they often can be applied only to special subclasses of Petri nets or special situations [155]. Because the encoding of the SecANet  is kept as simple as possible, and a SecANet  represents an ordinary, plain, pure, and safe Petri net, it can be easily represented in a matrix as well.

Based on these considerations, the structural theory of Petri nets will subsequently be introduced to be used in the OLive-M  approach. Here in particular, the addition of tokens, and the aim to search for firing sequences that lead to a proper final marking, point to the use of the so-called marking equation. This system of linear equations will then be adapted such that the OLive-M  approach can be used.

First, basic matrix notations that allow the relation of the behavior and structure of a Petri net are given.

Definition 4.1 (Token conservation equations).

Let $N = \langle P,T,\mathcal {F},m_{0} \rangle$ be a Petri net. Given a feasible sequence $m_0{\mathop {\rightarrow }\limits ^{\sigma }}m$ , the number of tokens for a place p in m is equal to the tokens of p in $m_0$ plus the tokens added by the input transitions of p in $\sigma$ minus the tokens removed by the output transitions of p in $\sigma$ :

$$\begin{aligned} m(p) = m_0(p) + \sum _{t \in ^\bullet \!p} |\sigma |_t \ \mathcal {F}(t,p) - \sum _{t \in \, p^\bullet } |\sigma |_t \ \mathcal {F}(p,t) \nonumber \end{aligned}$$

Definition 4.2 (Incidence matrix of a Petri net).

The matrix ${{\textbf {N}}}(p,t)$ which is defined by $\mathcal {F}(t,p) - \mathcal {F}(p,t)$ is called the incidence matrix of N .

Figure 4.3 gives an example of the incidence matrix of the DMV workflow net. Figure 4.4 shows the incidence matrix of the structurally more complex SecANet.

Figure 4.3

Incidence matrix of DMV workflow net

Figure 4.4

Incidence matrix of DMV SecANet  

Definition 4.3 (Parikh vector).

Let $\sigma$ be a feasible sequence of transitions of N . $|\sigma |_a$ represents the number of occurrences of a in $\sigma$ . The Parikh vector is a function $\widehat{}:T^*\rightarrow \mathbb {N}^n$ defined as $\widehat{\sigma }=(|\sigma |_{t_1},\ldots ,|\sigma |_{t_n})$ . For simplicity, $|\sigma |_{t_i}$ will also be represented as $\widehat{\sigma }(t_i)$ . The support of a Parikh vector $\widehat{\sigma }$ , denoted by $\text {supp}(\widehat{\sigma })$ is the set $\{ t_i | \widehat{\sigma }(t_i) > 0 \}$ .

Definition 4.4 (Linear Equality).

A linear equality is given by a row vector $a \in \mathbb {R}^{n}$, a vector of variables x, and a real value b. It is represented by

$$\begin{aligned} {a^{\top } \cdot x = b} \end{aligned}$$

and it is feasible if there exists some assignment $k \in \mathbb {R}^n$ to x satisfying $a^{\top } \cdot k = b$.

Definition 4.5 (System of Linear Equalities).

A system of linear equalities is a set of linear equalities. It is feasible if there exists a vector that satisfies all equalities of the set. If it is finite, it has a matrix-based representation

$$\begin{aligned} {\boldsymbol{A}} \cdot x = b \text { ,} \end{aligned}$$

where the vectors a of the linear equalities are the rows of the matrix ${\textbf {A}}$, and the numbers b are the components of the vector b.

Based on these definitions, the marking equations for all the places in the net can be written in the following matrix form (see Fig. 4.5c for an example): $m = m_0 + {{\textbf {N}}} \cdot \widehat{\sigma }$, where N $\in \mathbb {Z}^{P \times T}$ is the incidence matrix of the net: ${{\textbf {N}}}(p,t) = \mathcal {F}(t,p) - \mathcal {F}(p,t)$.

Definition 4.6 (Marking Equation).

If a marking m is reachable from $m_0$ , there exists a sequence $\sigma$ such that $m_0{\mathop {\rightarrow }\limits ^{\sigma }}m$ and the following system of equations has at least the solution $X=\widehat{\sigma }$ :

$$\begin{aligned} m = m_0 + {{\boldsymbol{N}}} \cdot X \end{aligned}$$

(4.1)

If equation (4.1) is not feasible, m is not reachable from $m_0$. The inverse does not hold in general: there are markings satisfying equation (4.1) which are not reachable. Those markings are said to be spurious [186]. Figures 4.5a-c show an example of a net with spurious markings. The Parikh vector $\widehat{\sigma } = (2,1,0,0,1,0)$ and the marking $m = (0,0,1,1,0)$ are a solution to the marking equation, as shown in Figure 4.5c. However, m is not reachable by any feasible sequence. Figure 4.5b depicts the graph containing the reachable markings and the spurious markings (shadowed). The numbers inside the states represent the tokens at each place ($p_1,\ldots ,p_5$). This graph is called the potential reachability graph. The initial marking is represented by the state (1, 0, 0, 0, 0). The marking (0, 0, 1, 1, 0) is reachable from the initial state only by visiting a negative marking through the sequence $t_1t_2t_5t_1$, as shown in Fig. 4.5b. Therefore, equation (4.1) provides only a sufficient condition for the reachability of a marking and the replayability for a solution of equation (4.1).

Figure 4.5

(a) Petri net. (b) Potential reachability graph. (c) Marking equation

For well-structured Petri nets, for example when nets are free-choice [155], live, bounded and reversible, equation (4.1) together with a collection of sets of places (traps) of the system completely characterizes reachability [76]. For the rest of cases, the problem of the spurious solutions can be palliated by the use of trap invariants [89], or by the addition of some special places named cutting implicit places [186] to the original Petri net that remove spurious solutions from the original marking equation. Concerning matrix equations, it is assumed that a Petri net is pure or is made pure by adding a “dummy pair” of a transition and a place, as discussed previously, to avoid self-loops [155].

To realize the OLive-M  approach, the marking equation is applied in the following way. First, on the basis of the obstructed marking, tokens must be added to make the marking live again. In a second step, the Parikh vector then can be computed to give the Parikh representation of the completion sequence. The marking equation is adapted accordingly:

Definition 4.7 (OLive-M  State Equation).

Let $\text{IMAGE}$ be an obstructed SecANet , with a corresponding obstruction marking $m_\otimes$ . Then, if there exists at least one transition $\text{IMAGE}$ that can be enabled by the addition of a marking $\text{IMAGE}$ to $m_\otimes$ ; i.e., the resulting marking $m_{live}\ge ^\bullet \!t$ , the following system of equations has at least the solution $\Delta = m$ :

$$\begin{aligned} m_{live} = m_\otimes + \Delta \end{aligned}$$

(4.2)

If a marking $m_{end}$ is reachable from $m_{live}$ , there exists a sequence $\sigma$ such that $m_{live}{\mathop {\rightarrow }\limits ^{\sigma }}m_{end}$ and the following system of equations has at least the solution $X=\widehat{\sigma }$ :

$$\begin{aligned} m_{end} = m_{live} + {{\textbf {N}}} \cdot X \end{aligned}$$

(4.3)

Figure 4.6

OLive-M  state equations applied on an obstructed DMV SecANet. Each place-related variable of $\Delta$ (e.g., $p_i$) denotes the number of tokens to be added to the corresponding place. Each transition-related variable of X (e.g., $t_1$) denotes the number of occurrences of the corresponding transition in the resulting Parikh vector

Example Solution of the OLive-M  State Equation:

There are various methods to solve systems of linear equations. Probably the most well-known algorithm in linear algebra is the Gaussian elimination method, which is a polynomial-time method for solving a system of linear equations [114, 184]. Solving the system of linear equations in Figure 4.6 that applies the OLive-M  marking equation to the example SecANet  results in the solution

$$\begin{aligned} t_1&= p_i{} & {} \\ t_2&= p_i + p_2 + 1{} & {} \\ t_{u_1t_1}&= -p_i - p_2 + p_5 + p_{SoD} - 1{} & {} \\ t_{u_2t_1}&= 2 p_i + p_2 - p_4 - p_5 - p_{SoD} + 1{} & {} \\ t_{u_1t_2}&= p_i + p_2 - p_5 + 1{} & {} \\ p_3&= -p_i - p_2{} & {} \\ p_6&= p_i - p_4{} & {} \\ p_o&= p_i + p_2 - p_5\text { .}{} & {} \end{aligned}$$

Based on the observation that one can restrict the addition of tokens to constraints, one could boil the possible solutions down considerably by setting all place variables that do not encode a constraint to zero. In the example, this results in the solution

$$\begin{aligned} t_1&= 0{} & {} \\ t_2&= 1{} & {} \\ t_{u_1t_1}&= p_{SoD} - 1{} & {} \\ t_{u_2t_1}&= - p_{SoD} + 1{} & {} \\ t_{u_1t_2}&= 1{} & {} \\ p_o&= 0{ .}{} & {} \end{aligned}$$

Because the values of X and $\Delta$ are supposed to be natural numbers, here there is only one solution, namely $p_{SoD}=1$; i.e., to escape the obstruction marking, $p_{SoD}$ is additionally marked with a token. Based on this, the elements of the corresponding Parikh vector X can be determined. Figure 4.7 shows this variable assignment that solves the OLive-M  state equation applied to the example DMV SecANet. Figure 4.8 shows the same solution graphically, which obviously corresponds to the solution found manually for Figure 4.2 above.

Figure 4.7

OLive-M  state equation $m_{live} = m_\otimes + \Delta$ (token(s) to add) and $m_{end} = m_{live} + {{\textbf {N}}} \cdot X$ (Parikh vector of completion sequence) to resolve the obstruction in DMV SecANet  

Figure 4.8

$\Delta$ (added tokens) and X (Parikh vector of completion sequence) to escape the obstructed state

Replayability of Solutions:

Based on the fact that the solutions of the marking equation can be spurious, it may not be possible to reach the final marking with a proposed solution; i.e., there is no respective firing sequence. Therefore, the replayability of each solution must be checked. This means that because the solutions provided by the X vector do not provide the real ordering of transition executions, all possible linearizations must be explored to assess whether a solution obtained denotes a real sequence (in some of its possible linearizations). Due to the simplicity of the example, the order in which the transitions encoded in X must be executed is obvious, namely, $t_{u_1t_2}$ $t_2$.

4.1.2 Linear Programming

The solution of the simple example in Section 4.1.1 suggests that the solution of the system of linear equations encoding the OLive-M  state equation does not propose a specific solution for $\Delta$ and X. The number of variables in the vectors X and $\Delta$ exceeds the number of linear equations, which indicates that a solution itself probably contains variables again. Hence, rather, the solution results in further linear equations, which builds the constraints of an optimization problem that is supposed to then find specific variable assignments of natural numbers. Here, with regard to security-sensitive optimization, LP seems particularly appropriate. It not only allows the solution of systems of linear equalities but also considers linear inequalities, also called constraints. Therefore, it is possible to take an objective function into account that can be used to find an optimal solution for the constraints given. That way, the decision on which tokens to add and which transitions to fire to achieve process completion will be embedded into a constrained optimization problem.

Definition 4.8 (Linear inequality).

A linear inequality or constraint is given by a row vector $a \in \mathbb {R}^{n}$, a vector of variables x, and a real value b. It is represented by

$$\begin{aligned} a^{\top } \cdot x \le b \end{aligned}$$

and it is feasible if there exists some assignment $k \in \mathbb {R}^n$ to x satisfying $a^{\top } \cdot k \le b$.

Definition 4.9 (System of Linear Inequalities).

A system of linear inequalities is a set of linear inequalities. It is feasible if there exists a vector that satisfies all inequalities of the set. If it is finite, it has the matrix-based representation

$$\begin{aligned} {\boldsymbol{A}} \cdot x \le b\text { ,} \end{aligned}$$

where the vectors a of the linear inequalities are the rows of the matrix ${\textbf {A}}$, and the numbers b are the components of the vector b.

Definition 4.10 (Linear Programming Problem).

A $\text{IMAGE}$problem is a system ${{\boldsymbol{A}} \cdot x \le b}$ of linear inequalities, and optionally a linear function ${c^{\top } \cdot x}$ called the objective function. A solution of the problem is a vector of rational numbers that satisfies the constraints. A solution is optimal if it minimizes the value of the objective function (over the set of all solutions). An LP   is feasible if it has a solution.

Definition 4.11 (Integer Linear Programming Problem).

An ILP   is an LP   where the set of solutions is given by vectors of integers only; i.e., it is feasible only if there exists some assignment ${k \in \mathbb {Z}^n}$ to x satisfying ${{\boldsymbol{A}} \cdot k \le b}$.

The complexity of solving a linear problem depends on the domain under consideration. Specifically, it is known [184] that:

• Each LP  over $\mathbb {R}$ can be solved in polynomial time.

• The solubility of ILP  is NP-complete.

Based on these definitions, LP  is not only suitable to resolve the OLive-M  state equation for an obstructed SecANet, it may be used directly to minimize the costs associated with the nodes of a SecANet  to find a security-sensitive solution. Because the algebraic representation of Petri nets is based on integers, and the envisaged approach to add tokens and find a completion sequence implies integers (the tokens in $\Delta$ are supposed to be natural numbers, as well as the transitions in X, which can only be fired entirely or not at all), the subsequent approach will directly apply an ILP model accordingly.

OLive-M  Realization by the Marking Equation and ILP:

Given an obstruction marking $m_\otimes$ and a final marking $m_{end}$, the marking equation $m = m_0 + {{\textbf {N}}} \cdot X$ may provide the Parikh vector X, indicating which transitions must be fired to reach the final marking. To enable the transitions proposed by X, first, a live marking must be reached by adding tokens from variable $\Delta$ to the obstructed marking. With the help of a cost function $cost(X,\Delta )$ considering sequence length, the number of tokens, and user-defined costs (e.g., for security violations), an optimized solution with minimal cost for X and $\Delta$ is supposed to be proposed. The ILP model below shows the approach for using the marking equation:

After an obstructed marking $m_\otimes$ has been reached, the necessary tokens will be added to the deadlocked model to take the current obstructed marking to a final state. The ILP model above has two sets of variables, according to the equations (4.2) and (4.3): $\Delta$ is the addition of tokens to $m_\otimes$ that takes to an unobstructed marking $m_{live}$, and X is the Parikh vector that will take from $m_{live}$ to $m_{end}$. A solution to the ILP model will then jointly decide the necessary number of tokens and the consequent firings to be made to reach $m_{end}$. Remarkably, the cost function is a minimization that considers both the length of the sequence completing the workflow (through the Parikh vector X) and the number of tokens required to escape from the obstruction marking (the variables $\Delta$), thus globally optimizing these two decisions. This thesis considers the cost as a user-defined function because, on the basis of different indicators, different costs could be assigned depending on the context; e.g., if the shortest path is preferred independent of the violations done, then one can set the $\Delta$ variables’ cost to 0 (or substantially less than the X variables). On the other hand, if the number of violations should be reduced, the opposite cost can be set. Also, the cost for variables in the X vector may differ if, e.g., the firing of certain activities should be incentivized or avoided. The same holds for the $\Delta$ variables.

For instance, for the Petri net in Figure 3.24, analogously to the example solution before, the given ILP model (assigning unitary costs to both X and $\Delta$) will find the solution $\Delta = (0,0,0,1,0,0,0,0)$ (i.e., putting a token in the SoD place) and $X = (0,1,0,0,1)$ (with X according to the sequence $t_1$, $t_2$, $t_{u_1t_1}$, $t_{u_2t_1}$, $t_{u_1t_2}$). Assuming that the costs associated with transitions are normally $> 0$, minimizing the costs of cyclic nets means that loops are avoided as far as possible. This then incentives that the process execution successfully completed as immediately as possible. The assignment on $\Delta$ and X variables defines the violations to make in order to complete the workflow. Ways to assess the impact and meaning of these violations in terms of security-sensitivity for the authorization, constraints, and users will be the subject of the discussion of the approach in Section 4.3.

4.2 OLive-M  Experiments for Model-Based Obstruction Solving

The implementation of the realization of the OLive-M  presented above was applied to the CEW SecANet  shown in Figure 3.46.

4.2.1 Implementation

The implementation of the OLive-M  obstruction solution bases on a Python implementation by Taymouri [197, 198] and uses Gurobi [100] as the ILP solver. The experiments were run on a MacBook Pro with 8 GB RAM and an Intel Core i7 3 GHz CPU. Based on an SecANet  input file in PNML standard format the the optimal solution is returned as a list that contains an encoding of the $\Delta$ and X vectors.

To assign costs in the implementation, the Petri net type definition (PNTD) of place/transition nets (P/T nets) was extended with the optional addition of costs to places or transitions, resulting in P/T cost Petri nets (P/TCost-nets)¹. This PNTD redefines the value of P/T-nets with costs for places and transitions and inherits the marking and annotations from the official PNML P/T-net definition.

4.2.2 Remarks on Costs and Results

Note that no matter how costly, there may be places to which a token must be added to reach the final marking constraint (e.g., the SoD place in the DMV SecANet  example). If there is a choice among multiple transitions or places (e.g., multiple SoD places to violate) to reach the final marking, the different costs assigned are crucial. The implementation can handle both unitary and differing costs. The optimal solution is obtained when the constraint regarding the proper final marking is satisfied. In general, the ILP solutions provided in the experiments are not unique. It is possible to have many optimal solutions, and all of them are correct.

4.2.3 Experiment Preparation

To allow the final marking to be determined only by the output place, further cancellation transitions were introduced at the end of the process. They consume all the remaining tokens in the places that were put on top of the initial workflow before the flattening; i.e., (un)assignment, SoD/BoD, and their corresponding capacity-1-complement places. Therefore, similar to the introduction of the re-enactment constructions to deal with loops, or, at the end of the SecA-WF-Net  encoding in Chapter 3, a transition “reach_end” was added just before the end place $p_o$. Firing this transition produces a token into a place to which all cancellation transitions are connected. That way, this construction allows the cancellation of remaining tokens if required. In this way, the obstruction marking could be changed without the necessity to consider changes in the final marking; in particular, changes in the marking for the places resulting from the flattening.

4.2.4 Experiment Setup and Solution

The tool was able to provide a solution based on the net in Figure 3.46 with unitary costs assigned (cost = 1.0 for each place and transition) and given an arbitrary obstruction marking and a final marking to reach. To demonstrate this, an interesting obstruction marking could be reached after executing the following sequence:

$\sigma _\otimes = \langle t_s,\, t_{m_1},\, t_{f_1},\, t_{dt_1},\, t_{1_\text {compute market value}},\, t_{at_2},\, t_{2_\text {control computation}},\, t_{\text {Computation correct?}_\text {yes}},$

$t_{o_3},t_{bt_3}, t_{3_\text {Evaluate Safeguarding Requirements}}, t_{\text {Safeguarding Required?}_\text {yes}}, t_{bt_4}, t_{4_\text {Prepare Safeguarding}},$

$t_{m_2},\, t_{j_1} \rangle$

The obstruction marking resulting from this sequence is shown below, listing only places that contain $m(p) > 0$. For reasons of clarity, the marked places (with $m(p) = 1$) are categorized:

Workflow places: $P_{j_1,t_5}$

$$\begin{aligned} SoD places: SoD_{ct_1t_2}, SoD_{at_5t_1}, SoD_{dt_5t_3}, SoD_{dt_5t_4}, SoD_{dt_5t_2} \end{aligned}$$

$$\begin{aligned} C1C places: SoD_{{at_1t_2}_{c1c}}, SoD_{{dt_1t_2}_{c1c}},BoD_{{bt_3t_4}_{c1c}}, BoD_{{dt_3t_4}_{c1c}}, SoD_{{at_5t_2}_{c1c}}, SoD_{{dt_5t1}_{c1c}} \end{aligned}$$

The solution provided required that a token be put into $SoD_{at_5t_2}$ on the basis of $\Delta$ and provided the Parikh vector X containing the following transitions²:

$$t_{\text {Approved?}_\text {yes}}, t_\text {reach end}, t_{at_5}, t_\text {Approve Acquisition}, t_e$$

However, running the tool again on the same obstruction marking and net provided a different optimal solution, namely adding one token into $SoD_{dt_5t_1}$ and firing a sequence containing the following transitions:

$$t_{\text {Approved?}_\text {yes}}, t_\text {reach end}, t_{dt_5}, t_\text {Approve Acquisition}, t_e$$

Hence, the approach obtained multiple correct solutions. The replayability for both of the Parikh vectors on the net was successfully checked with an extension to the same tool.

4.2.5 Experiments with More Extensive Nets

The same net was then concatenated step by step (again with equal costs) up to six times (see Figure 4.10 for an impression of the sixth concatenation) and encoded the obstruction marking above into it. For all cases, the solution proposed the addition of a token into either $SoD_{at_5t_2}$ or $SoD_{dt_5t_1}$.

More specifically, the obstruction marking was always encoded in the first of the concatenated nets. Therefore, in particular, the solutions assigning values to the X vector to reach the final marking increased.

Table 4.1 ILP statistics

Figure 4.9

Experiment runtimes

Table 4.1 shows the statistics of the ILP that was solved ³. Gurobi also computed the corresponding costs. Note here that transitions in the computed solution can happen multiple times because of cycles in the net. However, as indicated before, the occurrence of loops is minimized in the course of the optimization. Figure 4.9 shows a perfect linear relation between the execution time required and the size of the problem.

4.2.6 Replayability

Because the solutions provided by the X vector do not provide a real ordering of transition executions, all possible linearizations were explored to assess where a solution obtained denoted a real sequence. This checking could be done for only the first four experiments because for the rest the exploration of possible solutions was very large. It is remarkable that for these four models, the solutions obtained represent a real sequence; i.e., there was a replayable linearization in the model.

4.2.7 Obstruction Position

To determine whether the position of the obstruction in the net affected runtime, an obstruction was incorporated into the last of the six concatenated nets (cf. Figure 4.10). The regarded net with 911 variables took 0.725 seconds to be solved, although the solution contained only 18 variables instead of 188. Hence, there were no substantial runtime differences from the same net with the same size but different positions of the obstruction marking.

4.2.8 Differing Costs

In a further experiment, various costs were assigned to $SoD_{dt_5t_1}$ (cost = 3.0) and $SoD_{at_5t_2}$ (cost = 5.0) to the net from the first experiment (with 151 Variables). Consequently, then the second solution containing $SoD_{dt_5t_1}$ became the only solution, resulting in a total cost of 32.0. Hence, the proposed solution was the most security-sensitive with the lowest cost.

Figure 4.10

Impression of six concatenated nets

4.3 Discussion and Potentials of the OLive-M  Approach

Based on the conclusions and requirements from Chapters 1 and 2, this chapter addresses the obstructions that must be handled at runtime to restore the liveness of an obstructed process execution. Based on the given representation of the problem, possible solutions were identified. Finally, the solution, namely OLive-M, to finding a security-sensitive solution to complete the obstructed execution was deduced. By encoding the obstruction with a corresponding marking, the marking equation was used to provide a minimized Parikh vector to reach a completed marking, which if it is fired from the obstruction state, violates the firing rules. That way, on the basis of the model of a workflow and its authorizations and constraints, an obstructed state was solved not by changing the semantics of the model [25], but by finding the best path in the given model with minimal violation. Thereby, the language of a SecANet  is temporarily extended by the words resulting from the obstructed sequences and the appended sequence that completes the obstructed execution. This solution allows the enforcement of an obstruction-resolving (RSC-1) in a security-sensitive way (RSC-2). In addition to the minimization of the solution, a certain threshold of security sensitivity could moreover exclude proposed solutions, because depending on the severity of the violations, it may be less risky to abort the process than to resolve the obstruction for an unjustifiable cost. The plans obtained to resolve obstructions could be realized automatically by delegation (RSC-3). For example, they could be used to recommend who should do which tasks in a break-glass situation, or as an assisted delegation, showing to the delegator potential best delegates (with the least violations). In all of this, the SecANet  allowed searching for solutions that were fully aware of the obstruction (RSC-4). Although these requirements have thus been addressed to a certain extent, subsequent discussions of different aspects will point out the limitations but also the further potential of the presented approach.

4.3.1 Limitations in Solutions

Based on the objective function that considers the costs assigned to the places and transitions and the calculated total cost, solutions can be identified as optimal; i.e., minimal. However, based on the fact that the solutions of the ILP can be spurious regarding their marking, and hence spurious in reaching the final marking, it may be possible for a solution to be minimal but at the same time not able to reach the final marking; i.e., there would be no respective firing sequence based on the given Parikh vector X. Hence, the solutions have the limitation that they do not necessarily represent the minimal violations required to reach the proper final marking. Here, results could be investigated further to trade efficiency for precision; i.e., by incorporating ordering constraints in the marking equation. Moreover, because the existence of a firing sequence based on a Parikh vector is guaranteed only for weakly sound-bounded free-choice models, and not for more general Petri net classes, the SecANet  free-choice transformation identified in Chapter 3 could be further pursued here.

4.3.2 Efficiency

OLive-M  represents a “light” technique to resolve obstructions as structural methods are more efficient than reachability analyses. In particular, the matrix equation itself can be solved in polynomial time. Computing the ILP and replay may be inefficient for larger instances. However, smaller-sized ILP instances can be solved efficiently in practice. Because a SecANet  represents a plain, safe, and pure ordinary Petri net, the structural theory can be easily applied, with the data reasoning remaining mild. Although a SecANet  is, e.g, not free-choice, the experimental results speak well for the SecANet  (see Figure 4.9). Here, one could further customize the approach with regard to the SecANet  application by further refinements or simplifications. If ones assumes that only constraints may be violated by adding tokens one would not have to consider all other places for the addition of tokens such that the variables in the matrix equation, the number of possible solutions, and the complexity would be reduced. However, a comparison between Figures 4.3 and 4.4 indicates how the structural complexity of the SecANet  approach is a tradeoff for efficiency, which indicates the greater amount of space that is used for the SecANet  approach. As shown above (cf. Chapter 3), a free-choice transformation would further increase the structural complexity of the SecANet. With regard to the replay, just replaying all possible linearizations of the solutions could, in the worst case, result in exploring all reachable markings. In contrast, given the marking equation and a free-choice net, the solution cannot be spurious and can be found in polynomial time.

4.3.3 Replayability

To determine replayability, the experiment basically tried to replay all possible linearizations of the Parikh vector on the SecANet. This, however, was a very simple and exhaustive way to check replayability, as indicated by the fact that only the replayability of the first four nets could be checked. Here, instead of checking whether every possible linearization of the Parikh vector is repayable, a more efficient way to check replayability would be to take the model into account. For example, given a Parikh vector that includes the transitions $t_{u_1t_2}$ and $t_2$, if the model always starts with $t_{u_1t_2}$, there would be no need to try linearizations that start with $t_2$. That way, an exploration algorithm could try to fire all transitions in the Parikh vector and thereby change the marking. In case there are several options of which transitions to fire based on the model, the algorithm could backtrack to what extent branches could be further replayed. More sophisticated techniques in this respect can be found in, for example, the works of Taymouri and Carmona [199]. Their replayability checks operate in the context of the computation of model trace alignments for conformance checking (cf. Chapter 2 on Process Mining), but could certainly be adapted to the SecANet  context as well.

4.3.4 Emergency-SecANet  

In contrast to the basic DMV SecANet  example, the solutions of the CEW SecANet   show that multiple solutions with various violations of constraints are possible. However, there may also be only one constraint, as in the DMV SecANet  that can be violated such that the solution must involve the violation of that particular SoD constraint at no matter what cost. However, in a critical situation; for example, an emergency, there may still be further possibilities in the context of the processes that are not captured in the normal process specification. Therefore, to provide for more solutions to escape obstruction, one may consider not only violating constraints but also escalating user privileges or even introducing new users in the widened context of potential process participants. To address such exceptional situations, a so-called “emergency SecANet” could be defined. Such a net could then be used only in case an obstruction were entered. It would allow authorizing a user to a task that was not authorized in the initial policy and thus permitting further user-task assignments. Figure 4.11 shows such an additional user-task transition for the second tasks. Adding such a user could then be connected to a certain cost for, for example, the associated risk of privilege escalation. Alternatively, adding further user-task transitions could, for example, encode superuser rights. Further optional elements could be built into the SecANet  in that way as well; e.g., additional constraint places. Thereby, the obstruction marking could easily be transferred to the emergency SecANet  containing further net elements. Therefore, it would be important to allow only the additional constraints to contain a token, such that no existing constraints were enacted again. As a solution to resolve an obstruction in such an emergency SecANet  could then foster empowering users who were not authorized before, instead of taking a too-high violation of an SoD constraint into account. In this way, a SecANet  could be used to integrate break-glass scenarios and directly assess the best security-sensitive solution. This could also be developed to the point where a so-called “compensation task” would be introduced that even reduces costs; e.g., a task to review the affected case could have a negative cost assigned.

Figure 4.11

“Emergency-SecANet” with costly additional user-task assignment $t_{u_3t_2}$ that could be used to resolve the obstruction too

In conclusion, the main purpose of the OLive-M  approach is to demonstrate a use case where, on the basis of a SecANet, Petri net-based techniques can be used to find solutions to complete an obstructed state. Based on the considerations, the marking equation and ILP method were chosen to propose solutions to complete the workflow. Beyond the limitations and possibilities of the OLive-M  approach, the matrix representation may also be used not only for solving obstructions but to help detect obstructions. More specifically, on the basis of the structural patterns in the SecANet  encoding, one could also investigate whether there were certain structural patterns in the matrix representation in the SecANet—for example, in the incidence matrix—that could reveal obstructions beforehand, and that way simplify their detection. However, on the basis of the plethora of techniques that exist for or relate to Petri nets, the SecANet  encoding certainly builds the basis for further approaches that would resolve obstructions differently. Here one could, for example, allow the reversal of markings, and by that search for reachable markings from the initial marking that come the closest to the obstruction marking and still allow for process completion. Because these reachable markings would belong to full firing sequences that would end in the desired final marking, this could save checking replayability. Or, one could search for firing sequences that are closest to the obstructed sequence and in that way search for the least distant or best aligning alternative path that is exceptionally allowed to resolve the obstructed state. Thereby, both approaches could incorporate costs as well. In fact, the latter can be compared to the approach idea in the next chapter, which will be considered with regard to the log-based resolving of obstructions. As identified in Chapter 2, indeed, based on the general framework for requirements (GR) embedded in all SecANet-related solutions and also the policy and the model, the log may be considered as well to allow the consideration of all inputs (GR-3). It could be applied to the OLive-M  approach as well by deriving indicators, such as resource behavior indicators. In the sense of the aspired indicator-based security, these indicators could then also be incorporated in the costs assigned to the SecANet  elements, and thus enhance the SecANet  model.

4.3.5 Extending the OLive-M  Principle to Analyze Satisfiability and Resilience

The two parts of the OLive-M  principle, namely adding tokens and completing the execution in an optimal way, may have further applications. In the context of this work, and on the basis of the SecANet  encoding, it will subsequently be shown how the OLive-M  realization can be used to analyze satisfiability and resilience. Here, the graphical nature of the SecANet  particularly would allow the direct identification of weak spots in an unsatisfiable WSP instance. Moreover, the marking equation could be used to propose which users to add to make a workflow executable. Therefore, the notion of cost can be seen in a broader context because not only security-sensitive costing may be required, but also the costs of having employees available and assigned to a certain process.

4.3.5.1 Analyzing Satisfiability

Similar to the capture and detection of obstructions, an unsatisfiable workflow raises the question as to where exactly its weak point is; for example, to identify how authorization policies or the user base must be changed to allow for a valid execution plan. Therefore, the principle of the OLive-M  approach can be adapted to the context of WSP solving in a way that allows (even graphically) the identification of such weak spots in workflows and their authorization constraints by the use of Petri nets.

More specifically, on the basis of a start marking $m_{start}$ and a final marking $m_{end}$, the marking equation $m = m_0 + { {\textbf {N}}} \cdot X$ can be used to find the Parikh vector X, indicating which transitions must be fired to reach the final marking. If the policy specification cannot provide a valid plan; i.e., no firing sequence can reach the final marking, a live marking must be reached by adding tokens from variable $\Delta$ to the start marking. Analogously to the ILP model above, with the help of a cost function $cost(X,\Delta )$ considering sequence length, the number of tokens, and user-defined costs (e.g., for adding staff), an optimized solution with minimal cost for X and $\Delta$ is proposed. The ILP model below sketches the approach:

Hence, if there were a valid plan or firing sequence, no further tokens need be added; i.e., $\Delta = \textbf{0}$, and X would contain only the transitions that must be contained in the firing sequence. In contrast, if $\Delta$ is not empty (or $\textbf{0}$), this means that the workflow is not satisfiable. $\Delta$ then already indicates the weak spot of the policy; namely, for example, which user is missing at which task or which constraint is the foremost cause of the unsatisfiability. That way $\Delta$ provides an insight as to where the “bottleneck” occurs in the security-aware process. Here, a more in-depth evaluation could be further pursued that considers the efficiency of the ILP solution compared to that of the usual WSP techniques; e.g., based on SAT-Solvers. Eventually, such a satisfiability analysis technique providing a (graphical) representation of authorizations and workflow in one model could help policy designers to pinpoint deficits in the policy specification causing the unsatisfiability.

4.3.5.2 Analyzing Resilience

Another line of research could be devoted to estimating resilience by using the structural theory of Petri nets. That way, a minimal amount of users required to successfully complete a workflow could be estimated, which would provide insight into the resilience of the workflow. Based on the presented idea to extend the approach with user-availability nets (cf. Section 3.3.2 on SecANet+), a SecANet  could involve the encoding of user availability. Here, finding for instance the minimal amount of users to execute a workflow could be done by using the marking equation as well. More specifically, the “ILP model to find a firing sequence from $m_{start}$” (see Section 4.3.5.1) for satisfiability analysis could be used because, in the resilience setting, based on the initial marking, the final marking is supposed to be reached as well. The difference would lie in the SecANet, which is extended by the user-availability encoding. Analogously to the ILP model for satisfiability, adding tokens to the places that indicate users’ presence, $\Delta$ is then supposed to indicate which users to add by the tokens in the places encoding user presence to make the process executable. Such an ILP model could then be used to compute various resilience levels introduced at the end of Chapter 3. The $\Delta$-based approach would address primarily the static version of resilience. However, one could also consider the X vector for decremental or dynamic resilience and associate the costs of the respective transitions. This would cause user absence or user presence with positive or negative costs such that, for example, there would be incentives to make sure that users only must be there as long as they are required to run the process (so that making users absent would have a negative cost). That way, the structural theory could be used to actually propose where tokens; i.e., users, must be added ($\Delta$) and when users could become present or absent (X) to make a workflow resilient. Thereby, depending on the respective costs or risks that adding or removing personnel would mean in reality, adding users and changing user availability could be promoted or prevented.