Anica - Checking non-interference for safe Petri nets
Anica is an Automated Non-Interference Check Assistant, checking positive place based non-interference (PBNI+) and place based non-interference with downgrading (PBNID) for safe Petri nets.
Anica is a CLI-based single purpose program written in C++. As an input, Anica requires a safe Petri net, which transitions are labeled with HIGH and LOW (or additional with DOWN in case of PBNID) in case of verification. Anica provides the following features:
- Verification of a complete assigned Petri net
- Characterization of all valid assignments
- Presenting a witness path for each violation of non-interference
- Providing a fully automated use of the toolchain
- Coloring Petri nets with labeled confidence levels
- Coloring Petri nets with checked results
- Certificate-like result files
Use Case: Model support for confidential business processes
One driver of business process management is the opportunity to reduce costs by outsourcing certain tasks to third-party organizations. At the same time, it is undesirable that delicate information (e. g., customer data, trade secrets, or financial details) “leak” to the involved third parties, be it for legal or economic reasons. The absence of such leaks — called noninterference — can be checked automatically with Anica. Such a check requires an assignment of each task of the business process as either confidential or public. Drawbacks of this method are that (1) this assignment of every task is cumbersome, (2) an unsuccessful check requires a corrected confidentiality assignment although (3) the diagnosis and correction of information leaks is a nontrivial task. Anica together with Seda is a modeling prototype that integrates noninterference checks into the early design phase of an interorganizational business process. This not only allows for instant feedback on confidentiality assignments, but also for an automated completion of partial assignments toward guaranteed noninterference. Therefore the characterization of all valid assignments are used.
Watch an example on Youtube.
To use the model support the following steps are necessary:
Unzip Seda and make seda/seda executable (if necessary)
Untar Anica and run ./configure && make
Start the reasoner (part of Anica: ./src/reasoner)
Start Seda (./seda/seda or just double click it)
Add a new project to Seda (General one)
Create a new net or load the example process (drag & drop into the project folder)
Optionally add some confidentiality assignments (green and red colors)
Click the button 'Check Confidentiality of Transitions' in Seda
Download and Install
Anica is free software and is licensed under the GNU Affero General Public License. Other licenses can be negotiated with the author.
Anica is written in C/C++ and packaged by the GNU Autotools. To compile and install, unpack the tarball and execute the following commands:
For more information, please have a look at the files README, INSTALL, and REQUIREMENTS which are part of the source release.
Note: Anica needs LoLA to run.
A manual is part of the source release. A PDF version can be found here. After you installed Anica, you can get help by executing either of the following commands: