BANANA tool Usage

	BANANA a Tool for Boundary Ambients Nesting ANAlysis

A screen-shot of the BANANA tool is shown in the following figure.

tool snapshot

A user can edit the process to be analyzed by using either the Textual or the Graphical Editor. The security labelling (i.e., the labels denoting untrusted, confidential, and boundary ambients) can be inserted directly by the user, or automatically derived by the tool during the parsing phase. In the latter case, ambients starting with letter 'b' are labelled boundaries, while ambients starting with 'h' are labelled high.
By selecting an item in the Project Explorer window, the user can check/modify the properties of the ambient/capability. The user can also check the syntax correctness of the process by selecting the Parsing button.

The following figure gives an overview of the architecture of the tool

The user can then choose to launch either the Nielson or the Braghin et al. analysis. Once the analysis has started the tool parses the process, builds a syntax tree and computes the fix point algorithm yielding an over-approximation of all possible ambient nestings.
The result of the analysis is reported in the Output Console as a list of pairs of labels.

By post-processing the analysis results, the tool reports in the filed Protective the sure absence of information leakages.