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

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.

To use the model support the following steps are necessary:

1. Install Seda and Anica
2. Start Seda
3. Import the project files in Seda
4. Start the reasoner (part of Anica: src/reasoner)
5. Create a net or load the example process
6. Optionally add some confidentiality assignments (green and red colors)
7. Click the button in Seda

Anica is free software and is licensed under the GNU Affero General Public License. Other licenses can be negotiated with the author.

• Download Anica
• Anica source release
• Anica source code repository

Anica is written in C/C++ and packaged by the GNU Autotools. To compile and install, unpack the tarball and execute the following commands:

./configure
make
make 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.

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:

anica --help
man anica
info anica