UBIC - Unfolding Based Interference Checker for Petri nets

This page presents a prototypical version of the tool UBIC (Unfolding-Based Interference Checker) for checking the property BNDC (Bisimulation-based Non Deducibility on Composition) on safe Petri nets. The property BNDC is a non-interference property aimed at characterising the absence of undesired information flows. The underlying idea is simple: a system is viewed as consisting of components at different levels of confidentiality, in the simplest case a high part H, which intuitively should be secret, and a low part L, which is public. The absence of a flow of information from H to L is captured by asking that the activity of H does not determine visible effects, according to some selected observational semantics, at low level L. In the BNDC formalisation, a process S is deemed free of interferences whenever S alone, seen from the low level, is behaviourally equivalent to S interacting with any parallel high level process. In the setting of Petri nets, transitions are split into two sets: high transitions H and low transitions L. The BNDC property can be characterized in terms of undesired interactions between high and low transitions. The tool exploit a characterisation of such interactions expressed in terms of the unfolding semantics, as direct causalities high level to a low level transitions and direct conflicts between high and low level transitions. The algorithm it implements is described in

Paolo Baldan, Alberto Carraro Non interference by unfolding [PDF]

The tool is maintained by Paolo Baldan and Alberto Carraro.

The tool is based on CUNF a tool set for carrying out unfolding-based verification of Petri nets extended with read arcs, also called contextual nets, or c-nets.

Download

The current version of the tool can be downloaded here ubic-0.1.tgz as a tar gzipped archive.

Installation

In order to install UBIC move to the ubic-0.1 folder and type the following commands::

  make all
  make dist

The installation puts the binaries to the "dist/bin" folder from where you may copy them to suitable locations in your machine.

The ubic-0.1 folder also includes folders

examples the examples referred to in the paper
binaries pre-compiled binaries for linux and mac osx

Usage

The input net must be expressed in the PEP ll_net format, the output can be produced in the internal 'cuf' format or as a dot file (simple or fancy). The tool can generate an e-complete prefix or stop once the first weak causal place is found. When the fancy dot output format is chosen, weak causal places are depicted in red. For details on the file formats we refer to the CUNF documentation. We only mention that when defining the a net to be checked (in the PEP ll_net format) the confidentiality level of transitions is determined by the transition name: names starting by h correspond to high level transitions, all the others to low level transitions. The tool can

Executing ubic without arguments, you'll get an overview of the command line options.

Usage: ubic [OPTIONS] NETFILE

Argument NETFILE is a path to the .ll_net input file.  Allowed OPTIONS are:
 -s [on|off]  Stop once the first weak causal place is found and report it.
              (off by default, hence a prefix complete for interferences is
               generated)
 -d DEPTH     Unfold up to given DEPTH
 -o FILE      Output file to store the unfolding in.  If not provided,
              defaults to NETFILE with the last 7 characters removed
              (extension '.ll_net') plus a suffix depending option the -O
 -f FORMAT    Write unfolding in format FORMAT. Available formats: 'cuf',
              'dot', 'fancy'.  Default is 'cuf'. In 'fancy' format weak
              causal place representatives are depicted in red