Purpose

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:

1. Download Seda (1.1.3) and Anica (1.3-unreleased)

2. Unzip Seda and make seda/seda executable (if necessary)

3. Untar Anica and run ./configure && make

4. Start the reasoner (part of Anica: ./src/reasoner)

5. Start Seda (./seda/seda or just double click it)

6. Add a new project to Seda (General one)

7. Create a new net or load the example process (drag & drop into the project folder)

8. Optionally add some confidentiality assignments (green and red colors)

9. Click the button 'Check Confidentiality of Transitions' in Seda

Download and Install

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.

Manual

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: