This paper reports on ongoing work towards a framework to automatically rewrite business process models and, thereby, correctively enforce adherence to regulatory compliance and security policies. Specifically, the paper first motivates the need for rewriting mechanisms as a means to enforce a particular class of properties. Second, it describes the main building blocks of ReWrite, the framework to automatically rewriting process specifications. Third, in order to preserve the functional goals of the processes upon rewriting, a set of congruence relations is defined and their appropriateness is discussed. The presentation of the formal framework and rewriting algorithms is deferred to the full paper version.
Ensuring the compliance of business processes to regulations and security policies
is of utmost importance in business process management [
Specifically, this paper starts by motivating the need for rewriting mechanisms as a means to enforce a class of complex safety properties which encompass compliance requirements. In contrast to previous works, which merely present the challenge of enforcing compliance, this paper formally substantiates the need for rewriting using formal enforcement theories of computer security. By doing so, one establishes the relationship between the class of properties and the corresponding enforcement mechanisms needed to guarantee these properties.
Based on this, the paper further presents the building blocks and examples of the framework ReWrite to automatically rewrite business processes specifications and, thereby, ensure compliance with pertinent policies. The overall approach is depicted in Fig. 1. The key insight is to split responsibilities during the modeling phase and focus on the core competencies of each actor: the business experts design a process model (e.g. using BPMN or BPMN) and compliance experts design the compliance policy (i.e. description of applicable controls) and denote the processes to which they apply. The goal of ReWrite is to take process and policy specifications as input and produce an executable process model which complies to the policy.
Clearly, modifying the structure of the process may lead to a specification that does not achieve the business goals designated for that process. To circumvent this issue while still allowing for rewriting, one must define similarity relations between the original and the modified processes in terms of execution traces their produce: only modifications that preserve the similarity rela- Fig. 1. ReWrite approach. tion are appropriate. These relations are, however, not characterized in the literature. This paper defines and investigates the adequacy of four congruence relations. Initial investigations carried out with ReWrite show that rewriting operators – append, delete and replace activities in process models – can be supported by such relations, thereby allowing for effective rewriting algorithms.
Taking stock, this paper provides the following contributions: – Establishes the relationship between the compliance requirements, the underlying formal properties and the enforcement mechanisms. In particular, it shows a class of properties that can only be enforced using process rewriting and that process rewriting can enforce all other kinds of properties. – Presents the main building blocks of ReWrite. Specifically, it presents μBPMN, a Turing complete fragment of BPMN to express business processes and a meta-model for the expression of compliance policies. An example will illustrate the interplay of these requirements for rewriting. – Defines four congruence relations to guarantee the compliance with requirements while preserving the business (functional) goal of the process and discusses their adequacy for rewriting. – Reports on ongoing implementation of the ReWrite framework “as-a-service” and describes how its evaluation will be conducted.
The rewriting framework proposed in this paper can be used in three
dimensions and timepoints along the business process management lifecycle. Firstly,
before the process execution to ensure compliance “by design”. Here, if one
assumes that process are stable and faithfully executed by the business process
management system, then rewriting is capable of enforcing the designated class
(a)
(b)
of compliance properties. Secondly, during the execution for corrective
enforcement. In this setting, an execution monitor with rewriting capabilities is needed
to enforce properties. While this dimension comes along with a considerable
performance overhead, it allows for flexible process whose compliance can be
guaranteed at runtime. Thirdly, after the execution as a mechanism for automated
process enhancement and re-design based upon process models reconstructed
from event logs using process mining [
While the foundation of ReWrite can be used in any of these perspectives and timepoints, this paper focuses on the “by design” perspective – especially in terms of implementation. We currently apply these techniques to re-design reconstructed processes. Carrying over these concepts to in-line process monitoring is subject of future work. Further, it should be remarked that the focus of this paper is the presentation of the ReWrite framework, its building blocks and application. Pertinent proofs for properties – e.g., the Turing completeness μBPMN – are deferred to a longer version of the paper.
Paper structure. Section 2 establishes the relationship between classes of compliance properties and the corresponding enforcement mechanisms, thereby motivating the need for rewriting. Section 3 introduces the main building blocks of the rewriting approach, i.e. the process language and policies. Section 4 introduces the congruence relations and the corresponding rewriting operations. Section 5 reports on the implementation and evaluation of the approach. Example 1. We illustrate the high-level operation of ReWrite using an example. Consider the process model in Fig. 2(a). It stands for a medical workflow, namely updating the patient record. Activity A denotes a staff member inputting the patient_ID. If the ID exists, B queries the database and C updates the database with the updated patient record; otherwise, if there is no such an ID, D issues an error message. In both cases, E deletes local copies of query and record. One security policy may require that, before showing the query results, the staff member must be authenticated and authorized to do so, which is encoded with the activity F . Given that information, rewriting would inspect the original model to detect whether F is at the correct place. If not, ReWrite will add F to the process, which produces the process model depicted in Fig. 2(b). The remainder of this paper shows how to carry out such a rewriting.
Non-functional properties – be it security or privacy properties, or properties
arising from compliance requirements – can be classified according to two
hierarchies: (1) the Safety-Progress based on languages used to formalize the
properties [
Chang et al. [
m 6. Reactivity language: Π = ∩i=1(R(Φi) ∪ P (Ψi)).
In Fig. 3, each language encompasses those beneath it. This follows directly from the definition of the languages. For example, the language Obligation is built by the conjunction of the languages Safety and Guarantee. Further, all the Safety languages can be expressed in terms of the Obligation language, wheras the corresponding Guarantee part is empty (i.e. E(Ψi) = ∅) Obligation and Guarantee. Due to the existence operator E(Φ) the Obligation and Guarantee lan- Fig. 3. Safety-response. guages are relevant for the formalization of security and compliance requirements. For example, classical access control could be expressed in a way that the required prefix – denoting the process state – is available already by during the access decision. In this case, it can be decided that the property holds and could be no longer violated.
In another case, the required prefix is not at the decision time and must be
built during the further continuation of the process instance. Here, one cannot
decide whether the obligation will be fulfilled in a later point in time. The
enforcement of such property with classical access control is not possible. That is
because it cannot be decided whether the obligation will be fulfilled or not. If
at a given timepoint t one is to evaluate where a process instance is in the
Obligation language O1, then four different states are possible [
The rewriting approach presented in this paper allows for the automated enforcement of cases that evaluate to possibly false. The other cases can be tackled with existing access control mechanisms, in that they on the one hand prevent the transition from possibly true to false or possibly false, or if they do not allow the execution of a false instance. 2.2
This hierarchy is defined upon three well-known classes of preventive enforcement mechanisms, namely: (1) static verification before the execution; (2) runtime monitoring during the execution; and (3) rewriting before or during the execution. In particular, each of these mechanisms can recognize and therefore circumscribe a particular class of properties. The following formally defines the hierarchy, which is depicted in Fig 4.
Class Π0: Statically enforceable
properties. A policy P is statically enforceable if
there is a Turing machine MP for P that
terminates in finite time if P holds in the
process. It can be shown that the class
of enforceable security properties
corresponds to the class of recursively
decidable properties of programs, which in turn
corresponds to the arithmetic class Π0. Fig. 4. Safety-liveness hierarchy.
(See [
σ 6∈ Γ ⇒ ∃i : (∀τ ∈ Ψ : σ[..i]τ 6∈ Γ ) Based upon this, it can be shown that the class of security properties enforced by the monitor correspond to the class of co-recursively countable properties of programs, thereby circumscribing the class Π1 of the arithmetic hierarchy. Rewriting properties. The third class of properties in this hierarchy are those which can be enforced with the modification of the program. The definition of rewriting requires an adequate notion of equivalence. (See Sect. 4 for details.) For a given equivalence relation ≈, a rewriting mechanism R is considered “adequate” for enforcement if it exhibits the following properties:
P (R(M ))
P (M ) ⇒ M ≈ R(M )
These properties express that: Eq. (5) the modified program must guarantee
the compliance with a policy; and Eq. (6) if a program complies with a policy
before the rewriting, then it also complies with if after a modification. Hamlen et
al. [
The previous section demonstrates that there is a class of properties which demand process rewriting for their enforcement. This section describes the technical building blocks that serve as input to ReWrite, namely process specifications and policies, as depicted in Fig. 1. 3.1
μBPMN Syntax Our rewriting approach considers μBPMN as the modeling language for business processes. μBPMN is a Turing complete subset of BPMN containing its main constructs a formal semantics. Turing completeness is insofar relevant as it guarantees that all the computable processes can be modeled with and reasoned about in μBPMN. The formal semantics is essential to allow the rewriting and prove its correctness with regard to the congruence relations. (1) (2) (3) (4) (5) (6)
The μBPMN syntax possesses both a graphical and an algebraic notation. The
graphic notation is the same as the corresponding of BPMN construct, whereas
only the subset of the elements depicted in Fig. 5 is considered. The algebraic
formalization is required to give semantics to the language, which is in this case
based upon π-calculus [
The graphical notation of μBPMN
depicted in Fig. 5 consists of activities
(subprocesses, loops and sub-process loops)
and the gateways AND, OR and XOR,
which allow for the complete representa- Fig. 5. μBPMN language.
tion of logical constructs in the control
flow. Further, activities are linked with sequence arrows. Start and end markers
complete the subset of BPMN used in this paper. Based upon [
The consideration of subset of BPMN does not restrict the applicability of the
approach. First, because more complex modeling elements are seldom employed.
According to [
Process modeled using the μBPMN are mapped a subset of the π-calculus. Processes are thus described by a set of activities that are triggered one after the other, provided the preconditions for their firing hold.
Relevant bits of μBPMN semantics. μBPMN has an operational semantics defined via an abstract process execution engine – mimicking the operation of existing BPMN engines – whose function is to determine the state transitions (choice of the next activity) and the execution environment for the process execution (provision of runtime parameters).
For the purposes of this paper, it is enough to consider a trace-based semantics for μBPMN based upon this calculus. Let Π be a process, a path χ of Π is defined as a sequence of input/output operations of Π upon the input ω ∈ Σ. The set of all possible input parameters of a process Π is denoted by Γ ω; Π(ω) → χω denotes the path triggered by inputting ω into Π, which eventually produces the path denoted by χωΠ . Finally, ΞΠ denotes the set of all paths in a process generated by Π(Γ ω). The congruence relations defined in Sect. 4 build upon reductions of generated paths in order to describe the changes (rewriting) in the process structure before the runtime. These changes are denoted as follows: n ; χω when activity names are deleted in one path; N ; χω if activity names are deleted in all the possible paths of Π. 3.2
and where to apply the rule in a particular scope. The control defines which set of activities are to be triggered, as well as their order, so to ensure rule compliance.
This structure is expressive enough to capture the so-called “usage control”
policies and, hence, the majority of regulatory compliance requirements on
automated processes [
More specifically, the class diagram depicted in Fig. 7 shows how the compliance rules are implemented in ReWrite.
The scope consists of a list of processes to which the rule applies and one or more XPath expressions that describe the integration of (the controls specified in) this rule into the set of processes. The modality defines how the set of activities defined in the scope are treated. These activities can be deleted, replaced or complement with other activities. The latter (i.e. ap- Fig. 7. Class diagram for rules. pending) may have different modes. For example, one can distinguish between appending before, after or during an activity (in one execution branch of a parallel execution). Similarly, one can add time constraints (e.g. “within three hours”) and cardinality constraints (e.g. “exactly three times”). The controls with which the modalities are added to the process (process rewriting) are described as fragments of the BPEL language.
We define a XML schema in order to express policies rules in a machine readable format. Figure 8 depicts a policy specified in this XML schema. This rule applies to two processes (bpPatientReception and bpPatientInformation), in particular their parts (loci-tag) blood pressure and weight (here we replace the corresponding XPath expressions for simplicity). The modality-tag insertBefore conveys that the control process must be inserted before these loci. The control process, specified in the tag BPELFragment, can require in both cases the authentication of users using, for instance, their employee information. The concrete service invocation is omitted here. 4
This section sketches the rewriting operators necessary to ensure compliance. While modifying processes models one must ensure that the functional characteristics of processes are maintained. Therefore, before defining the rewriting operators, this section sketches the congruence relations operators must fulfill. 4.1
Determining the semantic congruence of two arbitrary processes is a not
decidable problem [
Formally: N = Ξp1 ∩ Ξp2 . – Unilateral semantic congruence: the set of all paths generated by the process p2 is a subset of the set of paths generated by p1. Formally: Ξp2 ⊂ Ξp1 . – Weak semantic congruence: At least one path generated the process p1 is also a path of the process p2. Formally: Ξp1 ∩ Ξp2 6= ∅.
Fig. 9 illustrates these relations. For simplicity, the processes are drawn as a simple state transition diagram (instead of μBPMN), with the dotted lines showing a possible move in the “congruence game”. The shaded circles denote activities that have been added to the process flow. The pictures denote examples of a process flow that preserve the relations.
Lack of space prevents us from providing the formal definition of all these relations. Below we provide the formal definition for the strong semantic congruence, then jumping to the rewriting operators.
Definition 1. Two processes p1 and p2 are strongly semantic congruent if the set of generated process paths after the reduction to the common names NC = Ξp1 ∩ Ξp2 6= ∅ is identical: (NC ; Ξp1 ) = (NC ; Ξp2 ). a
It is easy to show that this relation is commutative. The strong semantic congruent relation allows changes in the process paths, as the activities names are reduced to a set of names common to both processes. In doing so, rewriting operators can be defined using this definition. 4.2
The relations introduced in Sect. 4.2 are undecidable for two arbitrary processes.
This follows from Jancar [
Still, for rewriting to work it is necessary to guarantee that the original and the rewritten processes are semantically congruent and that the latter indeed Append
Delete Replace executes the controls required by the compliance policies. To achieve this in a decidable manner, we define atomic operators for appending, deleting and replacing activities in the process which, whenever applied in isolation or sequentially (one after the other), guarantee that the semantic congruence holds. Due to the lack of space, the following focuses on the “append” operator. An overview of the congruence guarantees for all the rewriting operators is given in Table 1. The “append” operator. The “append” operator adds (missing or required) activities to the process model. This operator can be applied without disturbing the semantic congruence of processes. However, the following restrictions have to be made for the case of the unilateral and weak semantic congruence: – If an activity has already been appended to one of the process models, then it is impossible to append further activities to the other model without disturbing the unilateral semantic congruence relation. – If the two processes possess solely one common path, then appending one activity may disturb the congruence relations.
We have proved these properties for the corresponding congruence relations. For the strong semantic congruence, the following can be shown: Theorem 1. The append operator preserves the strong semantic congruence. a Proof (Sketch). By appending an additional activity A to a process, then either ΞP1 or ΞP2 are extended with further traces. The computation of NC = ΞP1 ∩ ΞP2 according to Def. 1 will, however, remove this extension (by renaming the activities), so that the processes still fulfill the strong semantic congruence. tu
An analogous procedure can be used to demonstrate that the append operator preserves the unilateral and the weak semantic congruence relations, as shown in Table 1. Note that the “replace” operator is defined on the grounds of the primitive operators “append” and “delete”.
Adequacy of semantic congruence. Establishing a relationship between the rewriting operators, congruence relations and the original business goals of a process is not trivial. Here, one can distinguish between the adequacy of different relations. Considering the strong semantic congruence and the “delete” operators, for example. It is possible to remove nearly all activities of a process and still fulfill the strong semantic congruence. Our experience shows that the unilateral semantic congruence is the most promising relation within the ReWrite framework. It still suffers from the problem of the “delete” operator, but not to the same degree as the strong semantic congruence.
To tackle this problem, we add the following restrictions to the framework: (1) only activities that violate a compliance policy are deleted and, hence, should anyway not be executed; (2) if the semantic congruence is only violated at the same time that a compliance policy is violated, then the processes are still congruent. It can be shown that these restrictions are necessary and sufficient to tackle the problems arising from the “delete” operator. 5
The prototypical implementation of the ReWrite framework is based upon opensource technologies for the automation of processes with the standards of μBPMN, BPEL and automated translations from μBPMN into BPEL and the XML tools. This section reports on the realization of ReWrite and its envisaged evaluation.
The ReWrite framework has been designed as a component of the Security
Workflow Analysis Toolkit (short, SWAT) [
Figure 10 depicts the architecture of ReWrite in SWAT. The design strategy while integrating ReWrite into SWAT is the “security-as-a-service” approach. Correspondingly, the architecture consists of two modules, namely: (1) Modeling for process design and policy specification; and (2) Execution for the rewriting of noncompliant process models and the automated execution of processes. Regarding (1), SWAT offers support for process modeling in μBPMN, BPEL Fig. 10. ReWrite in SWAT. and Petri nets, whereas for process execution the specifications are translated into BPEL. Compliance policies are specified using the XML editor “Oxygen”, which is embedded in SWAT. Ongoing work is designing a policy editor and consistency checker for compliance rules. Regarding (2), SWAT employs OpenESB as an execution platform, whereas Glassfish acts an application server. It should be noted, though, that the actual realization of ReWrite does not require these technologies. Ongoing work is testing with a realization based upon jBPM.
The core of rewriting is actual modification of processes. The algorithms implementing these operators must guarantee, one the one hand, that the congruence relations are preserved (see Sect. 4.2) and, on the other, that the produced process models are correct with regard to the compliance policy. The latter depends on the compliance policy (i.e. controls defined therein) that are applied to the process. This is, however, out of the scope of this paper, as well as determining inconsistencies among policies.
The strategies for actually rewriting the processes is based on XSLT patterns, which are responsible for the transformation of XML documents (process models) with stylesheets. (Recall that the policy defines the scope of the rule, i.e., where to rewrite the process.) The following shows this using the append operator. Example 2. To guarantee the integrity of data, one can trigger controls after each data input. Considering a health care setting, for example, one could demand that, after inputting the results of an exam, the patient ID should be entered again to avoid mistakes. The realization of this requirement demands inserting a control after one activity. The corresponding algorithm thus replaces one activity with a pair activity and control. The XSLT template to enforce this control is as follows (we omit the actual call to the service realizing the control): <<x<bs lbp:petlee:mls:eapqsluaseitgnenc emnaantmacmhe==e=’’ ’’’ Eb’Rpnteuell:reaRsVesseiurglintfy[’ @’’’a>pctoiloinc Ty:yapcet=i o’ CnTonytpreo=l A’’ftReersEualcth’ ’’>] ’ ’>
<x l s : a p p l y −template /> <<<//bRbbpppee plee:lllaa::aascsessissgiibggnynn>>naacmt ue=a l’ ’ VcoenritfryoPl aftrioemntIcDo m’’p>liance r u l e </ b p e l : s e q u e n c e> </ x s l : t e m p l a t e> This template employs the namespace policy, with which action types can be assigned to activities. This facilitates the rewriting in processes where multiple occurrences of the same activity happen and are in the scope of a rule. a ReWrite envisaged evaluation. We plan to carried out an extensive evaluation of ReWrite, where qualitative and quantitative issues were of interest: firstly, which policies can be rewritten; secondly, what are the performance figures obtained in doing so. This section reports on the former.
To evaluate the expressiveness of ReWrite we plan to employ workflow
patterns [
To actually assess the expressiveness of ReWrite, we need to determine which policy pattern can be added to which workflow pattern and, further, which could be alternatively enforced with an execution monitor (EM) and which demand rewriting (RW). Our goal is to demonstrate that each workflow pattern can be rewritten to comply with the corresponding policy pattern. Ongoing experiments deliver very promising preliminary results that substantiate this conjecture. 6
Approaches to assessing business process compliance can be classified as [
Program rewriting is a mechanism for enforcing security properties [
The approaches discussed in the previous paragraph do not take into account
the achievement of the programs’ goals. The definition of some congruence
relation is given, e.g. [
De Backer and Snoeck discuss a concept called semantic compatibility which
results in definitions of similar types of congruences [
This paper introduces a framework for rewriting business processes, thereby enforce security, compliance and privacy policies. Specifically, it motivates rewriting by showing that existing enforcement mechanisms cannot cope with a relevant class of properties. The paper then defines the syntax and semantics for a graphical process modeling language and that of compliance rules. In order to ensure that the rewritten process still allows for the execution paths of the original process and, thereby, achieves the original business goals, different congruence relations are defined. Process rewriting must then not only correct the process, but also preserve some of these relations (depending on the kind of operation). Lessons learned. Rewriting is an established field in the theory of programs and logics. This paper carries over some of these concepts into business process compliance management. Although rewriting is in general undecidable for chains of modifications, this paper shows that it is possible to define primitive operators that allow for decidable procedures. The ReWrite framework thus opens up the possibility of automated correction of processes to ensure process compliance “by design” (for modeled or reconstructed processes) or during runtime. Further work. Besides the ongoing and future work already indicated in the text, future work comprises four directions: firstly, on the formal side it is still necessary to investigate the congruence relations. Spefically, we need to flesh out the details of the most sutiable relation to cover all the operators. Secondly, we see a relationship between the techniques we employ and process repositories. That in the sense that the same technologies for querying could be employed to support rewriting. Clarifying this interplay is subject of further work. Thirdly, the kinds of policy supported by ReWrite can be generalized to also consider security properties and other usage control policies. Future work will tackle the expressive power of policies and corresponding analysis techniques (e.g. inconsistency detection). Fourthly, testing ReWrite for monitoring process instances.