\documentclass[11pt]{entcs}

\usepackage{times}
\usepackage{fullpage}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\newcommand{\e}{\emptyset}
\newcommand{\proof}{\noindent{\bf Proof.~}~}
%\newcommand{\qed}{\hfill$\Box$\par \medskip \par}

\newcommand{\infig}[3]{\begin{figure*}[t]
\vspace*{.5cm} \centerline{\epsfbox{#1}}
\caption{\label{#2} #3} \end{figure*}}

\newcommand{\infigqui}[3]{\begin{figure*}[h] \input{epsf}
\centerline{\epsfbox{#1}}
\caption{\label{#2} #3} \end{figure*}}

\newcommand{\infigquinc}[3]{\begin{figure*}[h] \input{epsf}
\centerline{\epsfbox{#1}}
\end{figure*}}

\newcommand{\infq}{\mbox{\Large $\sqcap$}}
\newcommand{\supq}{\mbox{\Large $\sqcup$}}
\newcommand{\on}[2]{\Bigl(\!\begin{array}{c}{\scriptstyle #1}\\
                   {\scriptstyle #2}\end{array}\!\Bigr)}
\newcommand{\bigmcap}{\mbox{\tiny $+$} \hspace*{-1.9 ex}\bigcap}
        \newcommand{\mo}{\{ \hspace* {-0.35ex}[\,}
        \newcommand{\mc}{\,] \hspace* {-0.35ex}\}}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
%\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{corollary}[theorem]{Corollary}
%\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}

\usepackage{amsmath}
\newcommand{\eller}{\ensuremath{|}}
\newcommand{\la}[1][\ell]{\ensuremath{#1^{a}}}
\newcommand{\lt}[1][\ell]{\ensuremath{#1^{t}}}
\newcommand{\ambient}[2][{}]{\ensuremath{{\ambientname{#2}}_{#1}}}
\newcommand{\Mar}{\domain{Mar}}
\newcommand{\Labarg}[1]{\ensuremath{\domain{Lab}^{#1}}}
\newcommand{\Laba}{\Labarg{a}}
\newcommand{\Labt}{\Labarg{t}}
\newcommand{\fnnoarg}{\ensuremath{\mathit{fn}}} % For intext reference
\newcommand{\fn}[1]{\ensuremath{\fnnoarg(#1)}} % Free Names

% Macros for the syntax of the calculus of Mobile Ambients
\newcommand{\rest}[2]{\ensuremath{(\nu \ambientname{#1})#2}}
\newcommand{\zero}{\ensuremath{\mathbf{0}}}
\newcommand{\comp}[2]{\ensuremath{#1\ |\ #2}}
\newcommand{\compx}{\ensuremath{\ |\ }}
\newcommand{\repl}[1]{\ensuremath{{!}#1}}
\newcommand{\amb}[3]{\ensuremath{\ambientname{#1}^{#2}[#3]}}
\newcommand{\act}[2]{\ensuremath{#1.#2}}
\newcommand{\actt}[3]{\ensuremath{#1.#2.#3}}
\newcommand{\capa}[1]{\ensuremath{\mathit{#1}}}


\newcommand{\domain}[1]{\mbox{\rm\textbf{\textsf{#1}}}}
\newcommand{\Proc}{\domain{Proc}}
%\newcommand{\rest}[3]{\ensuremath{(\nu\,\ambientname{#2})#3}}
\newcommand{\toplevelamb}{\ensuremath{\ambientname{n}_{*}}}
\newcommand{\ambientname}[1]{\ensuremath{#1}}
\newcommand{\actl}[3][\lt]{\ensuremath{\act{\capa{#2}^{#1}}{\mathit{#3}}}}
\newcommand{\ambn}[1]{\ensuremath{\ambientname{#1}^{\la[\ell_{#1}]}}}
\newcommand{\ambl}[2]{\ensuremath{\ambientname{#1}^{\la[\ell_{#1}]}{[#2]}}}

% Scoped versions of shorthand macros
\newcommand{\samb}[3]{\ensuremath{\ambientname{#1}^{#2}[ \, #3 \, ] \, }}
\newcommand{\sambn}[2]{\ensuremath{\ambient[#2]{#1}^{\la[\ell_{#1}]}}}
\newcommand{\sambl}[3]{\ensuremath{\ambient[#2]{#1}^{\la[\ell_{#1}]}{[#3]}}}
%\newcommand{\sina}[2]{\ensuremath{\capa{in}^{#1} \ambient{#2}}}
%\newcommand{\souta}[2]{\ensuremath{\capa{out}^{#1} \ambient{#2}}}
%\newcommand{\sopena}[2]{\ensuremath{\capa{open}^{#1} \ambient{#2}}}
\newcommand{\sina}[2]{\ensuremath{\capa{\In}^{#1}\,\ambient{#2}}}
\newcommand{\souta}[2]{\ensuremath{\capa{\Out}^{#1}\,\ambient{#2}}}
\newcommand{\sopena}[2]{\ensuremath{\capa{\Open}^{#1}\,\ambient{#2}}}
\newcommand{\Out}{\mbox{\bf out}}
\newcommand{\In}{\mbox{\bf in}}
\newcommand{\Open}{\mbox{\bf open}}
\newcommand{\AMB}{\mbox{\bf Amb}}
\newcommand{\sincap}[3][\lt]{\act{\sina{#1}{#2}}{#3}}
\newcommand{\soutcap}[3][\lt]{\act{\souta{#1}{#2}}{#3}}
\newcommand{\sopencap}[3][\lt]{\act{\sopena{#1}{#2}}{#3}}

\newcommand{\cas}[1]{\ensuremath{(\mathit{#1})}}
\newcommand{\argu}[2]{\ensuremath{{#1}(#2)}}
\newcommand{\anno}[1]{\text{\rm #1}}
\newcommand{\annoCF}{\anno{CF}}
\newcommand{\annoOC}{\anno{OC}}
\newcommand{\annoB}{\anno{B}}

\newcommand{\betaCF}{\ensuremath{\beta^{\annoCF}}}
\newcommand{\betaOC}{\ensuremath{\beta^{\annoOC}}}
\newcommand{\betaB}{\ensuremath{\beta^{\annoB}}}
\newcommand{\gammaCF}{\ensuremath{\gamma^{\annoCF}}}
\newcommand{\gammaOC}{\ensuremath{\gamma^{\annoOC}}}
\newcommand{\gammaB}{\ensuremath{\gamma^{\annoB}}}
\newcommand{\alphaCF}{\ensuremath{\alpha^{\annoCF}}}
\newcommand{\alphaOC}{\ensuremath{\alpha^{\annoOC}}}
\newcommand{\alphaB}{\ensuremath{\alpha^{\annoB}}}
\newcommand{\A}{\ensuremath{\hat{A}}}
\newcommand{\I}{\ensuremath{\hat{I}}}
\newcommand{\Hc}{\ensuremath{\hat{H}}}
\newcommand{\IH}{\ensuremath{(\I,\Hc)}}
\newcommand{\IB}{\ensuremath{\hat{I_{B}}}}
\newcommand{\IE}{\ensuremath{\hat{I_{E}}}}
\newcommand{\IIH}{\ensuremath{(\IB,\IE,\Hc)}}
\newcommand{\hviss}{\ensuremath{\mathrm{iff}}}
\newcommand{\always}{\ensuremath{\mathrm{always}}}

\newcommand{\IHrelx}[2][\IH]{\ensuremath{#1\models^{\annoCF} #2}}
\newcommand{\IHrel}[2][\IH]{\ensuremath{#1\models^{\annoCF} #2}}
\newcommand{\IHrelNumb}[2]{\ensuremath{(\I_#1,\Hc_#1)\models^{\annoCF} #2_#1}}
\newcommand{\IHreln}[2][\IIH]{\ensuremath{#1\models^{\annoCF} #2}}
\newcommand{\IHreloc}[2][\IIH]{\ensuremath{#1\models^{\annoOC} #2}}
\newcommand{\IHrelb}[2][\IIH]{\ensuremath{#1\models^{\annoB} #2}}
\newcommand{\rep}{\ensuremath{\beta^{\annoCF}}}
\newcommand{\repb}{\ensuremath{\beta^{\annoB}}}
\newcommand{\repa}[2]{\ensuremath{\argu{\rep_{#1}}{#2}}}
\newcommand{\repab}[2]{\ensuremath{\argu{\repb_{#1}}{#2}}}
\newcommand{\specskip}{-4mm}
\newcommand{\set}[1]{\ensuremath{\left\lbrace #1\right\rbrace}}  % Short for {.}
\newcommand{\lub}[1][{}]{\ensuremath{\sqcup_{#1}}}       % Least-upper-bound
\newcommand{\og}{\ensuremath{\ \wedge\ }}
\newcommand{\foralled}[1]{\ensuremath{\forall #1 : }}

\newcommand{\lap}[1][\ell]{\ensuremath{#1^{a'}}}
\newcommand{\lapp}[1][\ell]{\ensuremath{#1^{a''}}}
\newcommand{\infrel}[3]{(#1,#2)\in#3}
\newcommand{\delmgd}[2]{\ensuremath{#1\subseteq#2}}
\newcommand{\capindent}{\quad}

%%% NEW MACROS
\newcommand{\leftbb}{\boldsymbol{[}\kern-.26em\boldsymbol{[}\,}
\newcommand{\rightbb}{\boldsymbol{]}\kern-.26em\boldsymbol{]}\,}
\newcommand{\bdbrackets}[1]{\leftbb #1 \rightbb}

\newcommand{\leftb}{[\![}
\newcommand{\rightb}{]\!]}

\newcommand{\boundary}[3]{\ensuremath{\,#1^{#2} \leftb #3 \, \rightb}}
\newcommand{\boldambient}[3]{\ensuremath{\,#1^{#2} \leftbb #3 \, \rightbb}}

%% DOUBLE SPACE
%\renewcommand{\baselinestretch}{2}

\def\lastname{Braghin, Cortesi and Focardi}

\begin{document}
\begin{frontmatter}
\title{Security Boundaries in Mobile Ambients\thanksref{levigiaco}}
\author{Chiara Braghin \ \ \ \ \ Agostino Cortesi \ \ \ \ \ Riccardo Focardi}
\address{Dipartimento di Informatica, \\
Universit\`a Ca' Foscari di Venezia, \\
Via Torino 155,
30173  Venezia -- Mestre (Italy) \\
 {\tt\{braghin,cortesi,focardi\}@dsi.unive.it}}
\thanks[levigiaco]{Partially
    supported by MURST Projects ``Interpretazione Astratta, Type Systems e
    Analisi Control-Flow'', and
    ``Modelli formali per la sicurezza'' and the EU Contract IST-2001-32617 ``Models
    and Types for Security in Mobile Distributed Systems''. The paper is an
    extended and revised version of~\cite{fmoods02,concoord01}.}
\vspace{0.3cm} \begin{abstract} A new notion of Security Boundary
is introduced to model multilevel security policies in the
scenario of mobile systems, within Cardelli and Gordon's ``pure''
Mobile Ambients calculus. Information leakage may be expressed in
terms of the possibility for a hostile ambient to access
confidential data that are not protected inside a security
boundary. A control flow analysis is defined, as a refinement of
the Hansen-Jensen-Nielsons's CFA, that allows to properly capture
boundary crossings. In this way, direct information leakage may be
statically detected.
\\
\noindent
{\bf Keywords:~}~ Mobile Ambients, Security, Static Analysis.
\end{abstract}
\end{frontmatter}


\section{Introduction}

\noindent {\bf The problem. }
In distributed systems, resources and data are shared among users with different locations, yielding to a number of security issues that are object of an increasing number of research projects.
Mobile Ambients Calculus has been introduced by Cardelli and Gordon in~\cite{Cardelli:97:MA} to model both mobile computation and mobile systems. A challenging problem, within this setting, is to properly tackle security issues.

We focus on {\it Multilevel Security}, a particular
{\it Mandatory Access Control} security policy: every
entity is bound to a security level (for simplicity, we consider only
two levels: high and low),
and information may just flow from the low level to the high one.
Typically, two access rules are imposed:
$(i)$ {\it No Read Up}, a low level entity
cannot access information of a high level entity; $(ii)$
{\it No Write Down}, a high level entity cannot leak information to a
low level entity.
Sometimes, these two access controls are not enough as information may be
indirectly leaked, through, e.g., some system side-effect: a typical
example is represented by a resource shared among the security levels
which may be alternatively
overloaded by some high level Trojan horse program (causing, e.g., longer response time at all
security levels)
in order to transmit information to a
malicious low level entity. These indirect ways of transmitting information
are called \emph{covert channels}. Figure~\ref{NRUNWD} summarizes this policy.
%
\infigqui{multi2.ps}{NRUNWD}{Multilevel Security Policy.}
%

\noindent In order to detect information
leakages, a typical approach (see, e.g.,
~\cite{BDNN99pi,focardi00information,FG95,FG97,hennessy00resource,smith98secure})  consists in directly
defining what is an information flow from one level to another
one. Then, it is sufficient to verify that, in any system
execution, no information flow is possible from level high to
level low. This is the approach we follow in this paper.

\vspace{0.5cm}
\noindent {\bf The scenario.}
We will consider information flow security
in the scenario of mobile systems. This
particular setting, where code may migrate from one security level to
another one, complicates even further the problem of capturing
all the possible information leakages.
As an example, confidential data
may be read by an authorized agent which, moving
around, could expose them to unexpected attacks. Moreover, the code itself
could be confidential, and so not allowed to be read/executed by lower
levels.

In order to study this problem as much abstractly as possible, we consider
the ``pure'' Mobile Ambients calculus~\cite{Cardelli:97:MA}, in which no
communication channels are present and the only possible actions are
represented by the moves performed by mobile processes.
This allows to study a very general notion of information flow which should
be applicable also to more ``concrete'' versions of the calculus (e.g.~\cite{BugCasCra:TACS:01,levi00controlling}).

\vspace{0.5cm}
\noindent {\bf Verification. }
We introduce the new notion of ``Security Boundary'', that allows to
identify ambients that may guarantee to properly protect their content.
The intuition is the following: to guarantee absence of information leakage,
every high-level data or process should be encapsulated into a boundary
ambient, and a boundary ambient can be opened only when it is nested into
another boundary ambient. Then, we may even allow that low level
information/processes interfere with high level data inside a boundary
ambient, but we want to be sure that once this happens, the low
information/process is trapped:  it can
neither carry high-level information out of the boundary ambient nor
move out of it.

Instead of proposing a new variant of Ambient Calculus to apply and
develop this ideas, we adopt a static analysis approach: given a process
P, and a partition of its ambient and capability labels into ``high'', ``low'',
and ``boundary'' sets, we
aim at providing methods and tools to {\it verify} that in every execution of
process P no direct information leakage occurs.

A first approach to this issue may consist in introducing
syntactic restrictions on process P, as initially proposed
in~\cite{concoord01}. A less
 restrictive and more accurate solution can be obtained by refining the control
 flow analysis by Hansen, Jensen and Nielson's~\cite{HJNN99ai}.

The aim of the analysis proposed in~\cite{HJNN99ai} is to
calculate an over approximation of ambient nestings,
 i.e. the analysis returns a set which contains all the ambient nestings that are possible
 at run-time. However, the fact that all nestings are collected in a unique set,
 may introduce some ``fake'' nestings in the result. As an example, consider a low level
 ambient $\ell$ that moves inside a boundary $b$ and, after that, is entered by a high
 level ambient $h$. The initial and the final situation may be depicted
 as:

\infigquinc{exampleAA.eps}{aabb}{}

\noindent If we write down all the nestings in the form $(x,y)$
meaning that ``$x$ may contain $y$'', we obtain $(env,\ell),
(env,b), (b,h)$ from the initial state, plus $(\ell,h)$ from the
final one. From this ``flat'' representation, we obtain
$(env,\ell)$ and $(\ell,h)$, i.e. a fake nesting showing that $h$
is unprotected (because outside of $b$), thus possibly exposed to
environment attacks.

\infigquinc{exampleC.eps}{cc}{}

\noindent Here, we propose a more accurate abstract domain that
separately considers nestings inside and outside boundaries,
yielding to a much more sophisticated control flow analysis. The
example above will be analyzed through two separate sets of
nestings, ${(env,\ell),(env,b)}$ and ${(b,h),(b,\ell)(\ell,h)}$,
representing the possible nestings outside and inside boundaries,
respectively. Note that now we do not have a nesting path leading
from $env$ to $h$. The fake nesting above is not derived by our
analysis as it keeps track that $h$ is inside $\ell$ only when
$\ell$ is inside some boundaries.

%A more accurate abstract domain is proposed that uses trees instead of sets, and keeps apart boundary nestings, yielding to a much more sophisticated control flow analysis.


\vspace{0.5cm} \noindent The rest of the paper is organized as
follows. In Section~\ref{formalization} we introduce the basic
terminology on ambient calculus and we briefly report the control
flow analysis of~\cite{HJNN99ai}. In Section~\ref{verification},
we present the model of multilevel security for mobile agents and
we show how to guarantee absence of unwanted information flows
through simple syntactic restrictions. In Section~\ref{CFA}, we
introduce the refined Control Flow Analysis, which is proved to be
correct in Section~\ref{proof}. Section~\ref{conclusions}
concludes the paper with final remarks and comparisons with
related works.

\section{Background}\label{formalization}
In this section we introduce the basic terminology of ambient
calculus and we briefly report the control flow analysis
of~\cite{HJNN99ai}.
\subsection{Mobile Ambients}
The Mobile Ambients calculus has been introduced in~\cite{Cardelli:97:MA} with the main purpose of explicitly modeling
mobility. Indeed, ambients are arbitrarily nested boundaries which
can move around through suitable capabilities. The syntax of
processes is given as follows, where $n \in \AMB$ denotes  an
ambient name.
%The labels $\la$ and $\lt$
%have been introduced in \cite{HJNN99ai} for the control flow analysis.

\begin{center}
\renewcommand{\arraystretch}{1.2}
\begin{tabular}[t]{rcll}
$P,Q$ & ::=    & \rest{n}{P}       & restriction \\
      & \eller & \zero                  & inactivity \\
      & \eller & \comp{P}{Q}            & composition \\
      & \eller & \repl{P}               & replication \\
      & \eller & \boldambient{n}{\la}{P}
                & ambient \\
      & \eller & \act{\sina{\lt}{n}}{P}
                & capability to enter $n$ \\
      & \eller & \act{\souta{\lt}{n}}{P}
                    & capability to exit $n$ \\
      & \eller & \act{\sopena{\lt}{n}}{P}
                & capability to open $n$

\end{tabular}
\end{center}

%\boldambient{b} {\la} {P}
\newcommand{\mysmash}[1]{\smash{#1}}
\noindent Labels $\la\in\Laba$ on ambients and labels
$\lt\in\Labt$ on transitions are introduced as it is customary in
static analysis to indicate ``program points''. They will be
useful in the next section when developing the analysis.

Intuitively, the restriction $\rest{n}{P}$ introduces the new name
$n$ and limits its scope to $P$; process $\zero$ does nothing;
$\comp{P}{Q}$ is $P$ and $Q$ running in parallel; replication
provides recursion and iteration as $\repl{P}$ represents any
number of copies of $P$ in parallel. By $\boldambient{n}{\la}{P}$
we denote the ambient named $n$ with the process $P$ running
inside it. The capabilities \mysmash{$\sina{\lt}{n}$} and
\mysmash{$\souta{\lt}{n}$} move their enclosing ambients in and
out ambient $n$, respectively; the capability
\mysmash{$\sopena{\lt}{n}$} is used to dissolve the boundary of a
sibling ambient $n$. The operational semantics of a process $P$ is
given through a suitable reduction relation $\rightarrow$ and a
structural congruence $\equiv$ between processes (see
Appendix~\ref{MAsemantics} for more details). Intuitively, $P
\rightarrow Q$ represents the possibility for $P$ of reducing to
$Q$ through some computation.

%denotes the reduction relation as defined in \cite{Cardelli:97:MA}.



\subsection{Control Flow Analysis}
\label{cfsec}

%\renewcommand{\baselinestretch}{1}

\begin{figure}
\centering

\fbox{\parbox{4.5in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lll}
\cas{res} & \repa{\ell}{\rest{n}{P}} & = & \repa{\ell}{P}\\
\\[\specskip]
\cas{zero} & \repa{\ell}{\zero} & = & (\emptyset,\emptyset)\\
\\[\specskip]
\cas{par} & \repa{\ell}{\comp{P}{Q}} & = &
   \repa{\ell}{P} \lub \repa{\ell}{Q}\\
\\[\specskip]
\cas{repl} & \repa{\ell}{\repl{P}} & = & \repa{\ell}{P}\\
\\[\specskip]
\cas{amb} & \repa{\ell}{\boldambient{n}{\la}{P}} & = &
  \repa{\la}{P} \lub (\set{(\ell,\la)}, \set{(\la,n)})\\
\\[\specskip]
\cas{in} & \repa{\ell}{\sincap{n}{P}} & = &
  \repa{\ell}{P} \lub (\set{(\ell,\lt)},\emptyset)\\
\\[\specskip]
\cas{out} & \repa{\ell}{\soutcap{n}{P}} & = &
  \repa{\ell}{P} \lub (\set{(\ell,\lt)},\emptyset)\\
\\[\specskip]
\cas{open} & \repa{\ell}{\sopencap{n}{P}} & = &
  \repa{\ell}{P} \lub (\set{(\ell,\lt)},\emptyset)
\end{array}
\end{displaymath}
}}
\caption{Representation Function for the Control Flow Analysis}
\label{cfa_repr}
\end{figure}



\begin{figure}
\centering

\fbox{\parbox{5.5in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lcl}
\cas{res} & \IHrel{\rest{n}{P}}& \hviss &\IHrel{P}\\
\\[\specskip]
\cas{zero} & \IHrel{\zero} & \multicolumn{2}{l}{\always}\\
\\[\specskip]
\cas{par} & \IHrel{\comp{P}{Q}}& \hviss & \IHrel{P} \og \IHrel{Q}\\
\\[\specskip]
\cas{repl} & \IHrel{\repl{P}}& \hviss & \IHrel{P}\\
\\[\specskip]
\cas{amb} & \IHrel{\boldambient{n}{\la}{P}} & \hviss & \IHrel{P}\\
\\[\specskip]
\cas{in} & \IHrel{\sincap{n}{P}}& \hviss & \IHrel{P} \og \\
 &  \multicolumn{3}{l}{
    \capindent
    \begin{array}[t]{@{}l}
     \foralled{\la,\lap,\lapp\in\Laba} (\infrel{\la}{\lt}{\I}
     \og \infrel{\lapp}{\la}{\I} \og
            \infrel{\lapp}{\lap}{\I}\\
     \quad \og \infrel{\lap}{n}{\Hc})
     \implies \infrel{\lap}{\la}{\I}\\
    \end{array}}\\
\\[\specskip]
\cas{out} & \IHrel{\soutcap{n}{P}}& \hviss & \IHrel{P} \og \\
 &  \multicolumn{3}{l}{
    \capindent
    \begin{array}[t]{@{}l}
     \foralled{\la,\lap,\lapp\in\Laba} (\infrel{\la}{\lt}{\I} \og
     \infrel{\lap}{\la}{\I} \og
            \infrel{\lapp}{\lap}{\I}\\
     \quad \og \infrel{\lap}{n}{\Hc})
     \implies \infrel{\lapp}{\la}{\I}\\
    \end{array}}\\
\\[\specskip]
\cas{open} & \IHrel{\sopencap{n}{P}}& \hviss & \IHrel{P} \og \\
 &  \multicolumn{3}{l}{
    \capindent
    \begin{array}[t]{@{}l}
    \foralled{\la,\lap\in\Laba} (\infrel{\la}{\lt}{\I} \og \infrel{\la}{\lap}{\I}
            \og \infrel{\lap}{n}{\Hc})\\
     \quad \implies \delmgd{\set{\comp{(\la,\ell')}{\infrel{\lap}{\ell'}{\I}}}}{\I}
    \end{array}}
\end{array}
\end{displaymath}
}}
\caption{Specification of the Control Flow Analysis}
\label{cfa_models}
\end{figure}

%\renewcommand{\baselinestretch}{2}

The control flow analysis described in~\cite{HJNN99ai} aims at
modeling which processes can be inside what other processes. It
works on pairs $(\hat{I},\hat{H})$, where:
\begin{itemize}
\item The first component $\hat{I}$
is an element of $\wp(\Laba \times (\Laba \cup \Labt))$.
If a process contains an ambient labelled $\ell^a$ having inside
either a capability or an ambient labelled $\ell$, then $(\ell^a,\ell)$
is expected to belong to $\hat{I}$.
\item The second component $\hat{H} \in \wp(\Laba \times \AMB)$ keeps track of the correspondence between
names and labels. If a process contains an ambient labelled $\ell^a$ with name $n$,
then $(\ell^a,n)$ is expected to belong to $\hat{H}$.
\item The pairs are component-wise partially ordered.
\end{itemize}
The analysis is defined by a representation function and a
specification\footnote{In ambient calculus bound names may be
$\alpha$-converted. For the sake of simplicity, here we are
assuming that ambient names are \emph{stable}, i.e., $n$ is indeed
a representative for a class of $\alpha$-convertible names.
See~\cite{HJNN99ai} for more details on how this can be handled.}.
They are recalled, respectively, in Figure~\ref{cfa_repr} and
Figure~\ref{cfa_models}.

The representation function aims at mapping concrete values to
their best abstract representation. It is given in terms of a
function $\repa{\ell}{P}$ which basically builds sets \I\; and
\Hc\; corresponding to process $P$, with respect to an enclosing
ambient labelled $\ell$. The representation of a process $P$ is
defined as $\repa{env}{P}$, where $env$ is a special label
corresponding to the environment.

\begin{example}\label{runEx1} {\rm Let $P$ be a process of the form:
P =
\boldambient{n}{\ell_{1}^{a}}{\boldambient{m}{\ell_{2}^{a}}{\souta{\lt}{n}}},
thus the representation function of P is the following:
$\repa{env}{P} =
(\{(env,\ell_{1}^{a}),(\ell_{1}^{a},\ell_{2}^{a}),
(\ell_{2}^{a},\lt)\},\{(\ell_{1}^{a},n),(\ell_{2}^{a},m)\})$ }.
\end{example}

The specification depicts how the process transforms one abstract
representation to another one, and it mostly amounts on recursive
check of subprocesses except for the three capabilities {\em
open}, {\em in}, and {\em out}. The rule for {\em open-}capability
says that if some ambient labelled $\ell^a$ has an {\em
open-}capability $\ell^t$ on an ambient $n$, that may apply due to
the presence of a sibling ambient labelled $\ell^{a'}$ whose name
is $n$, then the result of performing that capability should also
be recorded in $\hat{I}$, i.e. all the ambients/capabilities
nested in $\lap$ have to be nested also in $\la$. The {\it in} and
{\it out} capabilities behave similarly.

\begin{example}\label{runEx2}
{\rm Let $P$ be the process of Example~\ref{runEx1}, thus the
least solution of P is the pair (\I,\Hc) where \I = $\{
(env,\ell_{1}^{a}),(env,\ell_{2}^{a}),(\ell_{1}^{a},\ell_{2}^{a}),
(\ell_{2}^{a},\lt)\}$ and $\Hc =
\{(\ell_{1}^{a},n),(\ell_{2}^{a},m) \}$.}
\end{example}

The correctness of the analysis is proven by showing that every reduction
of the semantics is properly mimicked in the analysis:

\begin{theorem}\label{theo} Let $P$ and $Q$ be two processes such that
 $ \ \repa{env}{P} \sqsubseteq (\hat{I},\hat{H}) \  \  \wedge  \ \
 \IHrel{P}  \ \wedge \ P
\rightarrow Q. \ \ $ Then,  $\ \ \repa{env}{Q} \sqsubseteq
(\hat{I},\hat{H}) \ \  \wedge \ \
 \IHrel{Q}$.
\end{theorem}
Intuitively,  whenever $\IHrel{P}$ and the representation of $P$ is
contained in $(\hat{I},\hat{H})$, we are assured that
every nesting of ambients and capabilities in every possible derivative of
$P$ is also captured in $(\hat{I},\hat{H})$.

It is important to recall that the resulting control flow analysis
applies to any process, and that every process enjoys a {\em
least} analysis.


\section{Information Flow}\label{verification}
In this section, we present a formalization of multilevel security
in the setting of Mobile Ambients (Section~\ref{multilevesec}). We
apply the control flow of Section~\ref{cfsec} to the verification
of multilevel security and we show that in some cases it is too
approximate (Section~\ref{leakabsence}). Then, a simple syntactic
property is given which allows to very efficiently verify the
absence of unwanted information flows and which also solves some
of the approximation problems of the control flow
(Section~\ref{syntactic}).

\subsection{Modeling Multilevel Security}\label{multilevesec}
In order to define Multilevel security in Mobile Ambients we first
need to classify information into different levels of
confidentiality. We do this by exploiting the labelling of
ambients. In particular, we partition the set of ambient labels
$\Laba$ into three disjoint sets $\Laba_H, \Laba_L$ and $\Laba_B$,
which stand for \emph{high}, \emph{low}
 and \emph{boundary}
labels.

Given a process, the multilevel security policy may be established
by deciding which ambients are the ones responsible for confining
confidential information. These are all labelled with boundary
labels from set $\Laba_B$ and we will refer to them as
\emph{boundary ambients}. Thus, all the {\it high level ambients}
must be contained in a boundary ambient and labelled with labels
from set $\Laba_H$. Finally, all the external ambients are
considered {\it low level} ones and they are consequently labelled
with labels from set $\Laba_L$. This is how we will always label
processes, and it corresponds to defining the security policy:
what is secret, what is not, what is a container of possible
secrets. In all the examples, we will use the following notation
for labels: $b \in \Laba_B, h \in \Laba_H$, $m,m^{'}\in \Laba_L$
and $c, ch, cl, cm, cm^{'} \in \Labt$.

As an example consider the following process:
\[ P_{1} = \boldambient{container}{b}{
\boldambient{hdata}{h}{\act{\souta{c}{container}}{\zero}} } \ | \ Q\]
 where $Q$ contains
some low level ambients. Ambient $container$ is a boundary for the
high level data $hdata$ (note that data are abstractly represented
as ambients). This process is an example of a direct information
flow. Indeed, $P$ may evolve to $ \boldambient{container}{b}{ }\ |
\  \boldambient{hdata}{h}{ } \ | \ Q$, where the high level
$hdata$ is out of any boundary ambient, thus vulnerable and
potentially accessible by any ambient or process in
$Q$.~\footnote{Note that the presence of an ambient may be tested
by trying to open it or by entering and then exiting from it. A
low level ambient may thus test if $hdata$ is present. This may be
seen as reading high level information.} This flow of high level
data/ambients outside the security boundaries is exactly what we
intend to control and avoid. It may be formalized as follows.

\begin{definition}[Unprotected]
Given a process P and a labelling \Laba, ${\tt
Unprotected}~(\ell$,(\I,\Hc)) = true iff $\exists$ $\ell_{1},
..., \ell_{n} \in \Laba_L$ s.t $(env,\ell_{1}),
(\ell_{1},\ell_{2}), ..., (\ell_{n-1},\ell_{n}), (\ell_{n},\ell)
\sqsubseteq \I$.
\end{definition}

\begin{definition}[Protected]
Given a process P and a labelling \Laba, ${\tt
Protected}~(\ell$,(\I,\Hc)) = true iff $\neg {\tt
Unprotected}~(\ell$,(\I,\Hc)).
\end{definition}

\begin{definition}[Information Leakage]
Given a process P and a labelling \Laba, P leaks secret h $\in
\Laba_H$ iff $\;\exists Q, P \rightarrow ^{*} Q$ such that ${\tt
Unprotected}~(h,\beta^{CF}(Q)$).
\end{definition}

In distributed and mobile systems, it is unrealistic to consider a
unique boundary, containing all the confidential information. As
an example consider two different sites $venice$ and $london$,
each with some set of confidential information that need to be
protected. This can be modeled by defining two boundary ambients,
one for each site: $\boldambient{venice}{b}{ Q_1 }\ | \
\boldambient{london}{b}{ Q_2 } \ | \ Q$. In order to make the
model applicable, it is certainly needed a mechanism for moving
confidential data from one boundary to another one. This is
achieved through another boundary ambient which moves out from the
first protected area and into the second one. The following
example, also depicted in Figure~\ref{example}, describes the
exchange of confidential information between the two sites
$venice$ and $london$:
\[
P_{2} = \boldambient{venice}{b}{ \boldambient{send}{b}{
\act{\souta{c}{venice}}{\sina{c}{london}} \ | \
\boldambient{hdata}{h}} }\ | \
 \boldambient{london}{b}{ \sopena{c}{send} }
\ | \ Q
\]
The process may evolve to the following one (see steps (b) and (c)
of Figure~\ref{example}):
\[ \boldambient{venice}{b}{ }\ | \
\boldambient{london}{b}{ \sopena{c}{send} \ | \ \boldambient{send}{b}{
 \boldambient{hdata}{h}}} \ | \ Q  \]
and finally to (see step (d) of Figure~\ref{example}):
\[ \boldambient{venice}{b}{ }\ | \
\boldambient{london}{b}{
 \boldambient{hdata}{h}} \ | \ Q  \]

\noindent Note that $send$ is labelled as a boundary ambient. Thus, high
 level data $hdata$ is always protected by boundary ambients, during the whole execution.
 Observe that in this example we use the same label for all boundary ambients.
 If we were interested to distinguish ambient nestings inside different boundaries, it
 would be enough to assign different boundary labels.

\infigqui{exampleTOT.eps}{example}{Venice and London exchange confidential information}


\subsection{Verifying Absence of Information Leakage}
\label{leakabsence} In this section, we study how to verify that
no leakage of secret data/ambients outside the boundary ambients
is possible. A natural approach could be the direct application of
the control flow of~\cite{HJNN99ai} reported in
section~\ref{cfsec}.

\begin{corollary}
\label{coroNielson} Let $P$ be a process such that
 $ \ \repa{env}{P} \sqsubseteq (\hat{I},\hat{H}) \  \  \wedge  \ \
 \IHrel{P}  \ \wedge \ h \in \Laba_H \ s.t.\ {\tt Unprotected}~(h,(\I,\Hc))
 \Rightarrow$ P does not leak secret h.
\end{corollary}
\begin{proof}
By contradiction, assume that $P$ leaks secret $h$, thus there exists a process $Q$ s.t. $P \rightarrow^{*} Q$ and ${\tt
Un\-pro\-tec\-ted}~(h,\repa{}{Q})$. By iterating
Theorem~\ref{theo}, we obtain that $\repa{}{Q} \sqsubseteq
(\I,\Hc)$. From ${\tt Unprotected}~(h,\repa{}{Q})$ and
$\repa{}{Q} \sqsubseteq (\I,\Hc)$, it follows that ${\tt Unprotected}~(h,(\hat{I},\hat{H}))$, leading to a contradiction.\hfill{} $\Box$
\end{proof}

\vspace{0,3cm} As an example, consider again the process presented above:
\[ P_{2} = \boldambient{venice}{b}{
\boldambient{send}{b}{ \act{\souta{c}{venice}}{\sina{c}{london}} \ | \
\boldambient{hdata}{h}} }\ | \ \boldambient{london}{b}{ \sopena{c}{send} }
\] The least analysis for this process can be easily shown to be
the following:
\begin{eqnarray*}
\I_{2} &= &\{ (env, b), (b,b), (b,h), (b,c) \}  \\
\Hc_{2} & = & \{  (b, venice), (b, send), (b,london), (h, hdata)
\}
\end{eqnarray*}
Notice that $h$ is always contained inside $b$, i.e. it is
protected by a boundary ambient. Formally, $\repa{env}{P_{2}}
\sqsubseteq (\I_2,\Hc_2)$, $\IHrelNumb{2}{P}$ and ${\tt Protected}~(h,(\I_{2},\Hc_{2}))$,
thus Corollary~\ref{coroNielson} guarantees that $P_{2}$
does not leak secret $h$.

However, the fact that the analysis simply collects all the potential nesting
without considering the temporal ordering of the events, may sometimes lead to unnecessary approximations. As an example, consider again process $P_{2}$ above, and suppose that high level data is willing to enter some filter process, which could possibly be low level code:
\[
\begin{array}{c}
P_{3} = \boldambient{venice}{b}{
\boldambient{send}{b}{ \act{\souta{c}{venice}}{\sina{c}{london}}
\ | \ \boldambient{hdata}{h}{\sina{ch}{filter}}} }\ | \ \\
| \ \boldambient{london}{b}{ \sopena{c}{send} } \ | \
\boldambient{filter}{m}{\sina{c}{send}} \ | \  \sopena{cl}{filter}
\end{array}
\]
Note that the filter behaves correctly with respect to multilevel security
rules, i.e. it only enters boundaries. In particular,
this means that it will never
carry high level data outside the security boundaries.
However, if we perform the control flow analysis we obtain the following
least solution:
\begin{eqnarray*}
\I_3 &= &\{ (env, b), (env, h), (env, m), (env, cl),
(env, c),(b,b), (b,h), (b,m), (b,c), \\
& & (h,ch), (m,h), (m,c) \}  \\
\Hc_3 & = & \{  (b, venice), (b, send), (b,london), (h, hdata),
(m,filter) \}
\end{eqnarray*}
Note that in this solution $h$ appears at the environment level, leading to ${\tt Unprotected}~(h,(\I_3,\Hc_3)))$, showing
a potential attack. However, as observed before, there is no
execution leading to such a situation. The reason why the analysis
looses precision here, is due to the fact that $h$ enters a $m$
ambient which might be opened at the environment level, but the
analysis does not capture the fact that $h$ enters $m$ only after
it has crossed the boundary, and then it never gets out of it.
\hspace{.5cm}

\subsection{A Syntactic Approach}
\label{syntactic}

Syntactic conditions may be imposed  on
processes that are sufficient to prove the absence of leakage of
secret data/ambients outside the  boundary ambients. Moreover,
such conditions properly deal with the situation discussed
before. Let us briefly recall the main results in this direction, as first presented in~\cite{concoord01}.

The idea is to control the $\souta{l}{n}$ and $\sopena{l}{n}$
capabilities executed on
a boundary ambient $n$. In particular, we require that such
capabilities may only be performed by boundary ambients.

First, we characterize a subset of capability labels, in order to
mark {\it out} and {\it open} capabilities that refer to boundary ambients.
Let $\Labt_O \subseteq \Labt$  be the subset of labels that refer to
{\it out} and {\it open} capabilities, and let $\Labt_{BM}  \subseteq \Labt_O$
be a subset of  this set of {\it out} and {\it open} capability labels
($BM$ stands for \emph{boundary move} capabilities). Let also $\phi: \Labt
\rightarrow \wp({\textbf{\textsf{Amb}}})$ be a function that maps a capability label $\ell^t$ to the set of ambient names on which all the capabilities labelled by $\ell^t$ operate.

Given a process $P$, the conditions that should be imposed on $(\I_0,\Hc_0)$ =
$\repa{env}{P}$ to guarantee absence of information
leakage are the following.
\[
\begin{array}{lrcl}
%(i) & (\ell^a,\ell^t)\in \I_0, \ell_a \in \Laba_H, \ell^t \in \Labt_O
%& \Rightarrow & \ell^t \in \Labt_{BM}
%\\
(i) & (\ell^a, n) \in \Hc_0, \ell^a \in \Laba_B, n \in \phi(\ell^t),
\ell^t \in \Labt_O
& \Rightarrow & \ell^t \in \Labt_{BM}  \\
(ii) & (\ell, \ell') \in \I_0, \ell' \in \Labt_{BM}&  \Rightarrow & \ell \in \Laba_B
\end{array}
\]

\noindent Observe that condition $(i)$ turns out to be a well-formedness
condition over labelling. It requires that all the $out$ and
$open$ capabilities that operate on boundary ambients are labelled
as boundary moves (i.e., with labels in set $\Labt_{BM}$). If this
condition is initially satisfied by $P$ (i.e., by
$\repa{env}{P}$), then it will hold also for every derivative
of $P$, as the labelling cannot change during process execution.

Condition $(ii)$ requires that every $out$ and $open$ boundary
move is executed inside a boundary ambient. Note that, in general,
this may be not preserved when $P$ evolves. Indeed, the following
theorem states that also condition $(ii)$ is preserved, within every
execution of $P$.

\begin{theorem}
If the representation function $\repa{env}{P}$ fulfills conditions $(i)-(ii)$, then the least solution $\IHrel{P}$ to
the control flow analysis in~\cite{HJNN99ai} enjoys these conditions as well.
\end{theorem}
\begin{proof}
Let $(\I_{\beta},\Hc_{\beta}) = \repa{env}{P}$, and assume $(\I_{\beta},\Hc_{\beta})$ fulfills conditions {\it (i)} and {\it (ii)}. Now consider the least solution $(\I,\Hc) \models^{CF} P$ (such that $\repa{env}{P} \sqsubseteq (\I,\Hc)$). To be a least solution, a pair $(\I,\Hc)$ must satisfy $\Hc = \Hc_{\beta}$. In fact, notice that the analysis requires no changes to \Hc, thus the least \Hc containing $\Hc_{\beta}$ is $\Hc_{\beta}$ itself.
This proves that the least solution $(\I,\Hc)$ satisfies {\it (i)}.


Let us now turn to the first component of $(\I,\Hc)$. A way for calculating the least solution is to start from \repa{env}{P}, and then add all the pairs required by the analysis, until a fix point is reached.
Notice that every nesting in $\I \setminus \I_{\beta}$ (i.e., all the nestings added by the analysis) should have been required by at least one of the capability rules. If this is not the case, we could remove this kind of nestings, obtaining a smaller analysis, leading to a contradiction.

Let $(\ell,\ell^{'}) \in \I \setminus \I_{\beta}$ and $\ell^{'} \in \Labt_{BM}$. Notice that $\ell^{'}$ is a transition label, thus the pair $(\ell,\ell^{'})$ may only have been added by the {\it open} rule (in fact, {\it in} and {\it out} rules add pairs $(\lap,\la)$ with $\la \in \Laba$). By induction over the fix point algorithm steps, we may assume that before the application of the {\it open} rule the pair $(\I,\Hc)$ satisfies both {\it (i)} and {\it (ii)} conditions.
Now, we consider $\I \cup \{ (\la,\ell^{'}) \ | \ (\lap,\ell^{'}) \in \I\}$ with $(\la,\lt) \in \I \wedge (\la,\lap) \in \I \wedge (\lap,n) \in \Hc$. We focus on the case $\ell^{'} \in \Labt_{BM}$.

Notice that we have $open^{\lt} n$, thus $n \in \phi(\ell^t)$. As $\ell^{'} \in \Labt_{BM}$ and $(\lap,\ell^{'}) \in \I$, by induction on {\it (ii)}, we have that $\lap \in \Laba_B$. By induction on {\it (i)}, we obtain that $\lt \in \Labt_{BM}$, too. By applying again induction on {\it (ii)}, we also obtain that $\la \in \Laba_B$. This means that the set $\{ (\la,\ell^{'}) \ | \ (\lap,\ell^{'}) \in \I\}$, where $\ell^{'} \in \Labt_{BM}$ adds to \I only pairs with $\la \in \Laba_B$, thus still satisfying {\it (ii)}. \hfill{} $\Box$
\end{proof}

\vspace{0.5cm} \noindent Condition $(ii)$ basically states two
important behavioral properties: every time a boundary
ambient is opened, this is done inside another boundary ambient;
the only ambients that may exit from boundary ambients are
boundary ambients. By induction on reduction rules of Mobile
Ambients it is easy to prove the following information flow
theorem:
\begin{theorem}
If $\repa{env}{P}$ fulfills conditions $(i) - (ii)$, then
process P does not leak any secret h $\in \Laba_H$.
\end{theorem}
Note that the two conditions above are definitely easy to check. Consider
again the examples presented above. In particular,
\[ P_{1} = \boldambient{container}{b}{
\boldambient{hdata}{h}{\act{\souta{c}{container}}{\zero}} } \ | \ Q\]
does not satisfy condition $(ii)$. In fact, $\souta{c}{container}$ should be labelled as a boundary move by condition $(i)$. However this makes a boundary
move executable in a high level ambient, invalidating condition $(ii)$.
On the other side, the second example
\[
\begin{array}{c}
P_{2} = \boldambient{venice}{b}{ \boldambient{send}{b}{
\act{\souta{c}{venice}}{\sina{c}{london}} \ | \
\boldambient{hdata}{h}} }\ | \ \boldambient{london}{b}{
\sopena{c}{send} } \ | \ Q
\end{array}
\]
 fulfills both the conditions, with $c \in \Labt_{BM}$.
 This proves that $hdata$, in every execution,
 is always nested inside a boundary ambient, i.e. $P_{2}$ does not leak secret $h$.

The syntactic conditions successfully applies also to the extended
example with $hdata$ entering the filter:
\[
\begin{array}{c}
P_{3} = \boldambient{venice}{b}{ \boldambient{send}{b}{
\act{\souta{c}{venice}}{\sina{c}{london}}
\ | \ \boldambient{hdata}{h}{\sina{ch}{filter}}} }\ | \ \\
| \ \boldambient{london}{b}{ \sopena{c}{send} } \ | \
\boldambient{filter}{m}{\sina{c}{send}} \ | \  \sopena{cl}{filter}
\end{array}
\]

Also in this case, we are able to prove that $P_{3}$ does not leak
$h$. Note that this was not provable through the control
flow analysis introduced in Section~\ref{cfsec}.

The approach above may also be adapted to the case in which
the external environment (e.g. any malicious
process put in parallel with the analyzed process $P$) does not fulfill the
required conditions. This is indeed reasonable in a distributed open
system. The idea is to suitably restrict the scope of
boundary ambients and provide
low level ambients with
some ``taxi'' processes that, once entered, bring the client inside
restricted boundaries. Let $b_1, \ldots, b_n$ represent all the boundary
ambients of process $P$. Then consider process
\[ (\nu b_1, \ldots, b_n) (P \ | \  \boldambient{!t_1}{}{\sina{l}{b_1}} \ | \ \ldots \ | \
\boldambient{!t_n}{}{\sina{l}{b_n}} ) \ | \ Q
\]
As $b_1, \ldots, b_n$ are restricted names, they may not appear in $Q$.
As a consequence, if $P$ fulfills the conditions $(i) - (ii)$, this is
sufficient to prove that the whole system (whatever $Q$ is considered)
satisfies such conditions, too. It is indeed simple to prove the following:
\begin{proposition}
If $\repa{env}{P}$ fulfills conditions $(i) - (ii)$, then, for all
 $Q$ (labelled in $\Laba_L \cup \Labt \setminus \Labt_{BM}$),
\[ \repa{env}{(\nu b_1, \ldots, b_n) (P \ | \ \boldambient{!t_1}{}{\sina{l}{b_1}} \ | \
\ldots \ | \ \boldambient{!t_n}{}{\sina{l}{b_n}} ) \ | \ Q}
\]
 fulfills conditions $(i) - (ii)$.
\end{proposition}
Note that processes $\boldambient{!t_i}{}{\sina{l}{b_i}}$ allow
any low level ambient to enter boundary $b_i$. So, legitimate
flows from low to high level are possible even if boundaries are
restricted. Note also that the condition on the labelling of $Q$
simply means that $Q$ only contains low level ambients and its
capabilities are not (incorrectly) labelled as boundary moves.


\section{Refining the Control Flow Analysis}\label{CFA}
In this section we introduce a refinement of the Control Flow
Analysis of~\cite{HJNN99ai} reported in Section~\ref{cfsec}, that
incorporates into the analysis the ideas discussed in
Section~\ref{verification}, thus yielding to a more accurate tool
for detecting unwanted boundary crossings. The resulting analysis
improves also with respect to the syntactic properties presented
in Section~\ref{syntactic}.

The main idea is to split the $\I$ component of the abstract
domain in two (not necessarily disjoint) sets, that maintain nesting
information about ambients protected by boundaries, and about
``unprotected'' ones, respectively.

\vspace{0.5cm} \noindent The refined control flow analysis works
on triplets $(\IB,\IE,\Hc)$, where:
\begin{itemize}
\item[-] The first component $\IB$
is an element of $\wp(\Laba \times (\Laba \cup \Labt))$. If a
process contains either a capability or an ambient labelled $\ell$
inside an ambient labelled $\ell^a$ which is a boundary or an
ambient nested inside a boundary (referred as \textit{protected
ambient}) then $(\ell^a,\ell)$ is expected to belong to
$\IB$. As long as a high level datum is contained inside a
protected ambient there is no unwanted information flow.
\item[-] The second component $\IE$
is still an element of $\wp(\Laba \times (\Laba \cup \Labt))$. If
a process contains either a capability or an ambient labelled
$\ell$ inside an ambient labelled $\ell^a$ which is not protected,
then $(\ell^a,\ell)$ is expected to belong to $\IE$.
\item[-] The third component $\Hc$, as before, keeps track of the correspondence between
names and labels. If a process contains an ambient labelled
$\ell^a$ with name $n$, then $(\ell^a,n)$ is expected to belong to
$\Hc$.
\end{itemize}

\noindent Also in this case, the analysis is defined by a
representation function and a specification. They are depicted,
respectively, in Figure~\ref{n_cfa_repr} and Figure~\ref{n_cfa_models}.

%Dire che la beta raccatta le info nello stato iniziale.
\begin{example}\label{runEx3}
{\rm Let $P$ be the process of Example~\ref{runEx1}, i.e. of the form:
P = \boldambient{n}{\ell_{1}^{a}}{\boldambient{m}{\ell_{2}^{a}}{\souta{\lt}{n}}}, with $\ell_{1}^{a} \in \Laba_B$ and $\ell_{2}^{a} \in \Laba_L$, thus the representation function of P is the following:
$\repab{env}{P} =
(\{(\ell_{1}^{a},\ell_{2}^{a}),(\ell_{2}^{a},\lt)\},
 \{(env,\ell_{1}^{a})\},
 \{(\ell_{1}^{a},n),(\ell_{2}^{a},m)\})$ }.
\end{example}

%L'analisi raffina la in out e open di Nielson per collezionare correttamente le info di \IB e \IE.
%Ad esempio:
\begin{example}\label{runEx4}
{\rm Let $P$ be the process of Example~\ref{runEx3}. The
least solution of P is the triplet (\IB,\IE,\Hc) where \IB = $\{
(\ell_{1}^{a},\ell_{2}^{a}),(\ell_{2}^{a},\lt)\}$,
\IE = $\{(env,\ell_{1}^{a}),(env,\ell_{2}^{a}),
(\ell_{2}^{a},\lt)\}$, and $\Hc =
\{(\ell_{1}^{a},n),(\ell_{2}^{a},m) \}$. Observe that $(\IB,\IE,\Hc)$ strictly contains \repab{env}{P}, as expected being $(\IB,\IE,\Hc)$ a safe approximation.}
\end{example}

\noindent A pictorial representation of the most interesting
application of the \textit{in}-rule (i.e. the last one: a boundary
crossing) is provided by Figure~\ref{crossing}: the sets \IE \ and
\IB \ before and after the move of ambient {\it k} into ambient
{\it n} are represented by graphs (a) and (b), respectively. In
particular, ambient $k$ labelled as $\ell \not\in \Laba_B$ is
willing to enter ambient $n$ labelled as $\ell^{'} \in \Laba_B$.
In this case, all the nestings below $\ell$ have to be copied in \IB\;since
after the $in$ move they become protected.

%\renewcommand{\baselinestretch}{1}

\begin{figure}
\begin{small}
\centering

\fbox{\parbox{5.7in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lll}
& \repab{}{P} & = &
  \repab{env,False}{P} \\
\\[\specskip]
\\[\specskip]
\cas{res} & \repab{\ell,Protected}{\rest{n}{P}} & = & \repab{\ell,Protected}{P}\\
\\[\specskip]
\cas{zero} & \repab{\ell,Protected}{\zero} & = & (\emptyset,\emptyset,\emptyset)\\
\\[\specskip]
\cas{par} & \repab{\ell,Protected}{\comp{P}{Q}} & = &
   \repab{\ell,Protected}{P} \lub \repab{\ell,Protected}{Q}\\
\\[\specskip]
\cas{repl} & \repab{\ell,Protected}{\repl{P}} & = & \repab{\ell,Protected}{P}\\
\\[\specskip]
\cas{amb} & \repab{\ell,Protected}{\boldambient{n}{\la}{P}} & = &
\textmd{case \textit{Protected} of}\\
& & & \ \ \textmd{True\ :\ } \repab{\la,Protected}{P} \lub (\set{(\ell,\la)},\emptyset,\set{(\la,n)}) \\
& & & \ \ \textmd{False:\ if ($\ell_a \in \Laba_B$)  \ then} \\
& & & \ \ \ \ \ \ \ \ \ \ \ \textmd{let \ Protected$^{'}$ = True else  Protected$^{'}$ = False in}\\
& & & \ \ \ \ \ \ \ \ \ \ \ \repab{\la,Protected^{'}}{P} \lub (\emptyset,\set{(\ell,\la)},\set{(\la,n)}) \\
\\[\specskip]
\cas{in} & \repab{\ell,Protected}{\sincap{n}{P}} & = &
\textmd{case \textit{Protected} of}\\
& & & \ \ \textmd{True\ :\ } \repab{\ell,Protected}{P} \lub (\set{(\ell,\lt)},\emptyset,\emptyset)\\
& & & \ \ \textmd{False:\ } \repab{\ell,Protected}{P} \lub (\emptyset,\set{(\ell,\lt)},\emptyset)\\
\\[\specskip]
\cas{out} & \repab{\ell,Protected}{\soutcap{n}{P}} & = &
\textmd{case \textit{Protected} of}\\
& & & \ \ \textmd{True\ :\ } \repab{\ell,Protected}{P} \lub (\set{(\ell,\lt)},\emptyset,\emptyset)\\
& & & \ \ \textmd{False:\ } \repab{\ell,Protected}{P} \lub (\emptyset,\set{(\ell,\lt)},\emptyset)\\
\\[\specskip]
\cas{open} & \repab{\ell,Protected}{\sopencap{n}{P}} & = &
\textmd{case \textit{Protected} of}\\
& & & \ \ \textmd{True\ :\ } \repab{\ell,Protected}{P} \lub (\set{(\ell,\lt)},\emptyset,\emptyset)\\
& & & \ \ \textmd{False:\ } \repab{\ell,Protected}{P} \lub
(\emptyset,\set{(\ell,\lt)},\emptyset)
\end{array}
\end{displaymath}
}}
\caption{Representation Function for the refined Control Flow Analysis}
\label{n_cfa_repr}
\end{small}
\end{figure}



\begin{figure}
\begin{small}
\centering

\fbox{\parbox{6.3in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lcl}
\cas{res} & \IHrelb{\rest{n}{P}}& \hviss &\IHrelb{P}\\
\\[\specskip]
\cas{zero} & \IHrelb{\zero} & \multicolumn{2}{l}{\always}\\
\\[\specskip]
\cas{par} & \IHrelb{\comp{P}{Q}}& \hviss & \IHrelb{P} \og \IHrelb{Q}\\
\\[\specskip]
\cas{repl} & \IHrelb{\repl{P}}& \hviss & \IHrelb{P}\\
\\[\specskip]
\cas{amb} & \IHrelb{\boldambient{n}{\la}{P}} & \hviss & \IHrelb{P}\\
\\[\specskip]
\cas{in} & \IHrelb{\sincap{n}{P}}& \hviss & \IHrelb{P} \og \\
 &  \multicolumn{3}{l}{
    %\capindent
    \begin{array}[t]{@{}l}
    \foralled{\la,\lap,\lapp\in\Laba}\\
    \mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\lapp}{\la}{\IB} \og \infrel{\lapp}{\lap}{\IB} \og \infrel{\lap}{n}{\Hc}) \\
    \quad \implies \infrel{\lap}{\la}{\IB} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\lapp}{\la}{\IE} \og \infrel{\lapp}{\lap}{\IE} \og \la \in \Laba_B \og \infrel{\lap}{n}{\Hc}) \implies\\
    \quad \mbox{if (\;} \lap \in \Laba_B ) \mbox{\;then\;} \infrel{\lap}{\la}{\IB} \\
    \quad \mbox{else\;} \infrel{\lap}{\la}{\IE} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IE} \og \infrel{\lapp}{\la}{\IE} \og \infrel{\lapp}{\lap}{\IE} \og \infrel{\lap}{n}{\Hc}) \implies \\
\quad \mbox{if (\;} \lap \in \Laba_B ) \\
    \quad \quad \mbox{\;then\;}  \infrel{\lap}{\la}{\IB} \og \delmgd{\set{\comp{\infrel{\ell}{\ell'}{\IE}}{path_{E}(\la,\ell)}}}{\IB}  \\
    \quad \mbox{else\;} \infrel{\lap}{\la}{\IE} \\
    \end{array}}\\
\\[\specskip]
\cas{out} & \IHrelb{\soutcap{n}{P}}& \hviss & \IHrelb{P} \og \\
 &  \multicolumn{3}{l}{
    %\capindent
    \begin{array}[t]{@{}l}
    \foralled{\la,\lap,\lapp\in\Laba} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\lap}{\la}{\IE\cup\IB} \og \infrel{\lapp}{\lap}{\IE} \og \infrel{\lap}{n}{\Hc}) \implies \\
    \quad \mbox{if (\;} \la \in \Laba_B ) \mbox{\;then\;} \infrel{\lapp}{\la}{\IE} \\
    \quad \mbox{else\;} \infrel{\lapp}{\la}{\IE} \og \delmgd{\set{\comp{\infrel{\ell}{\ell'}{\IB}}{path_{B}(\la,\ell)}}}{\IE}\\
    \mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\lap}{\la}{\IB} \og \infrel{\lapp}{\lap}{\IB} \og \infrel{\lap}{n}{\Hc}) \\
    \quad \implies \infrel{\lapp}{\la}{\IB} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IE} \og \infrel{\lap}{\la}{\IE} \og \infrel{\lapp}{\lap}{\IE} \og \infrel{\lap}{n}{\Hc}) \\
    \quad \implies \infrel{\lapp}{\la}{\IE}\\
    \end{array}}\\
\\[\specskip]
\cas{open} & \IHrelb{\sopencap{n}{P}}& \hviss & \IHrelb{P} \og \\
 &  \multicolumn{3}{l}{
    %\capindent
    \begin{array}[t]{@{}l}
        \foralled{\la,\lap\in\Laba} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IE} \og \infrel{\la}{\lap}{\IE} \og \infrel{\lap}{n}{\Hc}) \implies \\
        \quad \mbox{if (\;} \lap \in \Laba_B ) \mbox{\;then} \delmgd{\set{\comp{(\la,\lapp)}{\infrel{\lap}{\lapp}{\IB}}}}{\IE} \og \\
    \quad \quad \delmgd{\set{\comp{(\ell,\ell')}{\infrel{\ell}{\ell'}{\IB} \og (\lap,\ell^{''}) \in \IB \og path_{B}(\ell^{''},\ell) }}}{\IE}\\
    \quad \mbox{else\;} \delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{\IE}}}}{\IE} \\
\mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\la}{\lap}{\IB} \og \infrel{\lap}{n}{\Hc}) \\
    \quad \implies \delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{\IB}}}}{\IB} \\
    \end{array}}\\
\end{array}
\end{displaymath}
}}
\caption{Specification of the refined Control Flow Analysis}
\label{n_cfa_models}
\end{small}
\end{figure}

%\renewcommand{\baselinestretch}{2}

%\infigqui{analisi_in_iii2.eps}{crossing}{The \textit{in}-rule: boundary crossing}
\infigqui{boundCross.eps}{crossing}{The \textit{in}-rule: boundary crossing}

\vspace{0.5cm} \noindent Observe that within the specification of
the analysis (depicted in Figure~\ref{n_cfa_models}), some
predicates are introduced that simplify the notation, namely

\begin{itemize}
  \item
  $path_{B}(\la,\ell) =
  \begin{cases}
    True   & \text{if} \ \la = \ell \vee \exists \ell_{1},\ell_{2},...,\ell_{n}\not\in\Laba_B: n \geq 0\\
            & (\la,\ell_{1}),(\ell_{1},\ell_{2}),...,(\ell_{n},\ell)\in\IB \og \la,\ell \not\in \Laba_B ,\\
    False & \text{otherwise}.
  \end{cases}$

  \item
  $path_{E}(\la,\ell) =
  \begin{cases}
    True   & \text{if} \ \la = \ell \vee \exists \ell_{1},\ell_{2},...,\ell_{n}\not\in\Laba_B: n \geq 0\\
            & (\la,\ell_{1}),(\ell_{1},\ell_{2}),...,(\ell_{n},\ell)\in\IE \og \la,\ell \not\in \Laba_B ,\\
    False & \text{otherwise}.
  \end{cases}$

\end{itemize}

\noindent The following holds.
\begin{theorem}\label{theoCorr} Let $P$ and $Q$ be two processes such that
 $ \ \repab{env}{P} \sqsubseteq (\IB,\IE,\Hc) \  \  \wedge  \ \
 \IHrelb{P}  \ \wedge \ P
\rightarrow Q \ \ $ then  $\ \ \repab{env}{Q} \sqsubseteq
(\IB,\IE,\Hc) \ \  \wedge \ \
 \IHrelb{Q}$.
\end{theorem}

\noindent The proof of the Theorem can be obtained by showing that the new control flow analysis is induced from the analysis with occurrence counting of~\cite{nielsonAbstr}, and it can be found in Section~\ref{proof}.


\vspace{0.5cm} \noindent The result of the analysis should be
read, as expected, in terms of information flows. No leakage of
secret data/ambients outside the boundary ambients is possible if
in the analysis $h$ (high level datum) does not appear in any of
the pairs belonging to $\IE$.

\begin{corollary}
Let P be a process and h $\in \Laba_H$ a high level label. Let
$\repab{}{P} \sqsubseteq (\IB,\IE,\Hc)$ and $ \IHrelb{P}$ and $ \forall (\ell^{'},\ell^{''}) \in \IE, \ell^{''} \neq h$. Then, P does not leak secret h.
\end{corollary}

\vspace{0.5cm} \noindent What about accuracy? The analysis just
introduced is a refinement of the CFA in~\cite{HJNN99ai} and it
properly deals with boundary nestings, in the spirit of Section~\ref{verification}. Referring again to example process $P_{3}$, we
may observe that our refined analysis properly captures the fact
that the ``filter'' is entered by confidential data only once it
inside of boundary ``london''.

\noindent In addition, it definitely improves in accuracy with
respect to the mentioned syntactic property introduced in~\cite{concoord01}. Consider, for instance, the following example,
where  the process discussed in the previous sections is extended
by allowing an {\it application} (say  an applet) to be downloaded
from the {\it web} within {\it london}; then, the application may
open the ambient {\it send} and disappear.
\begin{small}
\[
\begin{array}{c}

P_{4} = venice^{b_1} \leftbb send^{b_3} \leftbb \Out^c venice. \In^c london \ | \ hdata^h \ \leftbb \In^{ch} filter \rightbb  \rightbb \ | \\
| \ download^{m^{'}} \leftbb \Out^{cm^{'}} venice. \In^{cm^{'}} web.\In^{cm^{'}} london \rightbb  \rightbb \ | \ \\
| \ london^{b_2} \leftbb \Open^c web . \Open^c application \rightbb  \ | \\
web^{m} \leftbb application^{m} \leftbb \Open^{cm} send. filter^{m} \leftbb \rightbb \rightbb \ | \ \Open^{cm} download \rightbb \\

\end{array}
\]
\end{small}

\noindent Observe that in this case there is no information flow,
as the application is not exporting any data out of the london
boundary. In this case, our refined CFA yields to positive
information (see the least solution reported below), whereas the
syntactic property cannot be successfully applied. In fact, the
(untrusted) application downloaded from the net is not a boundary,
its  {\it open} capability is labelled $BM$ by the first rule, and
thus the second rule cannot be satisfied since ambient {\it
application} is not labelled as a boundary (i.e. $m \in \Laba_L$).
The least solution of the analysis $S_{4}=(\IB,\IE,Hc)$ is:

\begin{eqnarray*}
\IB &= &\{ (b_1,b_3), (b_1,m'), (b_3,h),
 (b_3,c), (h,ch), (m',cm'),
(b_2,b_3), (b_2,h), (b_2,m'), (b_2,b_2),
\\& & (b_2,m), (b_2,c), (b_2,cm'),
(b_2,cm), (m,h), (m,m'), (m,b_2), \\ & & (m,m), (m,cm'),
 (m,cm)\}\\
\IE &= &\{ (env,b_1), (env,b_3),
 (env,m'), (env,b_2), (env,m),
(m',cm'), (m,m'), (m,b_2), (m,m), (m,cm'), (m,cm)
\} \\
\hat{H} & = & \{ (b_1, venice), (b_3, send),
(b_2,london), (h,
hdata), (m',download), \\
& & (m,web), (m,application), (m,filter) \}
\end{eqnarray*}

\noindent Observe that the result is also more accurate than the
Hansen-Jensen-Nielsons's CFA~\cite{HJNN99ai} which computes the following
least solution:

\begin{eqnarray*}
\I_{4} &= &\{ (env,b_1), (env,b_3), (env,m'), (env,b_2), (env,m),
(b_1,b_3), (b_1,m'), (b_3,h), (b_3,c), (h,ch),\\ & & (m',cm'),
(b_2,b_3), (b_2,h), (b_2,m'), (b_2,b_2), (b_2,m), (b_2,c),
(b_2,cm'), (b_2,cm), (m,h), \\ & & (m,m'), (m,b_2), (m,m),
(m,cm'), (m,cm)
\}  \\
\Hc_{4} & = & \{  (b_1, venice), (b_3, send), (b_2,london), (h,
hdata), (m',download), \\
& & (m,web), (m,application), (m,filter) \}
\end{eqnarray*}

\noindent Note that \textit{h} appears inside a \textit{m} ambient
that at the beginning of the process is at the environmental
level, but the analysis does not capture the fact that \textit{h}
enters \textit{m} only after it has crossed the boundary and can
never return back.

\section{Correctness of the Refined Control Flow Analysis}
\label{proof}

In this section we prove the correctness of our refined CFA, as stated by Theorem~\ref{theoCorr}. To do this, we strictly follow the approach of~\cite{nielsonAbstr}, i.e. we prove that the new control
flow analysis is \textit{induced} from the analysis with
occurrence counting. As a consequence, the analysis is
semantically correct: each reduction of the semantics is
adequately mimicked in the analysis.

\noindent First, let us recall some auxiliary definitions in~\cite{nielsonAbstr}

\begin{itemize}
\item {\bf Induced Satisfaction Relation.}

\noindent Let $(\alpha,\gamma)$ be a Galois connection of $\mathcal{A}$ in $\mathcal{A}^{'}$, and let $\models: \mathcal{A} \times \Proc \rightarrow \{ {\tt tt, ff} \}$ and $\models^{'}: \mathcal{A^{'}} \times \Proc \rightarrow \{ {\tt tt, ff} \}$ be satisfaction relations. \\ The relation $\models$ is said to be {\tt induced} from the relation $\models^{'}$ when
\[
\forall A \in \mathcal{A}, P \in \Proc: \gamma(A) \models^{'} P \Longleftrightarrow A \models P.
\]

\item {\bf Approximate Satisfaction Relation.}

\noindent Let $(\alpha,\gamma)$ be a Galois connection of $\mathcal{A}$ in $\mathcal{A}^{'}$, and let $\models: \mathcal{A} \times \Proc \rightarrow \{ {\tt tt, ff} \}$ and $\models^{'}: \mathcal{A^{'}} \times \Proc \rightarrow \{ {\tt tt, ff} \}$ be satisfaction relations. \\ The relation $\models$ is said to be {\tt approximate} from the relation $\models^{'}$ when
\[
\forall A \in \mathcal{A}, P \in \Proc: \gamma(A) \models^{'} P \Longleftarrow A \models P.
\]

\item {\bf Induced Representation Function.}

\noindent Let $\mathcal{A^{'}}  \mathcal{A}$ be a Galois connection, then a representation function $\beta: \Proc \rightarrow \mathcal{A}$ is said to be {\tt induced} from a representation function $\beta^{'}: \Proc \rightarrow \mathcal{A^{'}}$ whenever:
\[
\alpha \circ \beta^{'} = \beta
\]
\end{itemize}


\begin{proposition}[Preservation of ``global'' correctness~\cite{nielsonAbstr}]\label{global}
Assume $\models, \beta, \models^{'} $ and $ \beta^{'}$ are given such that $\models$ approximates $\models^{'}$ and $\beta$ is induced from $\beta^{'}$, via the Galois connection $\mathcal{A^{'}}  \mathcal{A}$. Then
\[
\beta^{'}(P) \sqsubseteq A^{'} \wedge A^{'} \models^{'} P \wedge P \rightarrow^{*} Q \Rightarrow \beta^{'}(Q) \sqsubseteq A^{'}
\]
implies
\[
\beta^{'}(P) \sqsubseteq A^{'} \wedge A^{'} \models^{'} P \wedge P \rightarrow^{*} Q \Rightarrow \beta^{'}(Q) \sqsubseteq A^{'}
\]
for all P, Q, A and $A^{'}$.
\end{proposition}

\vspace{0.5cm} \noindent The abstraction and concretization
functions $\alphaB, \gammaB$ can be defined in terms of the
occurrence counting domain, where a third
component $\hat{A}$ maintains multiplicity information, as
follows:

\vspace{0.5cm} \noindent Let $\eta^{B}:\ \I \mapsto \IB $ and
$\eta^{E}:\ \I \mapsto \IE $ be functions splitting $\I$ according
to the boundary nestings, in~\footnote{According to~\cite{HJNN99ai}, a triplet \IIH \ is \textit{compatible} whenever
the labels in $\IE\cup\IB$ are consistent with the mapping \Hc. More
formally, if the following condition is satisfied: if
$\infrel{\la}{\ell}{\IE\cup\IB}$ or
$\infrel{\ell}{\la}{\IE\cup\IB}$ then there exists \textit{n} such
that $\infrel{\la}{n}{\IH}$. }

\begin{eqnarray*}
  \alphaB(\mathcal{C}) & = & \bigsqcup\{(\eta^{B}(\I),\eta^{E}(\I),\Hc)\; | \;
(\I,\Hc,\hat{A})\in \mathcal{C}\} \\
  \gammaB(\IB,\IE,\Hc) & = & \{(\I^{'},\Hc^{'},\hat{A}^{'})\; | \;
(\eta^{B}(\I^{'}),\eta^{E}(\I^{'}),\Hc^{'})\sqsubseteq
(\IB,\IE,\Hc)
 \og (\I^{'},\Hc^{'},\hat{A}^{'}) \\
 & &  \textrm{is compatible }  \}
\end{eqnarray*}
The two functions $\eta^{B}$ and $\eta^{E}$ are defined
in terms of protected and unprotected path predicates as follows:
\begin{itemize}
  \item
  $p\_path(\la) =
  \begin{cases}
    True   & \text{iff} \ \exists \ell_{0} \in \Laba_B \og \exists \ell_{1},\ell_{2},...,\ell_{n}: n \geq 0\\
            & (\ell_{0},\ell_{1}),(\ell_{1},\ell_{2}),...,(\ell_{n},\la)\in\I,\\
    False & \text{otherwise}.
  \end{cases}$

  \item
  $u\_path(\la) =
  \begin{cases}
    True   & \text{iff} \ \exists \ell_{1},\ell_{2},...,\ell_{n}: n \geq 0\\
            & (env,\ell_{1}),(\ell_{1},\ell_{2}),...,(\ell_{n},\la) \ \textrm{s.t.}\forall k  \  \ell_{k} \not\in \Laba_B ,\\
    False & \text{otherwise}.
  \end{cases}$
 \end {itemize}

\vspace{0.5cm}
\begin{itemize}
  \item[]$\eta^{B}:\ \wp(\Laba \times (\Laba \cup \Labt)) \rightarrow \wp(\Laba \times (\Laba \cup \Labt))$
  \item[]$\eta^{B} (\I) = \{(\la,\ell) | \ p\_path(\la) \vee \neg u\_path(\la) \} $
  \vspace{0.5cm}
  \item[]$\eta^{E}:\ \wp(\Laba \times (\Laba \cup \Labt)) \rightarrow \wp(\Laba \times (\Laba \cup \Labt))$
  \item[]$\eta^{E}(\I) = \{(\la,\ell) | \ u\_path(\la) \} $
\end{itemize}

\vspace{0.5cm} \noindent The abstraction and concretization
functions $\gammaB, \alphaB$ form a Galois connection of our abstract domain of triplets into \textbf{CountSet};
i.e.
\begin{itemize}
\item both functions are monotone;
\item $\mathcal{C} \subseteq \gammaB(\alphaB(\mathcal{C}))$ for any $\mathcal{C} \in$
\textbf{CountSet};
\item $\alphaB(\gammaB(\IB,\IE,\Hc)) \sqsubseteq (\IB,\IE,\Hc)$ for any triplet $(\IB,\IE,\Hc)$.
\end{itemize}

\vspace{0.5cm}
\noindent The following Proposition states that the refined Control Flow Analysis is induced from the occurrence counting analysis.

% of~\cite{nielsonAbstr}, thus the analysis is semantically correct and Theorem~\ref{theoCorr} holds.

%This leads to a hierarchy of abstractions that very well fits in the Abstract Interpretation
%theory, yielding an expected trade-off between accuracy and efficiency of the analyses.

%\vspace{0.5cm}  \noindent
\begin{proposition}\label{global2} If $P \in
\textbf{Proc}$ and \IIH is compatible then
\[
\gammaB \IHreloc P \Longleftrightarrow \IHrelb P
\]
and
\[
\alphaB(\betaOC(P)) = \betaB(P)
\]
\end{proposition}

\begin{proof} The proof follows the lines of the corresponding one in~\cite{nielsonAbstr}. Namely, it
suffices to prove
\begin{enumerate}
\item $ \gammaB\IHreloc P \Longleftrightarrow \IHrelb P $
\item $ \forall \ell\in\Laba : \alphaB (\{ \eta^{\annoOC}_{\ell}(P) \}) = \betaB_{\ell} (P) $
\end{enumerate}

\vspace{0.3cm} \noindent We just focus on proving point \textit{(i)} by structural
induction on process P (the proof of point {\it (ii)} is trivially obtained by rephrasing the corresponding proof in~\cite{nielsonAbstr}). The base of the induction is case P = 0, which is
always verified. The interesting cases arise when capabilities {\it in}, {\it out} and {\it open} apply.

%In the rest of the proof, we consider the case of \textit{in-}capabilities

\begin{figure}[h]
\centering
\fbox{\parbox{6in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lcl}
\cas{in} & \mathcal{C} \models^{\annoOC}{\sincap{n}{P}}& \hviss &
\mathcal{C} \models^{\annoOC} P \og \forall (\I, \Hc, \A)\in
\mathcal{C} \
: \forall \la, \lap,\lapp :\\
& \multicolumn{3}{l} {\left(\infrel{\la}{\lt}{\I} \og
\infrel{\lapp}{\la}{\I} \og \infrel{\lapp}{\lap}{\I} \og
\infrel{\lap}{n}{\Hc}\right) \Rightarrow }
\\
 &  \multicolumn{3}{l}{
    %\capindent
    \left(
    \begin{array}{@{}l}
            \textrm{case} \A(\la) \textrm{of} \\
            1: (\I \setminus \{(\lapp,\la) \} \cup \{(\lap,\la) \}, \Hc, \A ) \in \mathcal{C} \\
            \quad (\I \setminus \{(\lapp,\la), (\la,\lt) \} \cup \{(\lap,\la) \}, \Hc, \A ) \in \mathcal{C}\\
            \omega: (\I \cup \{(\lap,\la) \}, \Hc, \A ) \in \mathcal{C} \\
            \quad (\I \setminus \{(\lapp,\la) \} \cup \{(\lap,\la) \}, \Hc, \A ) \in \mathcal{C} \\
            \quad (\I \setminus \{(\la,\lt) \} \cup \{(\lap,\la) \}, \Hc, \A ) \in \mathcal{C} \\
            \quad (\I \setminus \{(\lapp,\la), (\la,\lt) \} \cup \{(\lap,\la) \}, \Hc, \A ) \in \mathcal{C}\\
    \end{array} \right)} \\

\\[\specskip]
\end{array}
\end{displaymath}
}} \caption{Specification of the analysis with occurrence counting
(\textit{in-}capabilities) } \label{oc_models_in}
\end{figure}

\begin{figure}[h]
\begin{footnotesize}
\centering
\fbox{\parbox{6in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lcl}
\cas{in} & \IHrelb{\sincap{n}{P}}& \hviss & \IHrelb{P} \og \\
 &  \multicolumn{3}{l}{
    %\capindent
    \begin{array}[t]{@{}l}
    \foralled{\la,\lap,\lapp\in\Laba}\\
    \mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\lapp}{\la}{\IB} \og \infrel{\lapp}{\lap}{\IB} \og \infrel{\lap}{n}{\Hc}) \\
    \quad \implies \infrel{\lap}{\la}{\IB} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\lapp}{\la}{\IE} \og \infrel{\lapp}{\lap}{\IE} \og \la \in \Laba_B \og \infrel{\lap}{n}{\Hc}) \implies\\
    \quad \mbox{if (\;} \lap \in \Laba_B ) \mbox{\;then\;} \infrel{\lap}{\la}{\IB} \\
    \quad \mbox{else\;} \infrel{\lap}{\la}{\IE} \\
    \mbox{case\;}(\infrel{\la}{\lt}{\IE} \og \infrel{\lapp}{\la}{\IE} \og \infrel{\lapp}{\lap}{\IE} \og \infrel{\lap}{n}{\Hc}) \implies \\
\quad \mbox{if (\;} \lap \in \Laba_B ) \\
    \quad \quad \mbox{\;then\;}  \infrel{\lap}{\la}{\IB} \og \delmgd{\set{\comp{\infrel{\ell}{\ell'}{\IE}}{path_{E}(\la,\ell)}}}{\IB}  \\
    \quad \mbox{else\;} \infrel{\lap}{\la}{\IE} \\
    \end{array}}\\
\\[\specskip]
\end{array}
\end{displaymath}
}} \caption{Specification of the refined Control Flow Analysis
(\textit{in-}capabilities)} \label{cfa_models_in}
\end{footnotesize}
\end{figure}


\begin{itemize}
\item Case {\it in} (Figure~\ref{oc_models_in} and Figure~\ref{cfa_models_in}). Proof of ``$\Leftarrow$''. Let us prove that
\begin{displaymath}
\IHrelb in^{\ell^{t}} n.P \Rightarrow \gammaB\IHreloc in^{\ell^{t}} n.P
\end{displaymath}
\noindent From the specification of the analysis depicted in Figure~\ref{cfa_models_in}, it follows that \IHrelb P. So, by
induction hypothesis, we have $\gammaB \IHreloc P $.

\noindent Then, consider $(\I^{'},\Hc^{'},\A^{'})\in
\gammaB(\IB,\IE,\Hc)$ and $\la, \lap, \lapp $ such that
\begin{displaymath}
\infrel{\la}{\lt}{\I^{'}} \og \infrel{\lapp}{\la}{\I^{'}} \og
\infrel{\lapp}{\lap}{\I^{'}} \og \infrel{\lap}{n}{\Hc^{'}}
\end{displaymath}
By definition of $\gammaB$, if $(\I^{'},\Hc^{'},\A^{'})\in
\gammaB(\IB,\IE,\Hc)$, then $(\I^{'},\Hc^{'},\A^{'})$ is
compatible and \linebreak
%\newline
$(\eta^{B}(\I^{'}),\eta^{E}(\I^{'}),\Hc^{'}) \sqsubseteq
(\IB,\IE,\Hc)$. It follows that
\begin{displaymath}
\begin{array}{c}
\infrel{\la}{\lt}{\eta^{B}(\I^{'}) \cup \  \eta^{E}(\I^{'})} \og
\infrel{\lapp}{\la}{\eta^{B}(\I^{'}) \cup \ \eta^{E}(\I^{'})} \og \\
\infrel{\lapp}{\lap}{\eta^{B}(\I^{'}) \cup \ \eta^{E}(\I^{'})} \og
\infrel{\lap}{n}{\Hc}.
\end{array}
\end{displaymath}
We have to consider the three cases in Figure~\ref{cfa_models_in}. the most informative one is case 3, when a boundary crossing occurs. In this case it also holds that either $(\lap,\la) \in \eta^{E}(\I^{'})$ or $\infrel{\lap}{\la}{\eta^{B}(\I^{'})} $ and $ \delmgd{\set{\comp{\infrel{\ell}{\ell'}{\eta^{E}(\I^{'})}}{path_{E}(\la,\ell)}}}{\eta^{B}(\I^{'})}$.

\noindent Then, we may look at the occurrence counting analysis. Observe that all the four triplets of Figure~\ref{oc_models_in}
\begin{displaymath}
    \begin{array}{@{}l}
            (\I \cup \{(\lap,\la) \}, \Hc, \A )\\
            (\I \setminus \{(\lapp,\la) \} \cup \{(\lap,\la) \}, \Hc, \A ) \\
            (\I \setminus \{(\la,\lt) \} \cup \{(\lap,\la) \}, \Hc, \A ) \\
            (\I \setminus \{(\lapp,\la), (\la,\lt) \} \cup \{(\lap,\la) \}, \Hc, \A )\\
    \end{array}
\end{displaymath}
are compatible, and only the pair $(\lap,\la)$ is added to \I. This pair is already
known to be either in \IE \ or in \IB.
Case  1 and case 2 of Figure~\ref{cfa_models_in} are analogous.

\noindent Thus, it follows that all the triplets of Figure~\ref{oc_models_in} are elements of \gammaB (\IB,\IE,\Hc). This concludes the proof that $\gammaB\IHreloc in^{\ell^{t}} n.P$.

\item Case {\it in} (Figure~\ref{oc_models_in} and Figure~\ref{cfa_models_in}). Proof of ``$\Rightarrow$''. Let us now show that
\begin{displaymath}
\gammaB\IHreloc in^{\ell^{t}} n.P \Rightarrow \IHrelb in^{\ell^{t}} n.P
\end{displaymath}
\noindent From the specification of the occurrence counting analysis (see Figure~\ref{oc_models_in}), it follows that \linebreak \gammaB \IHreloc P. By induction hypothesis, we have \IHrelb P.

\noindent Then, consider $\la, \lap, \lapp $ such that
\begin{displaymath}
\begin{array}{c}
\infrel{\la}{\lt}{\eta^{B}(\I^{'}) \cup \  \eta^{E}(\I^{'})} \og
\infrel{\lapp}{\la}{\eta^{B}(\I^{'}) \cup \ \eta^{E}(\I^{'})} \og \\
\infrel{\lapp}{\lap}{\eta^{B}(\I^{'}) \cup \ \eta^{E}(\I^{'})} \og
\infrel{\lap}{n}{\Hc}
\end{array}
\end{displaymath}
We know from~\cite{nielsonAbstr} (Section 4.2) that
\begin{displaymath}
(\I,\Hc,[\{\la |\ (\la,n)\in \Hc \}\mapsto \omega]) \in \gammaB
(\IB,\IE,\Hc)
\end{displaymath}
therefore
\begin{displaymath}
(\I \cup \ \{ (\lap,\la) \}, \Hc,[\{\la |\ (\la,n)\in \Hc
\}\mapsto \omega]) \in \gammaB (\IB,\IE,\Hc)
\end{displaymath}
Given the definition of \gammaB it follows that $(\lap,\la) \in
\IE \cup \IB$, and this concludes the proof that $\IHrelb
in^{\ell^{t}} n.P$.
\end{itemize}

\vspace{0,3cm} \noindent The proof for \textit{out-}capabilities
is analogous. Then, to conclude the whole proof we have to consider the {\it open} capability. In this case, we need to consider the multiplicity of the ambients dealt
with. In particular,

\begin{figure}[h]
\begin{footnotesize}
\centering

\fbox{\parbox{6in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lcl}
\cas{open} & \mathcal{C} \models^{\annoOC}{\sopencap{n}{P}}&
\hviss & \mathcal{C} \models^{\annoOC} P \og \forall (\I, \Hc,
\A)\in \mathcal{C} \
: \forall \la, \lap :\\
& \multicolumn{3}{l} {\left(\infrel{\la}{\lt}{\I} \og
\infrel{\la}{\lap}{\I} \og \infrel{\lap}{n}{\Hc}\right)
\Rightarrow }
\\
 &  \multicolumn{3}{l}{
 % \capindent
    \left(
    \begin{array}{@{}l}
            \textrm{case} \A(\lap) \textrm{of} \\
            1:\forall X \subseteq \{ (\la,\lt)\}: \\
            \quad (\I \setminus ( \{(\lap,\ell)\in \I |\  \ell \in \textbf{Lab}\} \cup \{(\la,\lap)\} \cup X) \cup \{(\la,\ell)|\ (\lap,\ell) \in \I\}, \\
            \quad \Hc \setminus \{(\lap,m)|\ m \in \textbf{SNam}\}, \A \setminus \{\lap\}) \in \textit{C} \\
            \omega: \forall Z \subseteq \{ (\lap,\ell) \in \I |\ \ell \in \Labarg{} \} : \forall X \subseteq \{(\la,\lt)\} : \forall \textsf{c} \in \{ 1,\omega \}:\\
            \quad \forall Y \subseteq \textrm{s.t.}\  Y \supseteq Z \cap \{(\lap,\ell)\in \I |\ \A(\ell)=1 \}: \\
            \quad \textrm{case \textsf{c} of} \\
            \quad \omega: \forall V \subseteq \{(\lap,\lfloor n \rfloor)\} \ \textrm{s.t.} \  \exists m \in \textbf{SNam}: (\lap,m) \in \Hc \setminus V:\\
            \quad \  \forall W \subseteq \{(\la,\lap)\}\  \textrm{s.t.} \ \exists \ell: (\ell,\lap) \in ((\I \setminus(Y \cup X)) \cup \{(\la,\ell)|\ (\lap,\ell) \in Z
            \})\setminus W: \\
            \quad \ (((\I \setminus (Y \cup X)) \cup \{(\la,\ell)|\ (\lap,\ell) \in Z \}) \setminus W, \Hc \setminus V, \A[\lap \mapsto \textsf{c}] ) \in C\\
            \quad 1: \forall V \subseteq \{(\lap,m) |\ (\lap,m) \in \Hc \}\\
            \quad \ \forall W \subseteq \{(\ell,\lap) |\ (\ell,\lap) \in ((\I \setminus (Y \cup X)) \cup \{(\la,\ell)|\ (\lap,\ell) \in Z
            \})\}: \\
            \quad \ (((\I \setminus (Y \cup X)) \cup \{(\la,\ell)|\ (\lap,\ell) \in
            Z\}) \setminus W, \Hc \setminus V, \A[\lap \mapsto
            \textsf{c}]) \in C
    \end{array} \right)} \\
\\[\specskip]
\end{array}
\end{displaymath}
}} \caption{Specification of the analysis with occurrence counting
(\textit{open-}capabilities)} \label{oc_models_open}
\end{footnotesize}
\end{figure}

\begin{figure}[h]
\centering

\fbox{\parbox{6in}{
\begin{displaymath}
\renewcommand{\arraystretch}{1.2}
\begin{array}{l@{\hspace{0.4cm}}lcl}
\cas{open} & \IHrelb{\sopencap{n}{P}}& \hviss & \IHrelb{P} \og \\
 &  \multicolumn{3}{l}{
    %\capindent
    \begin{array}[t]{@{}l}
        \foralled{\la,\lap\in\Laba} \\
    \mbox{case 1:\;}(\infrel{\la}{\lt}{\IE} \og \infrel{\la}{\lap}{\IE} \og \infrel{\lap}{n}{\Hc}) \implies \\
        \quad \mbox{if (\;} \lap \in \Laba_B ) \mbox{\;then} \delmgd{\set{\comp{(\la,\lapp)}{\infrel{\lap}{\lapp}{\IB}}}}{\IE} \og \\
    \quad \quad \delmgd{\set{\comp{(\ell,\ell')}{\infrel{\ell}{\ell'}{\IB} \og (\lap,\ell^{''}) \in \IB \og path_{B}(\ell^{''},\ell) }}}{\IE}\\
    \quad \mbox{else\;} \delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{\IE}}}}{\IE} \\
\mbox{case 2\;}(\infrel{\la}{\lt}{\IB} \og \infrel{\la}{\lap}{\IB} \og \infrel{\lap}{n}{\Hc}) \\
    \quad \implies \delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{\IB}}}}{\IB} \\
    \end{array}}\\
\end{array}
\end{displaymath}
}} \caption{Specification of the refined Control Flow Analysis
(\textit{open-}capabilities)} \label{cfa_models_open}
\end{figure}

\begin{itemize}
\item Case {\it open} (Figure~\ref{oc_models_open} and Figure~\ref{cfa_models_open}). Proof of ``$\Leftarrow$''. Let us prove that
\begin{displaymath}
\IHrelb open^{\ell^{t}} n.P \Rightarrow \gammaB\IHreloc open^{\ell^{t}} n.P
\end{displaymath}
\noindent From the specification of the analysis depicted in Figure~\ref{cfa_models_open}, it follows that \IHrelb P. So, by induction hypothesis we have $\gammaB \IHreloc P $.

\noindent Then, consider $(\I^{'},\Hc^{'},\A^{'})\in
\gammaB(\IB,\IE,\Hc)$ and $\la, \lap $ such that
\begin{displaymath}
\infrel{\la}{\lt}{\I^{'}} \og \infrel{\la}{\lap}{\I^{'}} \og
 \infrel{\lap}{n}{\Hc^{'}}
\end{displaymath}
\noindent By definition of $\gammaB$, if
$(\I^{'},\Hc^{'},\A^{'})\in \gammaB(\IB,\IE,\Hc)$, then
$(\I^{'},\Hc^{'},\A^{'})$ is compatible and \linebreak
$(\eta^{B}(\I^{'}),\eta^{E}(\I^{'}),\Hc^{'})\sqsubseteq
(\IB,\IE,\Hc)$. It follows that
\begin{displaymath}
\begin{array}{c}
\infrel{\la}{\lt}{\eta^{B}(\I^{'}) \cup \  \eta^{E}(\I^{'})} \og
\infrel{\la}{\lap}{\eta^{B}(\I^{'}) \cup \ \eta^{E}(\I^{'})} \og
\infrel{\lap}{n}{\Hc}.
\end{array}
\end{displaymath}
We have to consider the two cases depicted in Figure~\ref{cfa_models_open}. The most interesting one is case 1, when a boundary is dissolved. In this case, it holds that either $\delmgd{\set{\comp{(\la,\lapp)}{\infrel{\lap}{\lapp}{\IB}}}}{\eta^{E}(\I^{'})}$ and $\delmgd{\set{\comp{(\ell,\ell')}{\infrel{\ell}{\ell'}{\IB} \og (\lap,\ell^{''}) \in \IB \og path_{B}(\ell^{''},\ell) }}}{\eta^{E}(\I^{'})}$ or \linebreak $\delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{\IE}}}}{\eta^{E}(\I^{'})} $.

\noindent By looking at the occurrence counting analysis, we observe that all the triplets of Figure~\ref{oc_models_open} are
compatible and at most add the pairs
\begin{displaymath}
\delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{Z}}}}{\delmgd{\set{\comp{(\la,\ell)}{\infrel{\lap}{\ell}{\I^{'}}}}}{\{(\la,\ell)|\
(\lap,\ell) \in \IE \cup \IB \}}}
\end{displaymath}
which are already known to be either in \IE \ or in \IB. Case 2 of Figure~\ref{cfa_models_open} is analogous.

\noindent Thus, it follows that all the triplets above are elements of \gammaB
(\IB,\IE,\Hc). This concludes the proof that $\gammaB\IHreloc
open^{\ell^{t}} n.P$.

\item Case {\it open} (Figure~\ref{oc_models_open} and Figure~\ref{cfa_models_open}). Proof of ``$\Rightarrow$''. Finally, let us show now that
\begin{displaymath}
\gammaB\IHreloc open^{\ell^{t}} n.P \Rightarrow \IHrelb open^{\ell^{t}} n.P
\end{displaymath}
\noindent From the specification of the occurrence counting analysis (Figure~\ref{oc_models_open}), we get that \linebreak \gammaB \IHreloc P. By induction hypothesis, \IHrelb P.

\noindent Then, consider $(\I^{'},\Hc^{'},\A^{'})\in
\gammaB(\IB,\IE,\Hc)$ and $\la, \lap $ such that
\begin{displaymath}
\infrel{\la}{\lt}{\I} \og \infrel{\la}{\lap}{\I} \og
\infrel{\lap}{n}{\Hc}
\end{displaymath}

\noindent We know from~\cite{nielsonAbstr} that
\begin{displaymath}
(\I,\Hc,[\{\la |\ (\la,n)\in \Hc \}\mapsto \omega]) \in \gammaB
(\IB,\IE,\Hc).
\end{displaymath}
For this choice of element in $\gammaB(\IB,\IE,\Hc)$, in the specification of the analysis depicted in Figure~\ref{oc_models_open} we take:
\begin{displaymath}
\begin{array}{lll}
Z &= &\{(\lap \in \I )| \ \ell \in \textbf{Lab})  \}\\
Y &= & \emptyset \\
X &=& \emptyset \\
c &=& \omega \\
V &=& \emptyset \\
W &=& \emptyset \\
\end{array}
\end{displaymath}

\noindent Then, it follows that
\begin{displaymath}
(((\I \ \backslash \ (Y \cup X)) \cup \{(\la,\ell)| \ (\lap,\ell)
\in Z\}) \ \backslash \ W, \Hc \ \backslash \ V, \A[\lap \mapsto
\textsc{c}]) \in \gammaB(\IB,\IE,\Hc).
\end{displaymath}

\noindent Given the definition of \gammaB, it follows that
\begin{displaymath}
\{(\la,\ell)| \ (\lap,\ell) \in \I \} = \{(\la,\ell)| \
(\lap,\ell) \in Z \} \ \subseteq \I
\end{displaymath}
and this concludes the proof that $\IHrelb open^{\ell^{t}} n.P$.
\end{itemize}

\hfill{} $\Box$

\begin{proposition}[Theorem~\ref{theoCorr}]
Let $P$ and $Q$ be two processes such that
 $ \ \repab{env}{P} \sqsubseteq (\IB,\IE,\Hc) \  \  \wedge  \ \
 \IHrelb{P}  \ \wedge \ P
\rightarrow Q \ \ $ then  $\ \ \repab{env}{Q} \sqsubseteq
(\IB,\IE,\Hc) \ \  \wedge \ \
 \IHrelb{Q}$.
\end{proposition}
\begin{proof}
It follows immediately from Proposition~\ref{global} and Proposition~\ref{global2}.\hfill{} $\Box$
\end{proof}

\end{proof}

\section{Related Works and Conclusions}\label{conclusions}

The main novelty of the approach presented in this paper is that
we model multilevel information flow within a ``pure'' mobile
ambient setting based on the seminal ideas presented
in~\cite{BDNN98pi,HJNN99ai} on ambient nesting analysis. We do not
consider either channels or recently proposed restrictions of
Mobile Ambients designed for security issues. There have been
hardly any research efforts in this general direction. In fact,
the most interesting recent contributions in the area mainly
focused on either extending the ambient calculus thus enhancing
its expressive power, or on building suitable type systems to
verify security properties.


Among the type systems approaches, it is worth to mention~\cite{cardelli.ghelli.ea:ambient-groups}, where the authors introduce a new type system for tracking the behaviour of mobile computations. They introduce the concept of name group, which represents a collection of ambient names. Using groups, the type system can impose to an ambient behavioral constraints on the set of ambients it may cross and the set of ambients it may open. It has the effect of statically preventing certain communications through a mandatory access control policy, and can block accidental or malicious leakage of secrets.

Dezani and Salvo~\cite{Dezani-Salvo:00} extend the work of
Cardelli et al. just mentioned, with a type system that also
expresses security levels associated with ambients and provide
further control over ambient movement and opening.

Among the language extensions, valuable proposals are described
in~\cite{degano.levi.ea:safe-ambients,BugCasCra:TACS:01,BugCas:POPL:01,BugCas:CompLang:02,levi00controlling}. {\it Safe Ambients} is a
modification of Mobile Ambients, where a movement or an ambient
dissolution can take place only when the affected ambient agrees,
offering the corresponding coaction. {\it Boxed
Ambients}~\cite{BugCasCra:TACS:01} is another variant of the
Ambient calculus with a completely different model of
communication, which results from dropping the \textit{open}
capability. In their paper, Bugliesi et al. define also a type
system that provides an effective mechanism for resource
protection and access control.

Few efforts have been put on the analysis approach to security
issues in Mobile Ambients. In~\cite{levi.bodei:sec-analysis},
Degano et al. present a control flow analysis that mainly focuses on
access control. The analysis relies on the use of coactions
as a filter to control access to resources.

\vspace{0,5cm}

We are currently extending our analysis to deal with coactions in
order to evaluate benefits and disadvantages of the different
formalisms of ``information leakage'' and of the corresponding
analyses, and we are currently investigating how to extend our
analysis to communication channels as well. Finally, the way we propose to express a multilevel information
flow policy through the notion of boundary ambient, in our
opinion, may also lead to interesting applications to model
cryptographic protocols.

\newpage

\appendix
\section{Operational Semantics of Mobile Ambients}
\label{MAsemantics} For the sake of completeness, we report the
operational semantics of Mobile Ambients as described
in~\cite{Cardelli:97:MA}.

\vspace{0.3cm} \noindent {\bf Structural Congruence}
\[
\begin{array}{ll}
P \equiv P & P\;|\;Q \equiv Q\;|\;P \\
P \equiv Q \Rightarrow Q \equiv P & \comp{(\comp{P}{Q})}{R} \equiv \comp{P}{(\comp{Q}{R})}\\
P \equiv Q, Q \equiv R \Rightarrow  P \equiv R & \repl{P} \equiv \comp{P}{\repl{P}}\\
P \equiv Q \Rightarrow  \rest{n}{P} \equiv \rest{n}{Q} & \rest{n}{\rest{m}{P}} \equiv \rest{m}{\rest{n}{P}}\\
P \equiv Q \Rightarrow  \comp{P}{R} \equiv \comp{Q}{R} \hspace{4,4cm} & \rest{n}{\comp{P}{Q}} \equiv \comp{P}{\rest{n}{Q}} \mbox{\;if\;} n \not\in  fn(P)  \\
P \equiv Q \Rightarrow  \repl{P} \equiv \repl{Q} & \rest{n}{\boldambient{m}{\la}{P}} \equiv \boldambient{m}{\la}{\rest{n}{P}} \mbox{\;if\;} n\neq m\\
P \equiv Q \Rightarrow  \boldambient{n}{\ell}{P} \equiv \boldambient{n}{\ell}{Q} &  \comp{P}{0} \equiv P \\
P \equiv Q \Rightarrow  M.P \equiv M.Q & \rest{n}{0} \equiv 0 \\
& \repl{0} \equiv 0
\end{array}
\]
%\samb{n}{\la}{P}

\vspace{0.3cm} \noindent {\bf Reduction Rules}
%\begin{itemize}

\[
\begin{array}{l}
%\item [] $
\comp{\boldambient{n}{\la}{\act{\sina{c}{m}}\comp{P}{Q}}}{\boldambient{m}{\ell}{R}} \rightarrow \boldambient{m}{\ell}{\comp{\boldambient{n}{\la}{\comp{P}{Q}}}{R}} \\
%$\item [] $
\boldambient{m}{\la}{\comp{\boldambient{n}{\ell}{\comp{\act{\souta{c}{m}}P}{Q}}}{R}} \rightarrow \comp{\boldambient{n}{\ell}{\comp{P}{Q}}}{\boldambient{m}{\la}{R}} \\
%$\item [] $
\comp{\act{\sopena{c}{n}}P}{\boldambient{n}{\la}{Q}} \rightarrow
\comp{P}{Q} \\
%$\item [] $
P^{'} \equiv P, P \rightarrow Q, Q \equiv Q^{'} \Rightarrow P^{'} \rightarrow Q^{'} \\
%$\item [] $
P \rightarrow Q \Rightarrow \rest{n}{P} \rightarrow \rest{n}{Q} \\
%$\item [] $
P \rightarrow Q \Rightarrow \boldambient{n}{\ell}{P} \rightarrow \boldambient{n}{\ell}{Q} \\
%$\item [] $
P \rightarrow Q \Rightarrow  \comp{P}{R} \rightarrow \comp{Q}{R}
\end{array}
\]
%\end{itemize}

%\small

\newpage

\bibliography{bibliography}
\bibliographystyle{unsrt}
%\bibliographystyle{plain}

\end{document}

\begin{thebibliography}{10}

\bibitem{BDNN98pi}
Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne~Riis Nielson.
\newblock {C}ontrol {F}low {A}nalysis for the $\pi$-calculus.
\newblock In {\em Proc.~CONCUR'98}, number 1466 in Lecture Notes in Computer
  Science, pages 84--98. Springer-Verlag, 1998.

\bibitem{BDNN99pi}
Chiara Bodei, Pierpaolo Degano, Flemming Nielson, and Hanne~Riis Nielson.
\newblock {S}tatic {A}nalysis of {P}rocesses for {N}o {R}ead-{U}p and {N}o
  {W}rite-{D}own.
\newblock In {\em Proc.~FoSSaCS'99}, number 1578 in Lecture Notes in Computer
  Science, pages 120--134. Springer-Verlag, 1999.

\bibitem{fmoods02}
Chiara Braghin, Agostino Cortesi, and Riccardo Focardi.
\newblock {C}ontrol {F}low {A}nalysis of {M}obile {A}mbients with {S}ecurity
  {B}oundaries.
\newblock In Bart Jacobs and Arend Rensink, editors, {\em Proc. of Fifth IFIP
  International Conference on Formal Methods for Open Object-Based Distributed
  Systems ({FMOODS'02})}, pages 197--212. {K}luwer {A}cademic {P}ublisher,
  2002.

\bibitem{BugCas:CompLang:02}
Michele Bugliesi and Giuseppe Castagna.
\newblock {B}ehavioural {T}yping of {S}afe {A}mbients.
\newblock {\em Journal of Computer Security}, this issue.

\bibitem{BugCas:POPL:01}
Michele Bugliesi and Giuseppe Castagna.
\newblock {S}ecure {S}afe {A}mbients.
\newblock In {\em Proc. 28th ACM Symposium on Principles of Programming
  Languages {(POPL'01)}}, pages 222--235. ACM Press, 2001.

\bibitem{BugCasCra:TACS:01}
Michele Bugliesi, Giuseppe Castagna, and Silvia Crafa.
\newblock {B}oxed {A}mbients.
\newblock In {\em Proc. of the 4th Int. Conference on Theoretical Aspects of
  Computer Science ({TACS'01})}, volume 2215 of {\em LNCS}, pages 38--63.
  Springer-Verlag, 2001.

\bibitem{cardelli.ghelli.ea:ambient-groups}
Luca Cardelli, Giorgio Ghelli, and Andrew~D. Gordon.
\newblock {A}mbient {G}roups and {M}obility {T}ypes.
\newblock In J.~{van Leeuwen}, O.~Watanabe, M.~Hagiya, P.~D. Mosses, and
  T.~Ito, editors, {\em Theoretical Computer Science: Exploring New Frontiers
  of Theoretical Informatics, Proceedings of the International {IFIP}
  Conference {TCS} 2000 (Sendai, Japan)}, volume 1872 of {\em LNCS}, pages
  333--347. IFIP, Springer, August 2000.

\bibitem{Cardelli:97:MA}
Luca Cardelli and Andrew~D. Gordon.
\newblock {M}obile {A}mbients.
\newblock In M.~Nivat, editor, {\em Proceedings of Foundations of Software
  Science and Computation Structures (FoSSaCS)}, volume 1378 of {\em LNCS},
  pages 140--155. Springer-Verlag, Berlin, Germany, March 1998.

\bibitem{concoord01}
Agostino Cortesi and Riccardo Focardi.
\newblock {I}nformation {F}low {S}ecurity in {M}obile {A}mbients.
\newblock In {\em Proc. of International Workshop on Concurrency and
  Coordination {(ConCoord'01)}}, volume~54 of {\em Electronic Notes on
  Theoretical Computer Science, {ENTCS}}. Elsevier, July~6--8~ 2001.

\bibitem{degano.levi.ea:safe-ambients}
Pierpaolo Degano, Francesca Levi, and Chiara Bodei.
\newblock {S}afe {A}mbients: {C}ontrol {F}low {A}nalysis and {S}ecurity.
\newblock In Jifeng He and Masahiko Sato, editors, {\em Proc. of Advances in
  Computing Science - {ASIAN}'00 (6th Asian Computing Science Conference,
  Penang, Malaysia)}, volume 1961 of {\em LNCS}, pages 199--214. Springer,
  December 2000.

\bibitem{Dezani-Salvo:00}
Mariangiola Dezani-Ciancaglini and I.Salvo.
\newblock {S}ecurity {T}ypes for {M}obile {S}afe {A}mbients.
\newblock In Jifeng He and Masahiko Sato, editors, {\em Proc. of Advances in
  Computing Science - {ASIAN}'00 (6th Asian Computing Science Conference,
  Penang, Malaysia)}, volume 1961 of {\em LNCS}, pages 215--236. Springer,
  December 2000.

\bibitem{FG95}
Riccardo Focardi and Roberto Gorrieri.
\newblock {A} {C}lassification of {S}ecurity {P}roperties for {P}rocess
  {A}lgebras.
\newblock {\em Journal of Computer Security}, 3(1):5--33, 1995.

\bibitem{FG97}
Riccardo Focardi and Roberto Gorrieri.
\newblock {T}he {C}ompositional {S}ecurity {C}hecker: {A} {T}ool for the
  {V}erification of {I}nformation {F}low {S}ecurity {P}roperties.
\newblock {\em IEEE Transactions on Software Engineering}, 23(9):550--571, sep
  1997.

\bibitem{focardi00information}
Riccardo Focardi, Roberto Gorrieri, and Fabio Martinelli.
\newblock {I}nformation {F}low {A}nalysis in a {D}iscrete-{T}ime {P}rocess
  {A}lgebra.
\newblock In {\em Proc. of The 13th Computer Security Foundations Workshop
  ({CSFW})}, pages 170--184. IEEE Computer Society Press, 2000.

\bibitem{HJNN99ai}
R.~R. Hansen, J.~G. Jensen, F.~Nielson, and H.~Riis Nielson.
\newblock {A}bstract {I}nterpretation of {M}obile {A}mbients.
\newblock In A.Cortesi and G.File', editors, {\em Proc. of Static Analysis
  Symposium ({SAS}'99)}, number 1694 in Lecture Notes in Computer Science,
  pages 134--148. Springer-Verlag, 1999.

\bibitem{hennessy00resource}
Matthew Hennessy and James Riely.
\newblock {I}nformation {F}low vs. {R}esource {A}ccess in the {A}synchronous
  {P}i-{C}alculus.
\newblock In U.~Montanari, J.~Rolim, and E.~Welzl, editors, {\em Proc. of the
  International Colloquium on Automata, Languages and Programming}, volume 1853
  of {\em Lecture Notes in Computer Science}, pages 415--427, Geneva, August
  2000. Springer-Verlag.

\bibitem{levi.bodei:sec-analysis}
Francesca Levi and Chiara Bodei.
\newblock {S}ecurity {A}nalysis for {M}obile {A}mbients.
\newblock In {\em Electronic Proc. of IFIP WG 1.7 Workshop on Issues on the
  Theory of Security (WITS'00), Geneve}, 2000.

\bibitem{levi00controlling}
Francesca Levi and Davide Sangiorgi.
\newblock {C}ontrolling {I}nterference in {A}mbients.
\newblock In {\em Proc. 28th ACM Symposium on Principles of Programming
  Languages {(POPL'01)}}, pages 352--364, 2000.

\bibitem{nielsonAbstr}
F.~Nielson, R.~R. Hansen, and H.~Riis Nielson.
\newblock {A}bstract {I}nterpretation of {M}obile {A}mbients.
\newblock {\em Science of Computer Programming}, Special Issue on Static
  Analysis edited by A.Cortesi and G.File', to appear.

\bibitem{smith98secure}
Geoffrey Smith and Dennis Volpano.
\newblock {S}ecure {I}nformation {F}low in a {M}ulti-{T}hreaded {I}mperative
  {L}anguage.
\newblock In {\em Conference Record of {POPL} 98: The 25TH {ACM}
  {SIGPLAN}-{SIGACT} Symposium on Principles of Programming Languages, San
  Diego, California}, pages 355--364, New York, NY, 1998.

\end{thebibliography}

\end{document}
