|
Home
Tool Usage
Tool
References
|
|
|
|
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.
|
