In BPMN leaks-when analysis the input is a BPMN model with annotations in pseudocode to write out how different components are related.
The BPMN leaks-when analysis is based on the pseudocode with the syntax specified in the following. It expects that most tasks are specified and the tasks that use the input data objects specify the fields of the input data.
BPMN leaks when analysis is available through PE-BPMN editor. It allows to run the analysis as well as to attach scripts to tasks.
For an example please see this model in the BPMN leaks-when view in Pleak.
BPMN leaks-when analysis is accessible from the Disclosure editor and can be activated by clicking the respective button.
The analysis output is a table that summarizes which components of the inputs flow to the outputs. The cells in the table summarize the conditions and filters that the data passes. For data that always flows to the output there were no restrictive filters in the flow. The cell value never means that this output is not affected by that input. Finally, the if condition indicates that the flow is conditional and the passed filters can be seen when hovering over the cell. In addition, everything sent through the network (message flows) is summarized in a separate row for the potential network observer.
Computation scripts are only added to tasks. Most tasks are expected to have the respective output data object defined by the scripts. The only difference are the sending tasks that have no script and the task before an exclusive gateway (that task defines the predicate for the gateway). In addition, if PE-BPMN stereotypes are used then some of them result in default scripts - e.g. encryption tasks.
The main functions of interest are names filter_<filterName> (or hash_<filterName>) where the prefix filter (or hash) distinguishes these as the filtering functions collected to the analysis output with the predicate data.
In general, the lines of code look like:
<output_data_name>.<field_in_output_data> = function(<input_data_name>.<field_in_input_data>, …, <input_data_name>.<field_in_input_data>)
Instead of the function it is also possible to give constant values to the fields or copy some field of the input.
Constants can be either numeric or “strings” (with quotation marks).
For filters the function must be called
hash_<filterName>) so that the analyzer recognizes it as a filter.
For the predicate tasks (before the starting exclusive gateway) the script is just
is_<Predicate_name>(<input_data_name>.<field_in_input_data>, …, <input_data_name>.<field_in_input_data>)
where the predicate must start with “is_” and there is no output data object.
In addition to the filters the lists have special syntax where new objects can be appended and taken out later.
Association lists are a GADT “(keytype * valuetype) assoclist” with the following six operations:
They satisfy the following equalities:
Note that currently the list predicates contains and endsWith are not considered predicates in the BPMN leaks-when output. If the answer is clear then only the respective branch is analyzed, in case the predicate can not be simplified to a boolean value then both branches are analyzed and the predicate just does not show up in the analysis outcome.
BPMN leaks-when analysis has limited support for PE-BPMN stereotypes. It supports SKEncrypt and SKDecrypt as well as public key and attribute based encryption. In addition, it can take the SecureChannel stereotype into account for analysing the values available on the network.
Using the stereotypes means that the script in BPMN leaks-when is left empty bu the user and there is a PE-BPMN stereotype attached to the task in the PE-BPMN editor. The roles of the inputs (e.g. plaintext and the key) are determined based on the stereotype settings. We assume that the input data has a field called “data” and the key data object has a field called “key”. Hence, the encryption task encrypts the field “data” with the key from field “key” and puts the result into the output field “data”. The rest of the fields in the plaintext input are copied to the output with the same names as they had for the input.
Decryption works analogously with the fields with the same name. Decryption only succeeds when the right key is used.
Note that the model that correctly uses stereotypes for BPMN leaks-when analysis may not be valid for PE-BPMN analysis as the latter does not work with the inner structures of the data.
Also note that an input data object should not be directly used as a plaintext input to encryption - it should be preceded by some (potentially dummy) data processing task to ensure that the fields of the encryption intput are defined.
An example model for secret key encryption. Open BPMN leaks-when view in Pleak to see the analysis. An example model for asymmetric (public key) encryption