a Tool for Boundary Ambients Nesting ANAlysis


Tool Usage












BANANA  is a tool for the analysis of information leakage in mobile ambient specifications. The language considered is Mobile Ambient calculus, initially
proposed by Cardelli and Gordon with the main purpose of explicitly
modeling mobility.
Sites and agents (i.e., processes) are modeled as nested boxes (i.e., ambients), provided with capabilities for entering, exiting and dissolving other boxes. This specification language provides a very simple framework to reason about information flow and security when mobility is an issue.

The main features of BANANA are:

  • A textual and graphical editor for Mobile Ambients, to specify and modify  the process by setting ambient nesting capabilities and security attributes in a very user-friendly fashion.
  • A parser which checks for syntax errors and builds the syntax tree out of the Mobile Ambient process.
  • An analyzer which computes an over approximation of all possible nestings occurring at run-time. The tool supports two different control flow analyses, namely the one of Nielson et al. and the one by Braghin et al.
  • A post-processing module, that interprets the results of the analysis in terms of the boundary-based information-flow model, where information flows correspond to leakages of high-level (i.e., secret) ambients out of protective (i.e., boundary) ambients, toward the low-level (i.e., untrusted) environment.
  • A detailed output window reporting both the analysis and the security results obtained by the post-processing module, and some statistics about the computational costs of the performed analysis.