When outsourcing tasks of a business process to a third party, information ow security becomes a critical issue. In particular implicit information leaks are an intriguing problem. Given a business process one could ask whether the execution of a con dential task is kept secret to a third party which can observe some public (noncon dential) tasks. A business process is secure in sense of implicit information ow if a third party can not deduce the execution of con dential tasks based on observations of public tasks. We will show that we can verify much faster whether a given process model is secure, support a new information ow property, and support the modeler to create a secure process using a graphical modeling tool. The demo might be interesting for all process modelers and those who are concerned with security in the BPM community.
When outsourcing certain tasks of a business process to third-party organizations
one could \leak" sensitive information (e. g., customer data, trade secrets, or
nancial details) to the involved third parties. This is undesirable, be it for
legal or economic reasons. Information ow security concerns about such leaks
which are called interferences, so the absence of such information leaks is called
noninterference [
In the rest of the paper we explain the tools Anica and Seda and report on
experimental evaluation with over 550 industrial business processes [
Veri cation. Anica (Automated Non-Interference Check Assistant) veri es the
structural Place-based Noninterference properties PBNI+ [
Noninterference veri cation is not limited to Petri net-based process models.
We have shown in several evaluations [
To verify PBNI+ or PBNID a completely assigned and safe Petri net model of
the business process is necessary. Existing tools rst compute the complete state
space of the net and then search for information leaks making the approach
fail on large industrial business processes. Our command line interface
(CLI)based tool Anica instead decomposes the noninterference veri cation into many,
typically smaller reachability problems [
Figure 1 shows some example dot les generated by Anica. The green colored tasks l1 and l2 in Fig. 1(a) are the public tasks and the red colored task h1 is a con dential one. As shown in Fig. 1(b) there is a potential interference in which the blue colored place s is involved (as executing l1 again would allow to infer that h1 was executed). By Fig. 1(c) this potential inferences is not active (as l1 can only be executed once), otherwise the place s would also be colored blue. Therefore the Petri net used in this example is secure according to the noninterference property PBNI+. A typical veri cation run of Anica is shown in Fig. 1(d).
Modeling support. Pure veri cation is often uninteresting in practical situations: a modeler would have to mark each task either as public or con dential, check interference, and if necessary reassign. This is infeasible for industrial business processes with hundreds of tasks which permit an exponential number of assignments (2t assignments for t tasks). Rather, a modeler can create a partial assignment of some de nitely con dential tasks and some safely public tasks, leaving other tasks unassigned. However, security veri cation requires a complete assignment.
To support the modeler in this situation, we extended our veri cation tool Anica with a so called reasoner, which communicates between Anica and the graphical editor Seda, an open source Eclipse-based Petri net modeling tool3. Seda o ers the usual functionality to model and simulate Petri nets, and was extended to label each transition with a con dentiality, see Fig. 2 (left). Public tasks are labeled green, con dential tasks red, unassigned tasks are shown 3 http://service-technology.org/seda (Version 1.1.3).
GUI
Reasoner system call
system call
Business Process Model
t2 p1 p1 t1 t1 p2 p2 Confidentiality requirements
t2 updated confidentiality
t1 p1 p2 t3 t3 t2 t3
Petri net {"command":"net", "net":"UexBQ0UKICAgIHAxLAogICAgcDIKOwoKTUFSS0lORwogICAgcDEg
OiAxCjsKClRSQU5TSVRJT04gdDEKQ09OU1VNRQogICAg\ ncDEgOiAxOwpQUk9EVUNFCiAgICBwMiA6IDE7CgpUUkFOU0lUSU9OIHQyI
EhJR0gKQ09OU1VNRQogICAgcDIgOiAxOwpQUk9E\ nVUNFCjsKClRSQU5TSVRJT04gdDMKQ09OU1VNRQogICAgcDIgOiAxOwpQ
Uk9EVUNFCjsKCg=="}
Assignment {"assignment":{"t3":"","t2":"HIGH","t1":""}, "command":"assignment"}
implied assignments {"assignment":{"t3":"HIGH","t2":"HIGH","t1":""}, "command":"assignment"}
Labeled Petri net PLACE p1,p2; MARKING p1 : 1; TRANSITION t1 CONSUME p1 : 1; PRODUCE p2 : 1; TRANSITION t2 HIGH CONSUME p2 : 1; PRODUCE ; TRANSITION t3 CONSUME p2 : 1; PRODUCE ; Characterization initial t3 t2 true false p1 white, i.e., in Fig. 2 (left) t1 is con dential, t5 public and the rest unassigned. The modeler may now \Check Con dentiality of Transitions \ using a respective button which invokes the reasoner and Anica. If the current partial assignment is insecure, the modeler gets instant feedback. If the current partial assignment is secure, it is automatically extended to all other transitions that must be set to ensure the assignment chosen by the modeler, e.g., in Fig. 2 (right) four transitions were assigned to secure con dentiality of t1. This way the e ort for the modeler is reduced and the modeler gets feedback within a second allowing for a tight integration of modeling and security veri cation. Still unassigned transitions can be chosen freely by the modeler. A screen cast demonstrating the modeling support is available.4 Architecture and implementation details. Our integration of veri cation in a modeling tool also has an interesting software engineering aspect. The reasoner acts as a middleware between the CLI-based veri cation tool Anica written in C++ and Seda written in Java based on Eclipse. In our architecture the reasoner, written in C++, communicates via UDP packages based on JSON which allows to use di erent workstations for veri cation and for modeling.
Despite being a young discipline within BPM, there exist already two other tools
to check PBNI+: Frau et al. implemented PNSC [
We validated our technique in an experiment on verifying noninterference
of industrial process models [
Lessons learnt. Our approach to decompose a veri cation problem into many
typically smaller problems makes the veri cation of noninterference applicable
for industrial business processes. Furthermore the achieved speed allows a model
support based on partial assignment which are typically unusable for pure
verication tasks and tools, but as much more interesting for practical domains.
Future work. The next step could be the integration of the noninterference checks
in the context of other business process modeling tools (e.g, Oryx [
Acknowledgement. The authors cordially thank Niels Lohmann for his ideas about the reasoner. This work was partially funded by the German Research Foundation in the project WS4Dsec in the priority program Reliably Secure Software Systems (SPP 1496).