A screen-shot of the BANANA tool is
shown in the following figure.
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.