Technische Universität Wien, Vienna, Austria and http://www.eziobartocci.com
ezio.bartocci@tuwien.ac.athttps://orcid.org/0000-0002-8004-6601This research
was supported by the Austrian FWF project W1255-N23Imagination Technologies,
Kings Langley, UK
thomas.ferrere@imgtec.comhttps://orcid.org/0000-0001-5199-3143IST Austria,
Klosterneuburg, Austria and http://pub.ist.ac.at/~tah/
tah@ist.ac.athttps://orcid.org/0000-0002-2985-7724AIT Austrian Institute of
Technology, Vienna, Austria
dejan.nickovic@ait.ac.athttps://orcid.org/0000-0001-5468-0396Technische
Universität Wien, Vienna, Austria<EMAIL_ADDRESS>research was
supported by the Austrian FWF project W1255-N23 E. Bartocci and T. Ferrère and
T. A. Henzinger and D. Nickovic and A. Oliveira da Costa <ccs2012> <concept>
<concept_id>10002978.10002986.10002988</concept_id> <concept_desc>Security and
privacy Security requirements</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10003766.10003767</concept_id> <concept_desc>Theory of
computation Formalisms</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10010124.10010138.10010141</concept_id>
<concept_desc>Theory of computation Pre- and post-conditions</concept_desc>
<concept_significance>500</concept_significance> </concept> <concept>
<concept_id>10003752.10010124.10010138.10010140</concept_id>
<concept_desc>Theory of computation Program specifications</concept_desc>
<concept_significance>500</concept_significance> </concept> </ccs2012>
[500]Security and privacy Security requirements [500]Theory of computation
Formalisms [500]Theory of computation Pre- and post-conditions 2 2020

# Information-Flow Interfaces

Ezio Bartocci  Thomas Ferrère  Thomas A. Henzinger  Dejan Nickovic  Ana
Oliveira da Costa

###### Abstract

Contract-based design is a promising methodology for taming the complexity of
developing sophisticated systems. A formal contract distinguishes between
_assumptions_ , which are constraints that the designer of a component puts on
the environments in which the component can be used safely, and _guarantees_ ,
which are promises that the designer asks from the team that implements the
component. A theory of formal contracts can be formalized as an _interface
theory_ , which supports the composition and refinement of both assumptions
and guarantees.

Although there is a rich landscape of contract-based design methods that
address functional and extra-functional properties, we present the first
interface theory that is designed for ensuring system-wide security
properties, thus paving the way for a science of safety and security co-
engineering. Our framework provides a refinement relation and a composition
operation that support both incremental design and independent
implementability. We develop our theory for both stateless and stateful
interfaces. We illustrate the applicability of our framework with an example
inspired from the automotive domain. Finally, we provide three plausible trace
semantics to stateful information-flow interfaces and we show that only two
correspond to temporal logics for specifying hyperproperties, while the third
defines a new class of hyperproperties that lies between the other two
classes.

###### keywords:

Contract-based design, Interface Theory, Hyperproperties, Information-flow

##  1 Introduction

The rise of pervasive information and communication technologies seen in
cyber-physical systems, internet of things, and blockchain services has been
accompanied by a tremendous growth in the size and complexity of systems [30].
Subtle dependencies involving multiple architectural layers and unforeseen
environmental interactions can expose these systems to cyber-attacks. This
problem is further exacerbated by the heterogeneous nature of their
constituent components, which are often developed independently by different
teams or providers. In such a scenario, defining and enforcing security
requirements across components at an early stage of the design process becomes
a necessity. This engineering approach is called _security-by-design_.
Although in recent years there has been impressive progress in the
verification of security properties for individual system components, the
science of compositional security design [25] is still in its infancy.

Security policies are usually enforced by restricting the flow of information
in a system [32]. _Information-flow policies_ define which information a user
or a software/hardware component is allowed to observe by interacting with
another component. They cover both confidentiality and integrity constraints.
Confidentiality limits the availability of information, for example, by
forbidding confidential data to leak to public variables. Integrity, dually,
concerns the modification of information, by prohibiting untrusted agents to
interfere with trusted data. The goal of information-flow control is to ensure
that a system as a whole satisfies the desired policies. This task is
challenging because it needs to account also for implicit flows and side-
channels from which an attacker can infer information by combining multiple
observations. From a formal-language perspective, such security
vulnerabilities are not characterized by properties of a single system
execution, but rather by properties of sets of execution traces, which are
called _hyperproperties_ [8]. Much recent work on formal methods for security
has focused on model checking various classes of hyperproperties [7, 9, 17].

In this paper, we present a _contract-based design_ [4] approach for
information-flow properties. Contract-based design provides a formal framework
for building complex systems from individual components, mixing both top-down
and bottom-up steps. A top-down step decomposes and refines system-wide
requirements; a bottom-up step assembles a system by combining available
components. A formal contract distinguishes between _assumptions_ , which are
constraints that the designer of a component puts on the environments in which
the component can be used safely, and _guarantees_ , which are promises that
the designer asks from the team that implements the component. A theory of
formal contracts can be formalized as an _interface theory_ , which supports
the composition and refinement of both assumptions and guarantees [13, 14,
33]. While there is a rich landscape of interface theories for functional and
extra-functional properties [6, 15, 11], we present the first interface theory
that is designed for ensuring system-wide security properties, thus paving the
way for a science of safety and security co-engineering.

Our theory is based on information-flow assumptions as well as information-
flow guarantees. As an interface theory, our theory supports both incremental
design and independent implementability [14]. Incremental design allows the
composition of different system parts, each coming with their own assumptions
and guarantees, without requiring additional knowledge of the overall design
context. Independent implementability enables the separate refinement of
different system parts by different teams that, without gaining additional
information about each other’s design choices, can still be certain that their
designs, once combined, preserve the specified system-wide requirements. While
in previous interface theories, the environment of a component is held
responsible for meeting assumptions, and the implementation of the component
for the guarantees, there are cases of information-flow violations for which
blame cannot be assigned uniquely to the implementation or the environment. In
information-flow interfaces we therefore introduce, besides assumptions and
guarantees, a new, third type of constraint—called _properties_ —whose
enforcement is the shared responsibility of the implementation and the
environment.

We develop our framework for both stateless and stateful interfaces. Stateless
information-flow interfaces are built from primitive information-flow
constraints—assumptions, guarantees, and properties—of the form “the value of
a variable $y$ is always independent of the value of another variable $x$.”
Stateful information-flow interfaces add a temporal dimension, e.g., “the
value of $y$ is independent of $x$ _until_ the value of $z$ is independent of
$x$.” The temporal dimension is introduced through a natural notion of state
and state transition for interfaces, not through logical operators. Besides
proving that our calculus of information-flow interfaces satisfies the
principles of incremental design and independent implementability, we show
that among three plausible ways of giving a trace semantics to stateful
information-flow interfaces, only two correspond to temporal logics for
specifying hyperproperties, namely HyperLTL [7] and linear time epistemic
logic [16, 5]. The third, and arguably most natural, trace interpretation of
stateful information-flow interfaces defines a new class of hyperproperties
that lies between the other two classes.

##  2 Motivating Example

We illustrate the main concepts of our information flow interface theory using
an electronic vehicle immobilizer (EVI) example. An EVI is a security device
handling a transponder key and used by car manufacturers to prevent hot wiring
a car, thus prevent car theft. If the transponder authentication fails, then
the engine control unit blocks the car’s ignition. The communication between
the immobilizer and other components in the vehicle takes place through the
controller area network (CAN), a serial communication technology that is
commonly used in automobile architectures to connect electronic control units
(ECUs). This communication protocol does not include native support of
security-related features. Thus, it is the responsibility of the components
that use the bus to enforce confidentiality and integrity policies.

\begin{picture}(5724.0,1902.0)(514.0,-3151.0)\end{picture}

Figure 1: High-level view on immobilizer feature requirements.

In this example, we model the communication of an automotive engine control
with an immobilizer through the CAN. The authentication follows a challenge-
response protocol. The communication session starts with the engine’s ECU
sending a freshly generated random number encrypted with a secret key known to
both of the devices. The immobilizer replies to this challenge with an
appropriate response encrypted with the same key. Figure 1 depicts a high-
level overview of this model, which must enforce the following security
property: the secret key shall never leak to the environment via the CAN bus.
In the remainder of this section, we illustrate how we can use an interface
theory for information flow policies to implement the above specification in
(1) a top-down, and (2) a bottom-up design fashion.

Top-down design: We first demonstrate _stepwise refinement of a global
specification_ : different engineering teams can independently implement
subsystems, without violating the overall specification. We start by
illustrating this process for the stateless case in Fig. 2 (a). We start with
the interface $F$ that represents the overall (closed) system when it is in
operation mode. It specifies the global property that information from key is
not allowed to flow to can or deb. We assume that the secret key and the CAN
bus are standard components provided by third-party suppliers. Our goal is to
design the remaining sub-system consisting of the immobilizer and the ECU.
This gives us a natural decomposition of $F$ into three interfaces: (1)
$F_{\emph{key}}$ specifying the secret key, (2) $F_{\emph{can}}$ specifying
the CAN bus, and (3) $F_{\emph{team}}$ specifying the sub-system that we want
to further develop. We note that the property from $F$ becomes an assumption
in $F_{\emph{team}}$.

The proposed decomposition does not work because $F_{\emph{team}}$ _is not
compatible_ with $F_{\emph{can}}$—their composition would violate the
assumption from $F_{\emph{team}}$ by enabling the secret key to flow to the
CAN via the ECU or the immobilizer. These two interfaces can be made
compatible by strengthening guarantees of $F_{\emph{team}}$ and forbidding the
key to flow to the ECU and the immobilizer, resulting in the interface
$F_{\emph{team}}^{\prime}$. We further decompose $F_{\emph{team}}^{\prime}$
into two interfaces: (1) $F_{\emph{ecu}}$ specifying the ECU component, and
(2) $F_{\emph{imm}}$ specifying the immobilizer component. We note that the
composition of $F_{\emph{key}}$, $F_{\emph{can}}$, $F_{\emph{ecu}}$ and
$F_{\emph{imm}}$ refines the original system-level specification $F$. Finally,
we implement the four interfaces, derived from the overall specification, in
components $f_{\emph{key}}$, $f_{\emph{ecu}}$, $f_{\emph{imm}}$ and
$f_{\emph{can}}$. We note that the implementation of $f_{\emph{ecu}}$ and
$f_{\emph{imm}}$ could be done independently, by two separate teams. The ECU
(immobilizer) component guarantees that the secret key does not flow to its
output port and works correctly in any environment that forbids other means of
the secret key flowing to the CAN bus.

$F_{\emph{debug}}$$F_{\emph{init}}$$F$$F_{\emph{init}}$keyecukeycanimmkeycanecuimmcandeb$F_{\emph{key}}$$F_{\emph{can}}$$F_{\emph{ecu}}$$F_{\emph{imm}}$keyecukeycanimmkeycanecuimmcandeb$f_{\emph{key}}$$f_{\emph{ecu}}$$f_{\emph{imm}}$$f_{\emph{can}}$ecuimmcankeykeyecuimmcandeb$F_{\emph{key}}$$F_{\emph{can}}$ecuimmcandebkey$F$key$F_{\emph{team}}$$F_{\emph{imm}}$immkeycan$F_{\emph{key}}\otimes
F^{\prime}_{\emph{team}}\otimes
F_{\emph{can}}$candebecuimmkeyecuimmcankeyecuimmcandebkeykeyecukeycanimmkeycanecuimmcandebecuimmcankeykeyecuimmcandebkeyecuimmcandebecukeycanecuimmcandeb$F$$F_{\emph{key}}$$F_{\emph{team}}$$F_{\emph{can}}$$F_{\emph{key}}$$F^{\prime}_{\emph{team}}$$F_{\emph{key}}$$F_{\emph{can}}$$F_{\emph{ecu}}$$f_{\emph{key}}$$f_{\emph{ecu}}$$f_{\emph{imm}}$$f_{\emph{can}}$$F_{\emph{can}}$keyecudebcanimmkeyecucandebimm$\otimes$immkeyecu$F_{\emph{debug}}$$F_{\emph{init}}$$\mathbb{F}$:$F_{\emph{debug}}$$\mathbb{F}^{\prime}$:

Figure 2: EVI system: top-down design for (a) stateless and (b) stateful
interface, and (c) bottom-up design.

The system being designed can be in one of the following modes:
_initialization_ , _operational_ or _debug_. This is illustrated in the
stateful interface $\mathbb{F}$ in Fig. 2 (b). _Stateful interfaces_ are
finite state machines with every state being labeled with a stateless
interface. During initialization no information flows to CAN or the debug
port, this state ends when an immobilizer communicates with the car. Then, the
operation mode is decorated with the same $F$ interface from the stateless
example while the initialization is decorated with the interface
$F_{\emph{init}}$ in Fig. 2 (b). Debug mode specified in interface
$F_{\emph{debug}}$ allows all information to flow to the debug port.

In the stateful interface $\mathbb{F}^{\prime}$ we illustrate a refinement of
the initial specification in $\mathbb{F}$. We consider the case that the team
needs to accommodate two different architectures for the operational mode, for
example due to backward compatibility constraints. Then, in addition to the
decomposition of $F$ showcased in Fig. 2 (a), it is specified an alternative
in which the immobilizer is a third-party part. Note that $\otimes$ denotes
interface composition.

Bottom-up design: The bottom-up design, illustrated in Fig. 2 (c), is to a
large extent symmetric to the top-down approach. We start with the available
secret key, ECU, immobilizer and CAN components, specified by interfaces
$F_{\emph{key}}$, $F_{\emph{ecu}}$, $F_{\emph{imm}}$ and $F_{\emph{can}}$. The
main design step consists in composing a set of interfaces and _inferring new
global properties of the composition_. These properties are flows that cannot
be created given the current set of assumptions and guarantees. In the example
we infer two global properties, that the secret key can never flow either to
the CAN or to the debug port, because those ports can only be accessed through
ecu or imm ports to which key cannot flow.

In summary, our framework defines relations on both stateless and stateful
interfaces that allow to check if:

  * •

a given interface refines (or abstracts) the current specification;

  * •

two interfaces are compatible for composition, i.e. they respect each other
assumptions;

  * •

a specification is consistent, i.e. if the interface assumptions and
guarantees are sufficient to ensure its property;

  * •

information-flows in a component define an implementation of a given
interface.

Moreover, we define a composition operator which infers new global
specification from the local information-flow restrictions specified by the
interfaces being composed. We can then combine this operator with the
refinement relation to check if a system decomposition meets this system’s
specification.

##  3 Stateless Interfaces

In this section, we introduce a stateless interface and component algebra for
secure information flow. This algebra is based on properties of graphs linking
input and output variables, and enables us to reason about security
requirements in a hierarchical manner. We say that information flows from one
variable to another when the value of the first influences the second. We are
interested in the _structural_ properties of information flow within a system
and define relations abstracting flows, _flow relations_ , as being both
reflexive and transitively closed. Proofs are in the appendix A.

_Information-flow components_ abstract implementations of a system by a _flow
relation_. While information-flow interface specifies forbidden flows in an
open system by defining three kinds of constraints: assumptions, guarantees,
and properties. The _assumption_ characterizes flows that we assume are not
part of the environment while the _guarantee_ describes all flows the system
forbids and that are local to it. The _property_ qualifies the forbidden flows
at the interaction between the system and its environment. Hence, it
represents a requirement on the closed system that needs to be enforced by
guarantees on the open system and assumptions on its environment. The
distinction between the guarantee and the property is akin to the distinction
between open systems and closed systems. The property represents a requirement
on the closed system that is enforced by a guarantee on the open system and an
assumption on its environment.

######  Definition 3.1.

Let $X$ and $Y$ are disjoint sets of _input_ and _output_ variables,
respectively, with $Z=X\cup Y$ the set of all variables. A _flow relation_ in
$A\times B$ is reflexive in $A\cap B$ and transitive in $A\cup B$. A
_stateless information-flow component_ is a tuple $(X,Y,\mathcal{M})$, where
$\mathcal{M}\subseteq(X\cup Y)\times Y$ is a flow relation, called _flows_. A
_stateless information-flow interface_ is a tuple
$(X,Y,\mathcal{A},\mathcal{G},\mathcal{P})$, where: $\mathcal{A}\subseteq
Z\times X$ is a relation, called _assumption_ ; $\mathcal{G}\subseteq Z\times
Y$ is a relation, called _guarantee_ ; and $\mathcal{P}\subseteq Z\times Y$ is
a relation, called _property_.

In what follows, ${F=(X,Y,\mathcal{A},\mathcal{G},\mathcal{P})}$ and
$F^{\prime}=(X,Y,\mathcal{A}^{\prime},\mathcal{G}^{\prime},\mathcal{P}^{\prime})$
refer to arbitrary interfaces, and $f=(X,Y,\mathcal{M})$ and
$f_{\mathcal{E}}=(Y,X,\mathcal{E})$ to arbitrary components.

Given an interface we are interested in components that describe either one of
its implementations or one of the environments it admits. The implementation
of an interface shares its input/output signature, while the implementation of
its environment reverses it. We define _admissible environments_ and
_implementations_ of a given interface as components that do not include flows
forbidden by either the interface assumptions or guarantees, respectively.

######  Definition 3.2.

A component $f_{\mathcal{E}}$ of the form $f_{\mathcal{E}}=(Y,X,\mathcal{E})$
is called an _environment_ of $F$. An environment is _admissible for_ $F$,
denoted by $f_{\mathcal{E}}\models F$, iff
$\mathcal{E}\subseteq\overline{\mathcal{A}}$. A component $f$ of the form
$f=(X,Y,\mathcal{M})$ _implements_ the interface $F$, denoted by $f\models F$,
iff $\mathcal{M}\subseteq\overline{\mathcal{G}}$.

Note that the sets of implementations and admissible environments are mutually
exclusive, hence we can use the notation $\models$ for both.

An information-flow interface is _well-formed_ when it has at least one
implementation and one admissible environment. Therefore, all of its relations
must be irreflexive. A well-formed interface ensures, additionally, that its
property holds under any combination of its admissible environments and
implementations.

######  Example 3.3.

ecuimmkeycandeb$h$candebkeyecuimm$G$$g_{\mathcal{E}}$candebecuimmkey$g$ecuimmkeycandeb

Figure 3: Example of an ill-formed interface $G$ with an implementation $g$,
admissible environment $g_{\mathcal{E}}$, and a component $h$ that does not
implement it.

In Figure 3, interface $G$ requires as its only _property_ and _guarantee_
that no flow is created from the input variable key to the output variable
can. Additionally, the interface _assumes_ that the environment does not
create information flows from the input variable key to both imm and ecu. In
the same figure, we depict components $g$ and $g_{\mathcal{E}}$, which only
have flows allowed by $G$’s guarantee and assumptions, respectively. Hence,
$g$ _implements_ interface $G$, and $g_{\mathcal{E}}$ is an _admissible
environment_ of $G$.

A flow from key to can can be created by combining flows from both $g$ and
$g_{\mathcal{E}}$. In particular, the information can flow from key to deb,
then to ecu and finally to can. This violates the $G$ property. Its
assumptions and guarantees are too weak to ensure that the property is
satisfied under any combination of its admissible environments and
implementations. Thus, $G$ is _not_ a well-formed interface. For the same
reason, $G$ is _not_ a well-formed interface. The aforementioned path can be
used to show that $G$ does not satisfy the condition in Definition 3.4.

We note that the complement of a guarantee is not transitively closed and
hence does not define a flow relation (the same holds for the complement of an
assumption). This _prevents some interfaces to have a maximal implementation_
, i.e. a component that implements all allowed flows. Figure 3 shows an
interface $G$ and a component $h$ that does not implement it. Both flows from
$h$ (full arrows inside the box) are allowed to be implemented on their own,
but not together. Note that their transitive closure includes the only flow
forbidden by the interface—a flow from key to can. Thus, to evaluate possible
flow paths between implementations and environments we need to consider
alternated paths between the complement of the guarantees and the complement
of the assumptions.

To check that an interface is well-formed we need to verify that the flows
forbidden by its property can not be created by one of its implementations
interacting with one of its admissible environments. As explained above, we
cannot use the transitive closure of all flows allowed by assumptions,
_$\overline{\mathcal{A}}$_ , and guarantees, _$\overline{\mathcal{G}}$_ to
define all flows created by such interaction. We consider instead all flows
created by a path of arbitrary size that alternate between pairs of
$\overline{\mathcal{A}}$ and $\overline{\mathcal{G}}$.

######  Definition 3.4.

A _no-flow relation_ in $A\times B$ is irreflexive in $A\cap B$. An interface
$(X,Y,\mathcal{A},\mathcal{G},\mathcal{P})$ is _well-formed_ iff
$\mathcal{A}$, $\mathcal{G}$ and $\mathcal{P}$ are _no-flow relations_ ; and
$((\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{*}\circ\overline{\mathcal{G}})\cap\mathcal{P}=\emptyset$.

We show that our definitions capture the intended semantics for
implementations and environments. In particular, we prove that the interaction
between any of implementation and admissible environment of a given well-
formed interface cannot create flows forbidden by its property.

######  Proposition 3.5.

For all well-formed interfaces $F$, and for all components
$f=(X,Y,\mathcal{M})$ and $f_{\mathcal{E}}=(Y,X,\mathcal{E})$: if $f\models F$
and $f_{\mathcal{E}}\models F$, then
$(\mathcal{M}\cup\mathcal{E})^{*}\cap\mathcal{P}=\emptyset$.

We introduce below the auxiliary notion of derived properties, which are
guarantees that hold under any admissible environment. They are derived by
checking for all pairs $(z,y)$ of no-flows in the guarantees that there is no
alternated path using flows allowed by assumptions and guarantees that create
a flow from $z$ to $y$.

######  Definition 3.6.

We denote by $\mathcal{P}^{\mathcal{A},\mathcal{G}}$ the set of derived
properties from assumptions $\mathcal{A}$ and guarantees $\mathcal{G}$,
defined as follows
$\mathcal{P}^{\mathcal{A},\mathcal{G}}=\mathcal{G}\setminus((\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{*}\circ\overline{\mathcal{G}})$.

###  3.1 Composition

We now present how to compose components and interfaces. We introduce a
_compatibility_ predicate that checks whether the composition of two
interfaces is a well-formed interface. We prove that these two notions support
the _incremental design_ of systems. We prove that our composition is both
commutative and associative. The composition of two components is obtained as
the reflexive and transitive closure of union of individual component flows.

######  Definition 3.7.

We define the different type of variables between interfaces $F$ and
$F^{\prime}$, as follows: $Y_{F,F^{\prime}}=Y\cup Y^{\prime}$;
$X_{F,F^{\prime}}=(X\cup X^{\prime})\setminus Y_{F,F^{\prime}}$; and
$Z_{F,F^{\prime}}=Y_{F,F^{\prime}}\cup X_{F,F^{\prime}}$. The same definition
applies to components $f$ and $f^{\prime}$.

######  Definition 3.8.

The _composition_ of two components $f$ and $f^{\prime}$ is the component
defined as follows: $f\otimes
f^{\prime}=(X_{f,f^{\prime}},Y_{f,f^{\prime}},(\mathcal{M}\cup\mathcal{M}^{\prime})^{*}).$

We present interface composition by defining separately $\mathcal{A}$,
$\mathcal{G}$ and $\mathcal{P}$ of the composed interface.

The composition of two interfaces should not restrict the set of
implementations for each interface in isolation. We introduce below the notion
of _composite flows_ , as the set of all flows that can be in the composition
of any implementation of the interfaces being composed. We compute them by
considering all possible alternated paths between both interfaces. Then, given
that guarantees specify which flows cannot be implemented, we define
_composite guarantees_ as the composite flows’ complement.

######  Definition 3.9.

$F$ and $F^{\prime}$ _composite flows_ are defined as follows:

$\overline{\mathcal{G}}_{F,F^{\prime}}=(\text{Id}_{Z^{\prime}}\cup\overline{\mathcal{G}}_{F})\circ(\overline{\mathcal{G}}_{F^{\prime}}\circ\overline{\mathcal{G}}_{F})^{*}\circ(\text{Id}_{Y}\cup\overline{\mathcal{G}}_{F^{\prime}}).$

######  Definition 3.10.

$F$ and $F^{\prime}$ _composite guarantees_ are defined as
$\mathcal{G}_{F,F^{\prime}}\\!=\\!(Z_{F,F^{\prime}}\\!\times\\!Y_{F,F^{\prime}})\\!\setminus\\!\overline{\mathcal{G}}_{F,F^{\prime}}$.
We denote them by $\mathcal{G}_{F\otimes F^{\prime}}$ and
$\mathcal{G}_{F,F^{\prime}}$, interchangeably.

The assumptions of the composition of multiple interfaces is the weakest
condition on the environment that allows the interfaces being composed to work
together. Additionally, it must support incremental design. So, the
admissibility of an environment must be independent of the order in which the
interfaces are composed. Naturally, all the assumptions of each interface must
be considered during composition. However, not all of them can be kept as
assumptions of the composite.

The composition of two interfaces may change the classification of some input
variables of the interfaces being composed to output variables of their
composite (c.f. Definition 3.7). This happens to variables that are common to
both interfaces being composed, which we refer to as _shared variables_.
Interface assumptions that point to shared variables cannot be assumptions of
the composite interface, because they no longer point to an input variable.

Our solution is to compute _propagated assumptions_ between two interfaces.
Given an assumption pointing to a shared variable, we propagate it to all
variables that can reach the shared one. We define it below followed by an
illustrative example.

######  Definition 3.11.

The set of _assumptions propagated from $F$ to $F^{\prime}$_ is defined as
follows:

$\hat{\mathcal{A}}_{F\rightarrow F^{\prime}}=\\{(z,z^{\prime})\ |\ \exists
s\in X\cap Y^{\prime}\text{ s.t.\ }(z,s)\in\mathcal{A}\text{ and
}(z^{\prime},s)\in\overline{\mathcal{G}}_{F,F^{\prime}}\\}.$

The set with all propagated assumptions of $F$ and $F^{\prime}$ is defined as
$\hat{\mathcal{A}}_{F,F^{\prime}}=\hat{\mathcal{A}}_{F\rightarrow
F^{\prime}}\cup\hat{\mathcal{A}}_{F^{\prime}\rightarrow F}$.

The composite assumptions include all pairs that point to input variables and
are in the union of the assumptions of the interfaces being composed with
their propagated assumptions.

######  Definition 3.12.

The _composite assumptions_ of $F$ and $F^{\prime}$ is defined as follows:

$\mathcal{A}_{F,F^{\prime}}=(\mathcal{A}\cup\mathcal{A}^{\prime}\cup\hat{\mathcal{A}}_{F,F^{\prime}})\cap(Z_{F,F^{\prime}}\\!\times\\!X_{F,F^{\prime}})$.

######  Example 3.13.

$F_{\emph{imm}}\otimes
F_{\emph{can}}$$F_{\emph{can}}$candebecuimmimmcandebecukey$F_{\emph{imm}}$keycanimm

Figure 4: Assumptions for composion of $F_{\emph{imm}}$ with $F_{\emph{can}}$.

In Figure 4 we can see interface $F_{\emph{imm}}$ which has only one
assumption: key should not flow to can. As can is a shared variable of the
interfaces being composed, we need to compute the propagated assumptions that
it generates.

In $F_{\emph{can}}$ both ecu and imm can flow to can. So, they are allowed
flows in the composite interface, as well. Note that, by Definition 3.9,
$\\{(\textsf{ecu},\textsf{can}),(\textsf{imm},\textsf{can}),(\textsf{deb},\textsf{can})\\}\in\overline{\mathcal{G}}_{F_{\emph{imm}},F_{\emph{can}}}$.
Hence, by $\mathcal{A}_{F_{\emph{imm}}}=\\{(\textsf{key},\textsf{can})\\}$, we
have $\hat{\mathcal{A}}_{F_{\emph{imm}}\rightarrow
F_{\emph{can}}}=\\{(\textsf{key},\textsf{ecu}),(\textsf{key},\textsf{imm}),(\textsf{key},\textsf{deb})\\}$.
From the derived assumptions only $(\textsf{key},\textsf{ecu})$ points to an
input variable. Besides, as explained before, the only assumption of
$F_{\emph{imm}}$ cannot be kept after composition. Hence
$\mathcal{A}_{F_{\emph{imm}},F_{\emph{can}}}=\\{(\textsf{key},\textsf{ecu})\\}$.

The properties of the composition needs to preserve the individual properties
of each interface being composed. In addition, it adds all derived properties
from the assumptions and guarantees of the composite. This allows to infer
global properties from local specification.

######  Definition 3.14.

We denote by $\mathcal{P}_{F,F^{\prime}}$ the _composite properties_ of $F$
and $F^{\prime}$, defined as follows:
$\mathcal{P}_{F,F^{\prime}}=\mathcal{P}\cup\mathcal{P}^{\prime}\cup\mathcal{P}^{\mathcal{A}_{F,F^{\prime}},\mathcal{G}_{F,F^{\prime}}}$.

Interfaces composition is defined using the concepts of composite assumptions,
guarantees and properties defined before.

######  Definition 3.15.

The _composition_ of two interfaces $F$ and $F^{\prime}$ is the interface
defined as follows: $F\otimes
F^{\prime}=(X_{F,F^{\prime}},Y_{F,F^{\prime}},\mathcal{A}_{F,F^{\prime}},\mathcal{G}_{F,F^{\prime}},\mathcal{P}_{F,F^{\prime}}).$

We allow composition for any two arbitrary interfaces. However, not all
compositions result in well-formed interfaces. For this reason, we define the
notions of two interfaces being _composable_ and _compatible_. Composability
imposes the syntactic restriction that both interface’s output variables are
disjoint. Compatibility captures the semantic requirement that whenever an
interface $F$ provides inputs to an other interface $F^{\prime}$, then
$F^{\prime}$ needs to include guarantees that imply the assumptions of $F$.

######  Definition 3.16.

$F$ and $F^{\prime}$ are _composable_ iff $Y\cap Y^{\prime}=\emptyset$.

######  Definition 3.17.

Two interfaces $F$ and $F^{\prime}$ are _compatible_ , denoted $F\sim
F^{\prime}$ iff they are composable and
$((\mathcal{A}\cup\mathcal{A}^{\prime})\cap(Z_{F,F^{\prime}}\times
Y_{F,F^{\prime}}))\subseteq\mathcal{G}_{F,F^{\prime}}.$

######  Example 3.18.

$F_{\emph{imm}}\otimes F_{\emph{can}}$immcandebecukey$F_{\emph{ecu}}$keycanecu

Figure 5: Compatibility.

In Figure 5 we have interface $F_{\emph{ecu}}$ which has only one guarantee:
key does not flow to ecu. This interface is compatible with the composition of
$F_{\emph{can}}$ with $F_{\emph{imm}}$, because the only assumption of
$F_{\emph{can}}\otimes F_{\emph{imm}}$ is a guarantee of $F_{\emph{ecu}}$.

We prove below that our compatibility relation is sufficient to guarantee that
the result of composing two interfaces is a well-formed interface.

######  Theorem 3.19 (Composition preserves well-formedness).

Commutativity Let $F$ and $F^{\prime}$ be well-formed interfaces. If $F\sim
F^{\prime}$, then $F\otimes F^{\prime}$ is a well-formed interface.

The composition operator is both commutative and associative. In particular,
it supports incremental design of systems.

######  Proposition 3.20.

Let $F$ and $F^{\prime}$ be interfaces: $F\sim F^{\prime}\text{ iff
}F^{\prime}\sim F$, and $F\otimes F^{\prime}=F^{\prime}\otimes F$.

######  Theorem 3.21 (Incremental design).

Let $F$, $F^{\prime}$ and $F^{\prime\prime}$ be interfaces. If $F\sim
F^{\prime}$ and $(F\otimes F^{\prime})\sim F^{\prime\prime}$, then
$F^{\prime}\sim F^{\prime\prime}$ and $F\sim(F^{\prime}\otimes
F^{\prime\prime})$.

######  Proof 3.22 (Proof sketch).

We proved first that composite assumptions are associative. We assume that
$F\sim F^{\prime}$ and $(F\otimes F^{\prime})\sim F^{\prime\prime}$. The most
interesting case is when $(z,s)$ is an assumption of $F$ and we need to prove
$(z,s)\in\mathcal{G}_{F,F^{\prime}\otimes F^{\prime\prime}}$. We prove this by
assuming towards a contradiction that
$(z,s)\in\overline{\mathcal{G}}_{F,F^{\prime}\otimes F^{\prime\prime}}$. We
illustrate it in Figure 6.

$s$$z^{\prime}$$z$$z$$z^{\prime}$$s$$s^{\prime}$$F\otimes
F^{\prime}$$z^{\prime}$$F^{\prime\prime}$$s^{\prime}$$F$$\in\hat{\mathcal{A}}_{F\rightarrow
F^{\prime}}$

Figure 6: Incremental design.

By composite flows being associative,
$(z,s)\in\overline{\mathcal{G}}_{F\otimes F^{\prime},F^{\prime\prime}}$. By
$(z,s)$ being an assumption of $F$ and
$(s^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes F^{\prime}}$, then
$(z,s^{\prime})\\!\in\\!\hat{\mathcal{A}}_{F\rightarrow F^{\prime}}$ and, so
${(z,s^{\prime})\\!\in\\!\mathcal{A}_{F\otimes F^{\prime}}}$. Moreover,
${(z,s^{\prime})\\!\in\\!\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}}$, because $z$ can flow to $s^{\prime}$ when
$F\otimes F^{\prime}$ is composed with $F^{\prime\prime}$. This contradicts
our initial assumption that $(F\otimes F^{\prime})\sim F^{\prime\prime}$.

######  Corollary 3.23.

If $F\sim F^{\prime}$ and $F\otimes F^{\prime}\sim F^{\prime}$, then
$(F\otimes F^{\prime})\otimes F^{\prime\prime}=F\otimes(F^{\prime}\otimes
F^{\prime\prime}).$

Finally, we show that flows resulting from the composition of any components
that implement two given interfaces are allowed by the composition of these
interfaces.

######  Proposition 3.24.

Let $F$ and $F^{\prime}$ be interfaces, and $f=(X,Y,\mathcal{M})$ and
$f^{\prime}=(X^{\prime},Y^{\prime},\mathcal{M}^{\prime})$ be components. If
$f\models F$ and $f^{\prime}\models F^{\prime}$, then $f\otimes
f^{\prime}\models F\otimes F^{\prime}$.

###  3.2 Refinement and Independent Implementability

We now define a refinement relation between interfaces. Intuitively, an
interface $F^{\prime}$ refines $F$ iff $F^{\prime}$ admits more environments
than $F$, while constraining its implementations.

######  Definition 3.25.

Interface $F^{\prime}$ _refines_ $F$, written $F^{\prime}\preceq F$, when
${\mathcal{A}^{\prime}\subseteq\mathcal{A}}$,
$\mathcal{G}\subseteq\mathcal{G}^{\prime}$ and
$\mathcal{P}\subseteq\mathcal{P}^{\prime}$.

######  Proposition 3.26.

Let $F$ and $F^{\prime}$ be interfaces s.t. $F^{\prime}\preceq F$. Let
$f=(X,Y,\mathcal{M})$ and $f_{\mathcal{E}}=(Y,X,\mathcal{E})$ be components.
(a) If $f\models F^{\prime}$, then $f\models F$; and  (b) if
$f_{\mathcal{E}}\models F$, then $f_{\mathcal{E}}\models F^{\prime}$.

Derived properties are helpful to simplify the concept of wellformedness of an
interface. In fact, an interface is well-formed iff all no-flows in its
property are in the set of derived properties from its assumptions and
guarantees.

######  Proposition 3.27.

An interface $F=(X,Y,\mathcal{A},\mathcal{G},\mathcal{P})$ is well-formed iff
$\mathcal{P}\subseteq\mathcal{P}^{\mathcal{A},\mathcal{G}}$.

######  Theorem 3.28 (Independent implementability).

For all well-formed interfaces $F_{1}^{\prime}$, $F_{1}$ and $F_{2}$, if
$F_{1}^{\prime}\preceq F_{1}$ and $F_{1}\sim F_{2}$, then $F_{1}^{\prime}\sim
F_{2}$ and $F_{1}^{\prime}\otimes F_{2}\preceq F_{1}\otimes F_{2}$.

######  Proof 3.29 (Proof sketch).

(Full proof in appendix A) The challenging part is to prove that the refined
composite contains all properties of the abstracted one, i.e.
$\mathcal{P}_{F_{1}\otimes F_{2}}\subseteq\mathcal{P}_{F_{1}^{\prime}\otimes
F_{2}}$. We prove by induction on $n\in\mathbb{N}$ that: if
$(z,y)\notin(\text{Id}_{Z_{F_{1},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1},F_{2}}\circ\overline{\mathcal{A}}_{F_{1},F_{2}})^{n}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}$,
then
$(z,y)\notin(\text{Id}_{Z_{F_{1}^{\prime},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})^{n}\circ\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}.$
We remark that for all $(z,s)\in\overline{\mathcal{A}}_{F_{1},F_{2}}$ s.t.
there exists $(s,y)\in\mathcal{G}_{F_{1},F_{2}}$, then, by
$F_{1}^{\prime}\preceq F_{1}$, it follows that for all
$(z,s)\in\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}}$ there exists
$(s,y)\in\mathcal{G}_{F_{1}^{\prime},F_{2}}$. Hence if
$(z,y)\notin\overline{\mathcal{A}}_{F_{1},F_{2}}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}$,
then
$(z,y)\notin\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}$
as well.

###  3.3 Shared Refinement

The _shared refinement between two interfaces_ is their most general
refinement. It allows to describe components that are meant to be used in
different environments by providing separate descriptions for each case.
Implementation of the shared refined interface must be able to work with both
environments while guaranteeing the same properties.

In order to cope with both environments it may be necessary to allow the
environment to create flows that were assumed to not be there by one of the
interfaces. This may be problematic, because a property may need that no-flow
to be satisfied. To overcome this, we introduce _propagated guarantees_ below.
The idea is that for each no-flow assumption $(z,x)$ that cannot be in the
shared refined interface and for which it is relevant for a no-flow property
$(x,y)$ to hold, we add a no-flow guarantee $(x,y)$ that prevents a flow from
the sink of that assumption to the sink of the property.

######  Definition 3.30.

Let $F$ and $F^{\prime}$ be two interfaces. The _propagated guarantees_ $F$
and $F^{\prime}$ is defined as: $\hat{\mathcal{G}}_{F\rightarrow
F^{\prime}}=\\{(x,y)\ |\ (z,x)\in\mathcal{A},\
(z,x)\notin\mathcal{A}^{\prime}\text{ and }(z,y)\in\mathcal{P}\\}.$ The set of
all propagated assumptions is defined as $\hat{\mathcal{G}}_{F\rightarrow
F^{\prime}}=\hat{\mathcal{G}}_{F\rightarrow
F^{\prime}}\cup\hat{\mathcal{G}}_{F^{\prime}\rightarrow F}$.

######  Definition 3.31.

Let $F$ and $F^{\prime}$ be two interfaces such that $X=X^{\prime}$ and
$Y=Y^{\prime}$. The _shared refinement of_ $F$ and $F^{\prime}$ is defined as:
$F\sqcap
F^{\prime}=(X,Y,\mathcal{A}\cap\mathcal{A}^{\prime},\mathcal{G}\cup\mathcal{G}^{\prime}\cup\hat{\mathcal{G}}_{F,F^{\prime}},\mathcal{P}\cup\mathcal{P}^{\prime})$.

In the following, we prove that if interfaces are well-formed then their
shared refinement is well-formed, as well. Additionally, we show that the
shared refinement is the most abstract well-formed interface that refine both
of them.

######  Theorem 3.32.

Let $F$, $F^{\prime}$ and $F^{\prime}$ be well-formed interfaces. $F\sqcap
F^{\prime}$ is a well-formed interface; and if $F^{\prime\prime}\preceq F$ and
$F^{\prime\prime}\preceq F^{\prime}$, then $F^{\prime\prime}\preceq F\sqcap
F^{\prime}$.

######  Proof 3.33 (Proof sketch).

(Full proof in appendix A) The interesting step is to prove that the shared
refinement is well-formed. We assume towards a contradiction that it does not
hold. Then, we prove the following statement about alternated paths, for all
$n\in\mathbb{N}$: if
$(z,y)\in((\text{Id}_{Z}\cup\overline{\mathcal{A}}_{F\sqcap
F^{\prime}})\circ(\overline{\mathcal{G}}_{F\sqcap
F^{\prime}}\circ\overline{\mathcal{A}}_{F\sqcap
F^{\prime}})^{n}\circ\overline{\mathcal{G}}_{F\sqcap F^{\prime}})$, then
$(z,y)\in((\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{n}\circ\overline{\mathcal{G}})$.
Note that, if $(z,y)\in\mathcal{P}$, $(z,s)\in\mathcal{A}$ and
$(z,s)\notin\mathcal{A}^{\prime}$ then, by definition of propagated
guarantees, $(s,y)\in\hat{\mathcal{G}}_{F\rightarrow F^{\prime}}$. Thus, by
definition of shared refinement, it cannot be the case that
$(s,y)\in\overline{\mathcal{G}}_{F\sqcap F^{\prime}}$, and so
$(z,y)\notin\overline{\mathcal{A}}_{F\sqcap
F^{\prime}}\circ\overline{\mathcal{G}}_{F\sqcap F^{\prime}}$.

###  3.4 Discussion

Properties. Without properties in our interfaces (i.e. only with assumptions
and guarantees) it is not possible to define an useful algebra to specify
structural properties of no-flows that supports both incremental design and
independent implementability. Consider the top-down design of a system where
we start by defining a no-flow in a closed system that we expect to be
preserved along the decomposition of this system into smaller open systems.
Then, we would need assumptions or guarantees to specify global no-flows (i.e.
restrictions that hold under any composition of its implementations with any
of its environments). Then, we could not support incremental design.
Compatibility criteria for interfaces with global no-flows would need to be
too strong with intuitive and correct designs considered incompatible. Note
that, for any two variables $x$ and $y$ there exists an interface that can
create a flow between them, as long as $x$ is a source of some flow and $y$ is
a sink of some other flow. Hence we introduce global requirements as
_properties_ that enforces a well-formedness criteria on assumptions and
guarantees while it allows interfaces to be independently specified and
implemented.

Completing interfaces. There is no unique way to extend an ill-formed
interface into a well-formed one. Given an alternated path that witnesses a
violation of a property, it is sufficient to add one of its elements to the
interface specification to remove this specific violation. So, there are as
many extensions to the ill-formed interface as the elements in that path, and
all of them are incomparable.

Semantics. In this work we do not adopt any specific semantic characterization
of information flows, as we only work with its (abstracted) structural
properties. One possible interpretation of the pairs $(x,y)$ in _no-flow_
relations is as _independence predicates_. Then, $x$ is independent of $y$ if
the system outputs all combinations of all the possible values of $x$ and $y$.
Formally, if $\pi$ and $\pi^{\prime}$ are observations of different runs of
the system at time $t$, with $\pi[t](x)$ being the value of $x$ in $\pi$ at
that time, then there must exist a third observation $\pi^{\prime\prime}$ such
that $\pi[t](x)=\pi^{\prime\prime}[t](x)\ \wedge\
\pi^{\prime}[t](y)=\pi^{\prime\prime}[t](y)$, i.e. $\pi^{\prime\prime}$
_interleaves_ the value off $x$ in $\pi$ with $y$ in $\pi^{\prime}$.

##  4 Stateful Interfaces

We extend our theory with stateful components and interfaces. These are
transition systems in which each state is a stateless component or interface,
respectively. Proofs are in appendix B.

######  Definition 4.1.

A _stateful information-flow component_ $\mathbbm{f}$ is a tuple
$(X,Y,Q,\hat{q},\delta,\mathbb{M})$, where: $X$ and $Y$ are disjoint sets of
_input_ and _output_ variables respectively, with $Z=X\cup Y$ the set of all
variables; $Q$ is a set of states and $\hat{q}\in Q$ is the initial state;
$\delta:Q\rightarrow 2^{Q}$ is a transition relation; $\mathbb{M}:Q\rightarrow
2^{Z\times Y}$ is a state labeling. For each state $q\in Q$ we require that
$\mathbb{M}(q)$ is a flow relation and we denote by
$\mathbbm{f}(q)=(X,Y,\mathbb{M}(q))$ the stateless component implied by the
labeling of $q$.

######  Definition 4.2.

A _stateful information-flow interface_ $\mathbb{F}$ is a tuple
$(X,Y,Q,\hat{q},\delta,\mathbb{A},\mathbb{G},\mathbb{P})$, where: $X$ and $Y$
are disjoint sets of _input_ and _output_ variables, respectively; $Q$ is a
set of states and $\hat{q}\in Q$ is the initial state; $\delta:Q\rightarrow
2^{Q}$ is a transition relation; $\mathbb{A}:Q\rightarrow 2^{Z\times X}$ is
called _assumption_ ; $\mathbb{G}:Q\rightarrow 2^{Z\times Y}$ is called
_guarantee_ ; and $\mathbb{P}:Q\rightarrow 2^{Z\times Y}$ is called
_property_. For each state $q\in Q$ we require that $\mathbb{A}(q)$,
$\mathbb{G}(q)$ and $\mathbb{P}(q)$ are no-flow relations and we denote by
$\mathbb{F}(q)=(X,Y,\mathbb{A}(q),\mathbb{G}(q),\mathbb{P}(q))$ the stateless
interface implied by the assumption, guarantee and property of $q$.

In what follows,
$\mathbb{F}=(X,Y,Q,\hat{q},\delta,\mathbb{A},\mathbb{G},\mathbb{P})$ and
$\mathbb{F}^{\prime}=(X^{\prime},Y^{\prime},Q^{\prime},\hat{q}^{\prime},\delta^{\prime},\mathbb{A}^{\prime},\mathbb{G}^{\prime},\mathbb{P}^{\prime})$
are stateful interfaces, and
$\mathbbm{f}=(X,Y,Q_{\mathbbm{f}},\hat{q}_{\mathbbm{f}},\delta_{\mathbbm{f}},\mathbb{M})$
and
$\mathbbm{f}_{\mathcal{E}}=(Y,X,Q_{\mathcal{E}},\hat{q}_{\mathcal{E}},\delta_{\mathcal{E}},\mathbb{E})$
are stateful components.

######  Definition 4.3.

A _stateful interface_ $\mathbb{F}$ is well-formed iff $\mathbb{F}(\hat{q})$
is a well-formed stateless interface, and for all $q\in Q$ reachable from
$\hat{q}$ the stateless interface $\mathbb{F}(q)$ is well-formed.

###  4.1 Implements

A stateful component $\mathbbm{f}$ implements a stateful interface
$\mathbb{F}$ if there exists a simulation relation from $\mathbbm{f}$ to
$\mathbb{F}$ such that the stateless components in the relation implement the
stateless interfaces they are related to. Admissible environments are defined
analogously.

######  Definition 4.4.

A component $\mathbbm{f}$ _implements_ the interface $\mathbb{F}$, denoted by
$\mathbbm{f}\models\mathbb{F}$, iff there exists $H\subseteq
Q_{\mathbbm{f}}\times Q$ s.t. $(\hat{q}_{\mathbbm{f}},\hat{q})\in H$ and for
all $(q_{\mathbbm{f}},q)\in H$:  (i)
$\mathbbm{f}(q_{\mathbbm{f}})\models\mathbb{F}(q)$; and  (ii) if
$q_{\mathbbm{f}}^{\prime}\in\delta_{\mathbbm{f}}(q_{\mathbbm{f}})$, then there
exists a state $q^{\prime}\in\delta(q)$ s.t.
$(q_{\mathbbm{f}}^{\prime},q^{\prime})\in H$.

######  Definition 4.5.

A component $\mathbbm{f}_{\mathcal{E}}$ is an _admissible environment_ for the
interface $\mathbb{F}$, denoted by
$\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}$, iff there exists a relation
$H\subseteq Q\times Q_{\mathcal{E}}$ s.t. $(\hat{q},\hat{q}_{\mathcal{E}})\in
H$ and for all $(q,q_{\mathcal{E}})\in H$:  (i)
$\mathbbm{f}(q_{\mathcal{E}})\models\mathbb{F}(q)$; and  (ii) if
$q^{\prime}\in\delta_{\mathbb{F}}(q)$, then there exists a state
$q_{\mathcal{E}}^{\prime}\in\delta_{\mathcal{E}}(q_{\mathcal{E}})$ s.t.
$(q^{\prime},q_{\mathcal{E}}^{\prime})\in H$.

As for stateless interfaces, we want to prove that interface’s properties are
satisfied after we compose any of its implementations $\mathbbm{f}$ with any
of its admissible environments $\mathbbm{f}_{\mathcal{E}}$. We prove this
below for all sates $q$ that are common to any pair of relations witnessing
$\mathbbm{f}\models\mathbb{F}$ and
$\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}$.

######  Proposition 4.6.

Let $\mathbb{F}$ be a well-formed interface, and
$\mathbbm{f}\models\mathbb{F}$ and
$\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}$. For all $H\subseteq
Q_{\mathbbm{f}}\times Q$ and $H_{\mathcal{E}}\subseteq Q\times
Q_{\mathcal{E}}$ that witness them, respectively, then:  (i)
$(\mathbb{M}(\hat{q}_{\mathbbm{f}})\cup\mathbb{E}(\hat{q}_{\mathcal{E}}))^{*}\cap\mathbb{P}(\hat{q})=\emptyset$;
and  (ii) for all $q\in Q$ that are reachable from $\hat{q}$, if
$(q_{\mathbbm{f}},q)\in H$ and $(q,q_{\mathcal{E}})\in H_{\mathcal{E}}$, then
$(\mathbb{M}(q_{\mathbbm{f}})\cup\mathbb{E}(q_{\mathcal{E}}))^{*}\cap\mathbb{P}(q)=\emptyset.$

###  4.2 Composition

Composition of two components is defined as their synchronous product. The
composition of two interfaces is defined as their synchronous product, as
well. However, we only keep the states that are defined by the composition of
two comptible stateless interfaces. Recall that we assume that the environment
is helpful, so it will respect state’s assumptions.

######  Definition 4.7.

Let $\mathbbm{f}$ and $\mathbbm{f}^{\prime}$ be two components. Their
_composition_ is defined as the tuple:
$\mathbbm{f}\otimes\mathbbm{f}^{\prime}=(X_{\mathbbm{f},\mathbbm{f}^{\prime}},Y_{\mathbbm{f},\mathbbm{f}^{\prime}},Q_{\mathbbm{f},\mathbbm{f}^{\prime}},\hat{q}_{\mathbbm{f},\mathbbm{f}^{\prime}},\delta_{\mathbbm{f},\mathbbm{f}^{\prime}},\mathbb{M}_{\mathbbm{f},\mathbbm{f}^{\prime}})$,
where: $Q_{\mathbbm{f},\mathbbm{f}^{\prime}}=Q\times Q^{\prime}$ with
$\hat{q}_{\mathbbm{f},\mathbbm{f}^{\prime}}=(\hat{q},\hat{q}^{\prime})$;
$(q_{2},q_{2}^{\prime})\in\delta_{\mathbbm{f},\mathbbm{f}^{\prime}}(q_{1},q_{1})$
iff $q_{2}\in\delta(q_{1})$ and
$q_{2}^{\prime}\in\delta^{\prime}(q_{1}^{\prime})$; for all $(q,q^{\prime})\in
Q_{\mathbbm{f},\mathbbm{f}^{\prime}}:\
\mathbb{M}_{\mathbbm{f},\mathbbm{f}^{\prime}}(q,q^{\prime})=(\mathbb{M}(q)\cup\mathbb{M}^{\prime}(q^{\prime}))^{*}$.

######  Definition 4.8.

Let $\mathbb{F}$ and $\mathbb{F}^{\prime}$ be two interfaces. Their
_composition_ is defined as the tuple:
$\mathbb{F}\otimes\mathbb{F}^{\prime}=(X_{\mathbb{F},\mathbb{F}^{\prime}},Y_{\mathbb{F},\mathbb{F}^{\prime}},Q_{\mathbb{F},\mathbb{F}^{\prime}},\hat{q}_{\mathbb{F},\mathbb{F}^{\prime}},\delta_{\mathbb{F},\mathbb{F}^{\prime}},\mathbb{A}_{\mathbb{F},\mathbb{F}^{\prime}},\mathbb{G}_{\mathbb{F},\mathbb{F}^{\prime}},\mathbb{P}_{\mathbb{F},\mathbb{F}^{\prime}}),$
where: $\hat{q}_{\mathbb{F},\mathbb{F}^{\prime}}=(\hat{q},\hat{q}^{\prime})$
and
$Q_{\mathbb{F},\mathbb{F}^{\prime}}=\\{\hat{q}_{\mathbb{F},\mathbb{F}^{\prime}}\\}\cup\\{(q,q^{\prime})\
|\ \mathbb{F}(q)\sim\mathbb{F}^{\prime}(q^{\prime})\\}$;
$(q_{2},q_{2}^{\prime})\in\delta_{\mathbb{F},\mathbb{F}^{\prime}}(q_{1},q^{\prime}_{1})$
iff $q_{2}\in\delta(q_{1})$ and
$q_{2}^{\prime}\in\delta^{\prime}(q_{1}^{\prime})$; for all $(q,q^{\prime})\in
Q_{\mathbb{F},\mathbb{F}^{\prime}}:\
\mathbb{F}_{\mathbb{F},\mathbb{F}^{\prime}}(q,q^{\prime})=\mathbb{F}(q)\otimes\mathbb{F}^{\prime}(q^{\prime})$.

Two stateful interfaces are compatible if the stateless interfaces defined by
their initial states are compatible. Note that this implies that all of the
states reachable from the initial state are defined by the composition of two
compatible stateless interfaces, as well.

######  Definition 4.9.

Two interfaces $\mathbb{F}$ and $\mathbb{F}^{\prime}$ are _compatible_ ,
denoted by $\mathbb{F}\sim\mathbb{F}^{\prime}$, iff
$\mathbb{F}(\hat{q})\sim\mathbb{F}^{\prime}(\hat{q}^{\prime})$.

We prove below propositions related to the composition of stateful interfaces
that follow from results from the stateless interfaces.

######  Proposition 4.10.

For all interfaces $\mathbb{F}$ and $\mathbb{F}^{\prime}$:
$\mathbb{F}\sim\mathbb{F}^{\prime}\text{ iff
}\mathbb{F}^{\prime}\sim\mathbb{F}$.

######  Proposition 4.11 (Composition preserves well-formedness).

For all well-formed interfaces $\mathbb{F}_{1}$ and $\mathbb{F}_{2}$: If
$\mathbb{F}_{1}\sim\mathbb{F}_{2}$, then $\mathbb{F}_{1}\otimes\mathbb{F}_{2}$
is a well-formed interface.

######  Proposition 4.12 (Incremental design).

For all interfaces $\mathbb{F}$, $\mathbb{G}$ and $\mathbb{I}$, if
$\mathbb{F}\sim\mathbb{G}$ and $(\mathbb{F}\otimes\mathbb{G})\sim\mathbb{I}$,
then $\mathbb{G}\sim\mathbb{I}$ and
$\mathbb{F}\sim(\mathbb{G}\otimes\mathbb{I})$.

######  Proposition 4.13.

If $\mathbbm{f}\models\mathbb{F}$ and $\mathbbm{g}\models\mathbb{G}$, then
$\mathbbm{f}\otimes\mathbbm{g}\models\mathbb{F}\otimes\mathbb{G}$.

######  Proof 4.14.

Let $H_{\mathbbm{f}}$ and $H_{\mathbbm{g}}$ be the witnesses for
$\mathbbm{f}\models\mathbb{F}$ and $\mathbbm{g}\models\mathbb{G}$. Then, the
relation
${H=\\{((q_{\mathbbm{f}},q_{\mathbbm{g}}),(q_{\mathbb{F}},q_{\mathbb{G}}))\ |\
q_{\mathbb{F}}\in H_{\mathbbm{f}}(q_{\mathbbm{f}})\text{ and
}q_{\mathbb{G}}\in H_{\mathbbm{g}}(q_{\mathbbm{g}})\\}}$ witnesses
$\mathbbm{f}\otimes\mathbbm{g}\models\mathbb{F}\otimes\mathbb{G}$.

###  4.3 Refinement

Given an interface, we define transitions parameterized by no-flows on its
input variables (i.e. with fixed assumptions) or on its output variables (i.e.
with fixed guarantees and properties).

######  Definition 4.15.

Let $\mathbb{F}$ be an interface. _Input transitions_ from a given state $q\in
Q$ are defined as $\delta^{X}(q)=\\{\delta^{X}(q,\mathcal{A})\ |\
\mathcal{A}\subseteq Z\times X\\}$ with
$\delta^{X}(q,\mathcal{A})=\\{q^{\prime}\in\delta(q)\ |\
\mathbb{A}(q^{\prime})=\mathcal{A}\\}$. _Output transitions_ from a given
state $q\in Q$ are defined as
$\delta^{Y}(q)=\\{\delta^{Y}(q,\mathcal{G},\mathcal{P})\ |\
\mathcal{G}\subseteq Z\times Y\text{ and }\mathcal{P}\subseteq Z\times Y\\}$
with $\delta^{Y}(q,\mathcal{G},\mathcal{P})=\\{q^{\prime}\in\delta(q)\ |\
\mathbb{G}(q^{\prime})=\mathcal{G}\text{ and
}\mathbb{P}(q^{\prime})=\mathcal{P}\\}$.

Interface $\mathbb{F}_{R}$ refines $\mathbb{F}_{A}$, if all output steps of
$\mathbb{F}_{R}$ can be simulated by $\mathbb{F}_{A}$, while all input steps
of $\mathbb{F}_{A}$ can be simulated by $\mathbb{F}_{R}$. This corresponds to
alternating alternating refinement, as introduced in [1].

######  Definition 4.16.

Interface $\mathbb{F}_{R}$ _refines_ $\mathbb{F}_{A}$, written
$\mathbb{F}_{R}\preceq\mathbb{F}_{A}$, iff there exists a relation $H\subseteq
Q_{R}\times Q_{A}$ s.t. $(\hat{q}_{R},\hat{q}_{A})\in H$ and for all
$(q_{R},q_{A})\in H$:  (i)
$\mathbb{F}_{R}(q_{R})\preceq\mathbb{F}_{A}(q_{A})$;  (ii) for all set of
states $O\in\delta^{Y}_{R}(q_{R})$, there exists
${O^{\prime}\in\delta^{Y}_{A}(q_{A})}$ s.t. for all set of states
$I^{\prime}\in\delta^{X}_{A}(q_{A})$, there exists $I\in\delta^{X}_{R}(q_{R})$
s.t. $(O\cap I)\times(O^{\prime}\cap I^{\prime})\subseteq H$.

######  Example 4.17.

$z$$y$$x$$z$$y$$x$$z$$y$$x$$z$$y$$x$$x$$y$$z$$y$$y^{\prime}$$x^{\prime}$$x$$x$$y$$y^{\prime}$$x^{\prime}$$x$$y$$y^{\prime}$$x^{\prime}$$x$$y$$y^{\prime}$$x^{\prime}$$y$$y^{\prime}$$x^{\prime}$$x$$\preceq$$\preceq$$\hat{q}_{1}$$q_{2}$$q^{\prime}_{2}$$q^{\prime}_{3}$$\hat{q}^{\prime}_{1}$$\hat{q}_{1}$$\hat{q}^{\prime}_{1}$$q^{\prime}_{2}$$q_{2}$$q_{3}$

Figure 7: Refined interfaces with witness:
(a)$\\{(\hat{q}_{1},\hat{q}_{1}^{\prime}),(q_{2},q_{2}^{\prime})\\}$; and (b)
$\\{(\hat{q}_{1},\hat{q}_{1}^{\prime}),(q_{2},q_{2}^{\prime}),(q_{3},q_{2}^{\prime})\\}$.

In Figure 7 we depict two examples of refined stateful interfaces.

In Figure 7(a) the stateless interface in each state only uses output ports
and it only specifies properties. The initial state of both stateful
interfaces is the same, so they clearly refine each other. As there are no
assumptions and guarantees, then, by Definition 4.16, we need to check that
for all successors of the initial state in the refined interface $q_{s}$,
there exists a successor of the initial state in the abstract interface
$q^{\prime}_{s}$ such that
$\mathbb{P}_{A}(q^{\prime}_{s})\subseteq\mathbb{P}_{R}(q_{s})$. This holds for
the states $(q_{2},q_{2}^{\prime})$. Hence the relation
$\\{(\hat{q}_{1},\hat{q}_{1}^{\prime}),(q_{2},q_{2}^{\prime})\\}$ witnesses
the refinement. Note that the refined interface is obtained by removing a
nondeterministic choice on the transition function.

The witness relation for the refinement depicted in Figure 7(b) is
$\\{(\hat{q}_{1},\hat{q}_{1}^{\prime}),(q_{2},q_{2}^{\prime}),(q_{3},q_{2}^{\prime})\\}$.
The initial states are the same, so the condition (i) in Definition 4.16 is
trivially satisfied. The refined interface has two distinct output transitions
from the initial state $\hat{q}_{1}$. It can either go to state $q_{2}$ by
choosing the set of guarantees and proposition with only one element $(x,y)$
or it can transition to state $q_{3}$ by committing to the set of no-flows
$\\{(x,y),(x^{\prime},y)\\}$ for the guarantees and $\\{(x,y)\\}$ as property.
From the initial state of the abstract interface, there exists only one input
transition possible, to assume that $x$ does not flow to $x^{\prime}$ and
$y^{\prime}$ does not flow to $x$. The following holds for both states
accessible from the initial state in the refined interface:
$\mathbb{A}_{R}(q_{2})\subseteq\mathbb{A}_{A}(q^{\prime}_{2})$ and
$\mathbb{A}_{R}(q_{3})\subseteq\mathbb{A}_{A}(q^{\prime}_{2})$. The refined
interface specifies an alternative transition from the initial state
(represented by state $q_{3}$) that allows more environments while restricting
the implementation and preserving the property.

######  Theorem 4.18.

Let $\mathbb{F}^{\prime}\preceq\mathbb{F}$.  (a) If
$\mathbbm{f}\models\mathbb{F}^{\prime}$, then $\mathbbm{f}\models\mathbb{F}$.
(b) If $\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}$, then
$\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}^{\prime}$.

######  Proof 4.19.

Let $H_{\preceq}\subseteq Q_{1}\times Q_{2}$ be the relation witnessing
$H_{\preceq}\subseteq Q_{1}\times Q_{2}$.  (a) Let $H_{\models}\subseteq
Q_{\mathbbm{f}}\times Q_{1}$ be the relation witnessing
$\mathbbm{f}\models\mathbb{F}_{1}$. Then, $H=H_{\models}\circ H_{\preceq}$
witnesses $\mathbbm{f}\models\mathbb{F}$.  (b) Let $H_{\models}\subseteq
Q_{2}\times Q_{\mathcal{E}}$ be the relation witnessing
$\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}$. Then, $H=H_{\preceq}\circ
H_{\models}$ witnesses $\mathbbm{f}_{\mathcal{E}}\models\mathbb{F}^{\prime}$.

######  Theorem 4.20 (Independent implementability).

For all well-formed interfaces $\mathbb{F}_{1}^{\prime}$, $\mathbb{F}_{1}$ and
$\mathbb{F}_{2}$, if $\mathbb{F}_{1}^{\prime}\preceq\mathbb{F}_{1}$ and
$\mathbb{F}_{1}\sim\mathbb{F}_{2}$, then
$\mathbb{F}_{1}^{\prime}\sim\mathbb{F}_{2}$ and
$\mathbb{F}_{1}^{\prime}\otimes\mathbb{F}_{2}\preceq\mathbb{F}_{1}\otimes\mathbb{F}_{2}$.

######  Proof 4.21.

Let $H_{\preceq}\subseteq Q_{1}^{\prime}\times Q_{1}$ be the relation that
witnesses $\mathbb{F}_{1}^{\prime}\preceq\mathbb{F}_{1}$. Then, the relation
$H=\\{((q_{\mathbb{F}_{1}^{\prime}},q_{\mathbb{F}_{2}}),(q_{\mathbb{F}_{1}},q_{\mathbb{F}_{2}}))\
|\ (q_{\mathbb{F}_{1}^{\prime}},q_{\mathbb{F}_{1}})\\!\in\\!H_{\preceq}\text{
and
}\mathbb{F}_{1}(q_{\mathbb{F}_{1}})\sim\mathbb{F}_{2}(q_{\mathbb{F}_{2}})\\}$witnesses
$\mathbb{F}_{1}^{\prime}\\!\otimes\\!\mathbb{F}_{2}\preceq\mathbb{F}_{1}\\!\otimes\\!\mathbb{F}_{2}$.

###  4.4 Trace Semantics

In this section, we explore three set semantics for a particular stateful
interface. For simplicity, we restrict our attention to boolean variables.
Trace properties $T$ are defined as sets of infinite traces over the set of
propositional variables, that is, $T\subseteq Z^{\omega}$. The set
$\mathbb{T}=2^{Z^{\omega}}$ defines the set of all trace properties. A
system’s implementation is characterized by a set of its executions $S$
represented as a set of traces. An interface characterizes a set of
implementations,thus it defines sets of sets of traces, $\textbf{T}\subseteq
2^{\mathbb{T}}$.

$z$$y$$x$$x$$y$$z$

Figure 8: Stateful interface $\mathbb{F}_{\mathcal{U}}$.

Interface $\mathbb{F}_{\mathcal{U}}$, in Figure 9, specifies that $x$ does not
flow to $y$ until $x$ does not flow to $z$ and it stays in that state. In this
example, no-flows are interpreted as introduced in subsection 3.4. We use the
abbreviation $x_{1}[t]\not\rcurvearrowright_{3}y_{2}[t]\equiv x\neq y\ \wedge\
\pi_{1}[t](x)=\pi_{3}[t](x)\ \wedge\ \pi_{2}[t](y)=\pi_{3}[t](y)$, where
$\pi[t](x)$ denotes the _valuation of variable $x$ at time $t$ in $\pi$_.

To capture our intended interpretation for the no-flow predicate $\pi$ and
$\pi^{\prime}$ need to be universally quantified while $\pi^{\prime\prime}$
needs to be existentially quantified. The quantification over time admits
different interpretations. We can, for instance, force all traces of an
implementation to be synchronous concerning the states in that interface.
Then, state transitions are satisfied at the same time in all traces of an
implementation. This is the _strong no-flow_ interpretation over time.
Alternatively, we can require that for any arbitrary observation of a system
execution all valuations witnessing a no-flow requirement w.r.t. other
observations need to be in the same time point. In this case, state
transitions must be synchronous with respect to individual traces. This is the
_structure-aware no-flow_ interpretation over time. Finally, we may only
require that the witnesses are presented in some time which may differ for
each triple of traces. We refer to this interpretation as _unstructured no-
flow_.

######  Definition 4.22.

We define that _$x_{1}\not\rcurvearrowright_{3}y_{2}$ until it always holds
that $x_{1}\not\rcurvearrowright_{3}z_{2}$_ as:

$\displaystyle\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\equiv\ 0<t\
\wedge\ (\forall 0\leq t^{\prime}<t\
x_{1}[t^{\prime}]\not\rcurvearrowright_{3}y_{2}[t^{\prime}])\ \wedge(\forall
t\leq t^{\prime\prime}\
x_{1}[t^{\prime\prime}]\not\rcurvearrowright_{3}z_{2}[t^{\prime\prime}]).$

There are three plausible set semantics for $\mathbb{F}_{\mathcal{U}}$, which
differ in the position of $\exists t$:

Strong no-flow

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}=\\{T\ |\ \exists t\
\forall\pi_{1}\\!\in\\!T\ \forall\pi_{2}\\!\in\\!T\
\exists\pi_{3}\\!\in\\!T:\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\\}$;

Structure-aware no-flow

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}=\\{T\ |\
\forall\pi_{1}\\!\in\\!T\ \exists t\ \forall\pi_{2}\\!\in\\!T\
\exists\pi_{3}\\!\in\\!T:\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\\}$;

Unstructured no-flow

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}=\\{T\ |\
\forall\pi_{1}\\!\in\\!T\ \forall\pi_{2}\\!\in\\!T\ \exists\pi_{3}\\!\in\\!T\
\exists t:\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\\}$.

Clearly,
$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}$.
The other direction does not hold. Hence these set semantics are not
equivalent.

######  Theorem 4.23.

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}\not\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}\not\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}.$

######  Proof 4.24.

$T_{u}\in\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}$ but
$T_{u}\notin\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}$. And,
$T_{a}\in\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}$ but
$T_{a}\notin\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}$.

| t=0 | t=1 | 1 < t
---|---|---|---
| x | y | z | x | y | z | x | y | z
$\pi_{1}$ | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0
$\pi_{2}$ | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0
$\pi_{3}$ | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0

Table 1: Set of traces $T_{u}$.

| t=0 | t=1 | 1 < t
---|---|---|---
| x | y | z | x | y | z | x | y | z
$\pi_{1}$ | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0
$\pi_{2}$ | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0
$\pi_{3}$ | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0
$\pi_{4}$ | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0

Table 2: Set of traces $T_{a}$.

Linear temporal logic [27] (LTL) cannot express the properties introduced in
Definition 4.25 [8, 7]. LTL extended with knowledge (linear time epistemic
logic [5]) under the synchronous perfect recall semantics can express the
strong no-flow interpretation of $\mathbb{F}_{\mathcal{U}}$ [5]. The
unstructured no-flow semantics can be specified in HyperLTL [7]. HyperLTL
extends LTL by allowing quantification over traces, which occur at the
beginning of the formula. Epistemic temporal logic and HyperLTL have
incomparable expressive power [5]. To the best of our knowledge, there is no
temporal formalism that supports the structure-aware semantics.

###  4.5 Discussion

The composition operation on stateful information-flow interfaces can be
generalized to distinguish between compatible and incompatible transitions of
interfaces when they are composed. Usually this is done by labeling
transitions with letters from an alphabet, so that only transitions with the
same letter can be synchronized. While necessary for practical modeling, we
omit this technical generalization to allow the reader to focus on the
novelties of our formalism, which are the information-flow constraints
(environment assumptions, implementation guarantees, and global properties) at
each state of an interface.

###  4.6 Trace Semantics

In this section, we explore three set semantics for a particular stateful
interface. For simplicity, we restrict our attention to boolean variables.
Trace properties $T$ are defined as sets of infinite traces over the set of
propositional variables, that is, $T\subseteq Z^{\omega}$. The set
$\mathbb{T}=2^{Z^{\omega}}$ defines the set of all trace properties. A
system’s implementation is characterized by a set of its executions $S$
represented as a set of traces. An interface characterizes a set of
implementations,thus it defines sets of sets of traces, $\textbf{T}\subseteq
2^{\mathbb{T}}$.

$z$$y$$x$$x$$y$$z$

Figure 9: Stateful interface $\mathbb{F}_{\mathcal{U}}$.

Interface $\mathbb{F}_{\mathcal{U}}$, in Figure 9, specifies that $x$ does not
flow to $y$ until $x$ does not flow to $z$ and it stays in that state. In this
example, no-flows are interpreted as introduced in subsection 3.4. We use the
abbreviation $x_{1}[t]\not\rcurvearrowright_{3}y_{2}[t]\equiv x\neq y\ \wedge\
\pi_{1}[t](x)=\pi_{3}[t](x)\ \wedge\ \pi_{2}[t](y)=\pi_{3}[t](y)$, where
$\pi[t](x)$ denotes the _valuation of variable $x$ at time $t$ in $\pi$_.

To capture our intended interpretation for the no-flow predicate $\pi$ and
$\pi^{\prime}$ need to be universally quantified while $\pi^{\prime\prime}$
needs to be existentially quantified. The quantification over time admits
different interpretations. We can, for instance, force all traces of an
implementation to be synchronous concerning the states in that interface.
Then, state transitions are satisfied at the same time in all traces of an
implementation. This is the _strong no-flow_ interpretation over time.
Alternatively, we can require that for any arbitrary observation of a system
execution all valuations witnessing a no-flow requirement w.r.t. other
observations need to be in the same time point. In this case, state
transitions must be synchronous with respect to individual traces. This is the
_structure-aware no-flow_ interpretation over time. Finally, we may only
require that the witnesses are presented in some time which may differ for
each triple of traces. We refer to this interpretation as _unstructured no-
flow_.

######  Definition 4.25.

We define that _$x_{1}\not\rcurvearrowright_{3}y_{2}$ until it always holds
that $x_{1}\not\rcurvearrowright_{3}z_{2}$_ as:

$\displaystyle\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\equiv\ 0<t\
\wedge\ (\forall 0\leq t^{\prime}<t\
x_{1}[t^{\prime}]\not\rcurvearrowright_{3}y_{2}[t^{\prime}])\ \wedge(\forall
t\leq t^{\prime\prime}\
x_{1}[t^{\prime\prime}]\not\rcurvearrowright_{3}z_{2}[t^{\prime\prime}]).$

There are three plausible set semantics for $\mathbb{F}_{\mathcal{U}}$, which
differ in the position of $\exists t$:

Strong no-flow

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}=\\{T\ |\ \exists t\
\forall\pi_{1}\\!\in\\!T\ \forall\pi_{2}\\!\in\\!T\
\exists\pi_{3}\\!\in\\!T:\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\\}$;

Structure-aware no-flow

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}=\\{T\ |\
\forall\pi_{1}\\!\in\\!T\ \exists t\ \forall\pi_{2}\\!\in\\!T\
\exists\pi_{3}\\!\in\\!T:\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\\}$;

Unstructured no-flow

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}=\\{T\ |\
\forall\pi_{1}\\!\in\\!T\ \forall\pi_{2}\\!\in\\!T\ \exists\pi_{3}\\!\in\\!T\
\exists t:\phi_{\mathcal{U}}(t,x_{1},y_{2},z_{2},\pi_{3})\\}$.

Clearly,
$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}$.
The other direction does not hold. Hence these set semantics are not
equivalent.

######  Theorem 4.26.

$\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}\not\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}\not\subseteq\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}.$

######  Proof 4.27.

$T_{u}\in\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{u}$ but
$T_{u}\notin\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}$. And,
$T_{a}\in\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{a}$ but
$T_{a}\notin\llbracket\mathbb{F}_{\mathcal{U}}\rrbracket_{s}$.

| t=0 | t=1 | 1 < t
---|---|---|---
| x | y | z | x | y | z | x | y | z
$\pi_{1}$ | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0
$\pi_{2}$ | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0
$\pi_{3}$ | 0 | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0

Table 3: Set of traces $T_{u}$.

| t=0 | t=1 | 1 < t
---|---|---|---
| x | y | z | x | y | z | x | y | z
$\pi_{1}$ | 0 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0
$\pi_{2}$ | 0 | 0 | 0 | 1 | 1 | 0 | 0 | 0 | 0
$\pi_{3}$ | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 0
$\pi_{4}$ | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0

Table 4: Set of traces $T_{a}$.

Linear temporal logic [27] (LTL) cannot express the properties introduced in
Definition 4.25 [8, 7]. LTL extended with knowledge (linear time epistemic
logic [5]) under the synchronous perfect recall semantics can express the
strong no-flow interpretation of $\mathbb{F}_{\mathcal{U}}$ [5]. The
unstructured no-flow semantics can be specified in HyperLTL [7]. HyperLTL
extends LTL by allowing quantification over traces, which occur at the
beginning of the formula. Epistemic temporal logic and HyperLTL have
incomparable expressive power [5]. To the best of our knowledge, there is no
temporal formalism that supports the structure-aware semantics.

##  5 Related Work

Interface theories belong to the broader area of contract-based design [4, 3,
2, 10, 28]. The use of contracts to design systems was popularized by Bertrand
Meyer [26], following the earlier ideas introduced by Floyd and Hoare [18,
22]. Hoare logic allows to reason formally about refinement and composition
for sequential imperative programs. Other language-based techniques have been
proved useful to verify and enforce information flow policies [31]. Examples
range from type systems [19] to program analysis using program-dependency
graphs (PDGs) [21, 20]. These techniques are tailored for specific
implementation languages. In our approach we are we aim at working with
composition and refinement notions that are independent of the language
adopted for the implementations. Therefore, language oriented techniques are
not directly related to our work.

Interface automata [12] (IA), is a stateful interface language designed to
capture interfaces’ input/output (I/O) temporal aspect. IA allows the
specification of _input_ and _output_ actions through which a component can
interact with the environment, while _hidden_ actions represent the internal
transitions that cannot be observed by the environment. This formalism has
been later further enriched to include also extra functional requirements such
as resource [6], timing [15, 11] and security [24] requirements.

The work in [24] presents a variant of IA called _Interface for structure and
security_ (ISS) that enables the specification of two different kind of
actions: one type for actions related to low confidential information that are
accessible to all users and another type related to high confidential
information that are accessible to users with appropriate rights. In this
setting the authors present a bisimulation based notion of non-interference
(BNNI) that checks whether the system behaves in the same way when high
actions are performed or when they are considered hidden actions. In a recent
paper [23], the same authors notice ISS and BNNI may fail to detect an
information leakage and they propose an alternative refinement-based notion of
non-interference. Our approach is orthogonal to IA and their extensions: we do
not characterise the type of actions of each component, but only their
input/output ports defining explicitly the information flow relations among
them.

Closer to our approach is [13], which defines theories for both stateless and
deterministic stateful interfaces where the assumptions on the environment are
satisfiable predicates over input variables and the guarantees are predicates
over output variables. These theories support both stepwise-refinement and
independent implementation of components and they have proven to be very
successful to reason compositionally about trace properties [4]. We are not
aware of extensions that provide explicit support for security policies such
as information flow. Interface theories require input and output ports to be
disjoint, and so it cannot express properties that relate them. On the
contrary, our information flow interfaces, to ensure compositionality, require
a third relation (property) that specifies forbidden information flows for
which the component and the environment must share responsibility to enforce
them.

Our approach took inspiration from the work on _relational interfaces_ (RIs)
in [33]. RIs specify the legal inputs that the environment is allowed to
provide to the component and for each the legal input, what are the legal
outputs that the component can generate when provided with that input. A
contract in RIs is expressed as first-order logic (FOL) formulas that are
evaluated over individual traces. Hence, RIs can only relate input and output
values in a trace, and not across multiple traces. Our formalism can instead
specify information flow requirements that are related to sets of systems’
executions.

Temporal logics [27], like LTL or CTL* are used to specify trace properties of
reactive systems. HyperLTL and HyperCTL* [7] extend temporal logics by
introducing quantifiers over path variables. They allow relating multiple
executions and expressing for instance information-flow security properties
[8, 7]. Epistemic temporal logics [5] provide the knowledge connective with an
implicit quantification over traces. All these extensions reason about closed
systems while our approach allows compositional reasoning about open systems.

##  6 Conclusion

We propose a novel interface theory to specify information flow properties.
Our framework includes both _stateless_ and _stateful_ interfaces and supports
both incremental design and independent implementability. We also provide
three plausible trace semantics for the class of stateful interfaces with
boolean variables. We show that, while two of these semantics correspond to
temporal logics for specifying information-flow properties, for the third
(_structure-aware no-flow_), we do not know of any temporal formalism
supporting it.

As future work, we will explore how to extend our theory with sets of _must-
flows_ , i.e. support for modal specifications [29]. This will enable, for
example, to specify flows that a state $q$ must implement so that the system
can transition to a different state, which is useful to specify
declassification of information. Another direction is to investigate the
expressiveness of the _structure-aware no-flow_ trace semantics,
characterizing further the class of hyperproperties [8] that can be expressed
in our formalism.

## References

  * [1] Rajeev Alur, Thomas A Henzinger, Orna Kupferman, and Moshe Y Vardi.  Alternating refinement relations.  In International Conference on Concurrency Theory, pages 163–178. Springer, 1998.
  * [2] Sebastian S. Bauer, Alexandre David, Rolf Hennicker, Kim Guldstrand Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski.  Moving from specifications to contracts in component-based design.  In Proc. of FASE 2012: the 15th International Conference on Fundamental Approaches to Software Engineering, volume 7212 of Lecture Notes in Computer Science, pages 43–58. Springer, 2012.  doi:10.1007/978-3-642-28872-2.
  * [3] Albert Benveniste, Benoît Caillaud, Alberto Ferrari, Leonardo Mangeruca, Roberto Passerone, and Christos Sofronis.  Multiple viewpoint contract-based specification and design.  In Proc. of FMCO 2007: the 6th International Symposium on Formal Methods for Components and Objects, volume 5382 of Lecture Notes in Computer Science, pages 200–225. Springer, 2008.  doi:10.1007/978-3-540-92188-2\\_9.
  * [4] Albert Benveniste, Benoît Caillaud, Dejan Nickovic, Roberto Passerone, Jean-Baptiste Raclet, Philipp Reinkemeier, Alberto L. Sangiovanni-Vincentelli, Werner Damm, Thomas A. Henzinger, and Kim G. Larsen.  Contracts for system design.  Foundations and Trends in Electronic Design Automation, 12(2-3):124–400, 2018.  doi:10.1561/1000000053.
  * [5] Laura Bozzelli, Bastien Maubert, and Sophie Pinchinat.  Unifying hyper and epistemic temporal logics.  In International Conference on Foundations of Software Science and Computation Structures, pages 167–182. Springer, 2015.
  * [6] Arindam Chakrabarti, Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga.  Resource interfaces.  In Proc. of EMSOFT 2003: the Third International Conference on Embedded Software, volume 2855 of LNCS, pages 117–133. Springer, 2003\.  doi:10.1007/978-3-540-45212-6\\_9.
  * [7] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez.  Temporal logics for hyperproperties.  In Proc. of POST 2014: the Third International Conference on Principles of Security and Trust, volume 8414 of Lecture Notes in Computer Science, pages 265–284. Springer, 2014.  doi:10.1007/978-3-642-54792-8.
  * [8] Michael R. Clarkson and Fred B. Schneider.  Hyperproperties.  Journal of Computer Security, 18(6):1157–1210, 2010.  doi:10.3233/JCS-2009-0393.
  * [9] Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup.  Verifying hyperliveness.  In Proc. of CAV 2019: the 31st International Conference on Computer Aided Verification, volume 11561 of Lecture Notes in Computer Science, pages 121–139. Springer, 2019.  doi:10.1007/978-3-030-25540-4.
  * [10] Werner Damm, Hardi Hungar, Bernhard Josko, Thomas Peikenkamp, and Ingo Stierand.  Using contract-based component specifications for virtual integration testing and architecture design.  In Proc. of DATE 2011: Design, Automation and Test in Europe, pages 1023–1028. IEEE, 2011.  doi:10.1109/DATE.2011.5763167.
  * [11] Alexandre David, Kim G. Larsen, Axel Legay, Ulrik Nyman, and Andrzej Wasowski.  Timed I/O automata: a complete specification theory for real-time systems.  In Proc. of HSCC 2010: the 13th ACM International Conference on Hybrid Systems: Computation and Control, pages 91–100. ACM, 2010.
  * [12] Luca De Alfaro and Thomas A. Henzinger.  Interface automata.  In Proc. of the 8th European Software Engineering Conference held jointly with 9th ACM SIGSOFT International Symposium on Foundations of Software Engineering 2001, pages 109–120. ACM, 2001.
  * [13] Luca De Alfaro and Thomas A. Henzinger.  Interface theories for component-based design.  In International Workshop on Embedded Software, pages 148–165. Springer, 2001.
  * [14] Luca de Alfaro and Thomas A. Henzinger.  Interface-based design.  In Manfred Broy, Johannes Grünbauer, David Harel, and Tony Hoare, editors, Engineering Theories of Software Intensive Systems, pages 83–104, Dordrecht, 2005. Springer Netherlands.
  * [15] Luca de Alfaro, Thomas A. Henzinger, and Mariëlle Stoelinga.  Timed interfaces.  In Proc. of EMSOFT 2002: the Second International Conference on Embedded Software, volume 2491 of LNCS, pages 108–122. Springer, 2002\.  doi:10.1007/3-540-45828-X.
  * [16] Ronald Fagin, Yoram Moses, Joseph Y Halpern, and Moshe Y Vardi.  Reasoning about knowledge.  MIT press, 2003.
  * [17] Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah.  Model checking quantitative hyperproperties.  In Proc. of CAV 2018: the 30th International Conference on Computer Aided Verification, volume 10981 of Lecture Notes in Computer Science, pages 144–163. Springer, 2018.  doi:10.1007/978-3-319-96145-3.
  * [18] Robert W. Floyd.  Assigning meanings to programs.  Proceedings of Symposium on Applied Mathematics, 19:19–32, 1967\.
  * [19] Riccardo Focardi and Matteo Maffei.  Types for security protocols.  Formal Models and Techniques for Analyzing Security Protocols. Cryptology and Information Security Series, 5:143–181, 2011.
  * [20] Jürgen Graf, Martin Hecker, and Martin Mohr.  Using JOANA for information flow control in Java programs - a practical guide.  In Proceedings of the 6th Working Conference on Programming Languages (ATPS’13), Lecture Notes in Informatics (LNI) 215, pages 123–138. Springer Berlin / Heidelberg, February 2013.
  * [21] Christian Hammer and Gregor Snelting.  Flow-sensitive, context-sensitive, and object-sensitive information flow control based on program dependence graphs.  International Journal of Information Security, 8(6):399–422, 2009\.
  * [22] C. A. R. Hoare.  An axiomatic basis for computer programming.  Commun. ACM, 12(10):576–580, October 1969.  URL: http://doi.acm.org/10.1145/363235.363259, doi:10.1145/363235.363259.
  * [23] M. Lee and P. R. D’Argenio.  A refinement based notion of non-interference for interface automata: Compositionality, decidability and synthesis.  In 2010 XXIX International Conference of the Chilean Computer Science Society, pages 280–289, Nov 2010.  doi:10.1109/SCCC.2010.14.
  * [24] Matias Lee and Pedro R. D’Argenio.  Describing secure interfaces with interface automata.  In Proceedings of the 7th International Workshop on Formal Engineering approaches to Software Components and Architectures (FESCA 2010), volume 264(1) of Electronic Notes in Theoretical Computer Science, pages 107 – 123, 2010.  doi:https://doi.org/10.1016/j.entcs.2010.07.008.
  * [25] Heiko Mantel.  On the composition of secure systems.  In Proc. of 2002 IEEE Symposium on Security and Privacy, pages 88–101. IEEE Computer Society, 2002.  doi:10.1109/SECPRI.2002.1004364.
  * [26] Bertrand Meyer.  Applying ‘design by contract’.  Computer, 25(10):40–51, 1992.
  * [27] Amir Pnueli.  The temporal logic of programs.  In Proc. of FOCS77: the 18th Annual Symposium on Foundations of Computer Science, pages 46–57. IEEE Computer Society, 1977.  doi:10.1109/SFCS.1977.32.
  * [28] S. Quinton and S. Graf.  Contract-based verification of hierarchical systems of components.  In 2008 Sixth IEEE International Conference on Software Engineering and Formal Methods, pages 377–381. IEEE Computer Society, Nov 2008\.  doi:10.1109/SEFM.2008.28.
  * [29] Jean-Baptiste Raclet, Eric Badouel, Albert Benveniste, Benoît Caillaud, Axel Legay, and Roberto Passerone.  A modal interface theory for component-based design.  Fundamenta Informaticae, 108(1-2):119–149, 2011.
  * [30] Denise Ratasich, Faiq Khalid, Florian Geissler, Radu Grosu, Muhammad Shafique, and Ezio Bartocci.  A roadmap toward the resilient internet of things for cyber-physical systems.  IEEE Access, 7:13260–13283, 2019.  doi:10.1109/ACCESS.2019.2891969.
  * [31] Andrei Sabelfeld and Andrew C Myers.  Language-based information-flow security.  IEEE Journal on selected areas in communications, 21(1):5–19, 2003\.
  * [32] Fred B. Schneider.  Enforceable security policies.  ACM Transactions on Information and System Security, 3(1):30–50, 2000.  doi:10.1145/353323.353382.
  * [33] Stavros Tripakis, Ben Lickly, Thomas A. Henzinger, and Edward A. Lee.  A theory of synchronous relational interfaces.  ACM Transactions on Programming Languages and Systems (TOPLAS), 33(4):14, 2011.

##  Appendix A Stateless Interfaces: Proofs and Auxiliary Results

######  Lemma A.1.

If $F\sim G$ and $F\otimes G\sim I$, then their output variables are pairwise
disjoint, in particular, $Y_{F}\cap Y_{G}=\emptyset$, $Y_{F}\cap
Y_{I}=\emptyset$, and $Y_{G}\cap Y_{I}=\emptyset$.

######  Proof A.2.

Trivial.

######  Lemma A.3.

If $F_{1}\sim F_{2}$ and ${F_{1}\otimes F_{2}\sim F_{3}}$, then:
$\mathcal{P}^{\mathcal{A}_{F_{1}\otimes F_{2}},\mathcal{G}_{F_{1}\otimes
F_{2}}}\subseteq\mathcal{P}^{\mathcal{A}_{F_{1}\otimes
F_{2},F_{3}},\mathcal{G}_{F_{1}\otimes F_{2},F_{3}}}$.

######  Proof A.4.

Follows from $\overline{\mathcal{A}}_{F_{1}\otimes
F_{2},F_{3}}\subseteq\overline{\mathcal{A}}_{F_{1}\otimes F_{2}}$ and
$\overline{\mathcal{G}}_{F_{1}\otimes
F_{2},F_{3}}\subseteq\overline{\mathcal{G}}_{F_{1}\otimes F_{2}}$.

From now on, $F=(X,Y,\mathcal{A},\mathcal{G},\mathcal{P})$ is an interface,
and $f=(X,Y,\mathcal{M})$ and $f_{\mathcal{E}}=(Y,X,\mathcal{E})$ are
components.

###  A.1 Proof for Proposition 3.5

_Let $F$ be a well-formed interface. For all components $f=(X,Y,\mathcal{M})$
and $f_{\mathcal{E}}=(Y,X,\mathcal{E})$: if $f\models F$ and
$f_{\mathcal{E}}\models F$, then
$(\mathcal{M}\cup\mathcal{E})^{*}\cap\mathcal{P}=\emptyset$._

######  Proof A.5.

Consider an arbitrary interface $F$. Assume that:  (a1) $F$is a well-formed
interface,  (a2) $f\models F$, and  (a3) $f_{\mathcal{E}}\models F$.

$\displaystyle(z,z^{\prime})\in(\mathcal{M}\cup\mathcal{E})^{*}\ \
\overset{\text{denesting rule}}{\Leftrightarrow}$
$\displaystyle(z,z^{\prime})\in\mathcal{E}^{*}\circ(\mathcal{M}\circ\mathcal{E}^{*})^{*}\overset{\text{flows
are closed for *}}{\Leftrightarrow}$
$\displaystyle(z,z^{\prime})\in(\text{Id}_{Z}\cup\mathcal{E})\circ(\mathcal{M}\circ\mathcal{E})^{*}\circ(\text{Id}_{Y}\cup\mathcal{M})\underset{\ref{thm:well_formed:a2}}{\overset{\ref{thm:well_formed:a1}}{\Rightarrow}}$
$\displaystyle(z,z^{\prime})\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{*}\circ(\text{Id}_{Y}\cup\overline{\mathcal{G}})\Rightarrow$
$\displaystyle(z,z^{\prime})\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{*}\circ\overline{\mathcal{G}}\
\text{ or }\ (z,z^{\prime})\in Z\times X\ \
\overset{\ref{thm:well_formed:a}}{\Rightarrow}$
$\displaystyle(z,z^{\prime})\notin\mathcal{P}.$

Hence, $(\mathcal{M}\cup\mathcal{E})^{*}\cap\mathcal{P}=\emptyset$.

###  A.2 Properties of Composite Flows

Let $F$ and $F^{\prime}$ be interfaces.

######  Proposition A.6.

The definition of composite flows can be rewritten as follows:

$\displaystyle\overline{\mathcal{G}}_{F,F^{\prime}}=\overline{\mathcal{G}}\cup\overline{\mathcal{G}}^{\prime}\cup(\overline{\mathcal{G}}\circ\overline{\mathcal{G}}^{\prime})^{+}\cup(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+}\cup((\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+}\circ\overline{\mathcal{G}}^{\prime})\cup((\overline{\mathcal{G}}\circ\overline{\mathcal{G}}^{\prime})^{+}\circ\overline{\mathcal{G}}).$

######  Proof A.7.

$\displaystyle\overline{\mathcal{G}}_{F,F^{\prime}}\overset{\text{def.
}\ref{def:compos:flows}}{=}$
$\displaystyle(\text{Id}_{Z^{\prime}}\cup\overline{\mathcal{G}})\circ(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{*}\circ(\text{Id}_{Y}\cup\overline{\mathcal{G}}^{\prime})=$
$\displaystyle\overline{\mathcal{G}}^{\prime}\cup(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+}\cup((\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+}\circ\overline{\mathcal{G}}^{\prime})\
\cup\overline{\mathcal{G}}\cup(\overline{\mathcal{G}}\circ(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+})\cup(\overline{\mathcal{G}}\circ(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{*}\circ\overline{\mathcal{G}}^{\prime})=$
$\displaystyle\overline{\mathcal{G}}^{\prime}\cup\overline{\mathcal{G}}\cup(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+}\cup(\overline{\mathcal{G}}\circ\overline{\mathcal{G}}^{\prime})^{+}\
\cup((\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{+}\circ\overline{\mathcal{G}}^{\prime})\cup((\overline{\mathcal{G}}\circ\overline{\mathcal{G}}^{\prime})^{+}\circ\overline{\mathcal{G}}).$

From the previous proposition we can derive that composite flows are
commutative.

######  Proposition A.8.

$\overline{\mathcal{G}}_{F,F^{\prime}}=\overline{\mathcal{G}}_{F^{\prime},F}.$

######  Proof A.9.

Follows directly from Proposition A.6.

######  Proposition A.10.

$\overline{\mathcal{G}}_{F,F^{\prime}}$ is a reflexive relation in
$Y_{F,F^{\prime}}$.

######  Proof A.11.

By definition of interface $\overline{\mathcal{G}}$ and
$\overline{\mathcal{G}}^{\prime}$ are reflexive relations. Moreover, we can
derive that
$\text{Id}_{Y_{F,F^{\prime}}}\subseteq\overline{\mathcal{G}}\cup\overline{\mathcal{G}}^{\prime}$.
Then, by definition of composite flows, it follows that,
$\overline{\mathcal{G}}\cup\overline{\mathcal{G}}^{\prime}\subseteq\overline{\mathcal{G}}_{F,F^{\prime}}$,
and so
$\text{Id}_{Y_{F,F^{\prime}}}\subseteq\overline{\mathcal{G}}_{F,F^{\prime}}$.
Hence $\overline{\mathcal{G}}_{F,F^{\prime}}$ is a reflexive relation in
$Y_{F,F^{\prime}}$.

In the lemma bellow we prove some properties of composite flows that are used
in the proofs of important results later. The first property tell us that,
when the set of output ports is disjoint, then the only way to flow to a given
output variable is through the flows allowed by that variable’s interface.
This property is very important to prove results related to the assumptions
derived for the composition, which are defined later. The second property tell
us that considering more interfaces can only increase the possible flows.
Finally, the third property states that our operator always compute the same
set of possible flows between multiple interfaces independently of the order
in which each interface is considered. This last property tell us that the
composition’s guarantee is associative.

######  Lemma A.12.

Let $F$, $F^{\prime}$ and $F^{\prime\prime}$ be interfaces.

  1. (a)

Suffix: If $(z,y)\in\overline{\mathcal{G}}_{F,F^{\prime}}$ and $y\in
Y\setminus Y^{\prime}$, then

     * •

$(z,y)\in\overline{\mathcal{G}}\cup(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{G}})$
and

     * •

if $(z,y)\notin\overline{\mathcal{G}}$, then for all
$(z,s)\in\overline{\mathcal{G}}_{F,F^{\prime}}$ and
$(s,y)\in\overline{\mathcal{G}}$, we have $s\in Y^{\prime}$.

  2. (b)

Monotonicity:
$\overline{\mathcal{G}}_{F,F^{\prime}}\subseteq\overline{\mathcal{G}}_{F,F^{\prime}\otimes
F^{\prime\prime}}$.

  3. (c)

Associativity: $\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}=\overline{\mathcal{G}}_{F,F^{\prime}\otimes
F^{\prime\prime}}$.

######  Proof A.13.

Consider arbitrary interfaces $F$, $F^{\prime}$ and $F^{\prime\prime}$.

  1. (a)

Assume that $(z,y)\in\overline{\mathcal{G}}_{F,F^{\prime}}$ with $y\in
Y\setminus Y^{\prime}$.

$\displaystyle(z,y)\in$ $\displaystyle\ \
\overline{\mathcal{G}}_{F,F^{\prime}}\ \ \underset{y\in Y\setminus
Y^{\prime}}{\overset{\text{prop.
}\ref{prop:composflow:alt}}{\Leftrightarrow}}$ $\displaystyle(\star)(z,y)\in$
$\displaystyle\ \
\overline{\mathcal{G}}\cup\big{(}(\overline{\mathcal{G}}^{\prime}\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{G}}^{\prime})^{*}\circ\overline{\mathcal{G}})\cup(\overline{\mathcal{G}}\circ\overline{\mathcal{G}}^{\prime})^{+}\circ\overline{\mathcal{G}}\big{)}\overset{\text{prop.
}\ref{prop:composflow:alt}}{\Rightarrow}$ $\displaystyle(z,y)\in$
$\displaystyle\ \
\overline{\mathcal{G}}\cup(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}).$

By $(\star)$, it follows that, if $(z,y)\notin\overline{\mathcal{G}}$, then
$(z,y)=(z,s)\circ(s,y)$ with $(z,s)\in\overline{\mathcal{G}}_{F,F^{\prime}}$,
$(s,y)\in\overline{\mathcal{G}}$ and $s\in Y^{\prime}$.

  2. (b)

$\displaystyle(z,y)\in$ $\displaystyle\ \
\overline{\mathcal{G}}_{F,F^{\prime}}\ \ \overset{\text{def.
}\ref{def:compos:flows}}{\Leftrightarrow}$ $\displaystyle(z,y)\in$
$\displaystyle\ \
(\text{Id}_{Z^{\prime}}\cup\overline{\mathcal{G}})\circ(\overline{\mathcal{G}}^{\prime}\circ\overline{\mathcal{G}})^{*}\circ(\text{Id}_{Y}\cup\overline{\mathcal{G}}^{\prime})\
\ \underset{Z^{\prime}\subseteq
Z_{F^{\prime},F^{\prime\prime}}}{\overset{\overline{\mathcal{G}}^{\prime}\subseteq\overline{\mathcal{G}}_{F^{\prime}\otimes
F^{\prime\prime}}}{\Rightarrow}}$ $\displaystyle(z,y)\in$ $\displaystyle\ \
(\text{Id}_{Z_{F^{\prime},F^{\prime\prime}}}\cup\overline{\mathcal{G}})\circ(\overline{\mathcal{G}}_{F^{\prime}\otimes
F^{\prime\prime}}\circ\overline{\mathcal{G}})^{*}\circ(\text{Id}_{Y}\cup\overline{\mathcal{G}}_{F^{\prime}\otimes
F^{\prime\prime}})\overset{\text{def.
}\ref{def:compos:flows}}{\Leftrightarrow}$ $\displaystyle(z,y)\in$
$\displaystyle\ \ \overline{\mathcal{G}}_{F,F^{\prime}\otimes
F^{\prime\prime}}.$

  3. (c)

We start by proving that: $\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}\subseteq\overline{\mathcal{G}}_{F,F^{\prime}\otimes
F^{\prime\prime}}$.

Consider an arbitrary $(z,y)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$. We consider first the case that $y\in
Y^{\prime\prime}$. Then, by definition of composite flows, we can derive that
what we want to prove is equivalent to the following statement over
(alternated) paths, for all $n\in\mathbb{N}$, $0\leq i\leq n/2$ and $0\leq
j\leq m/2$:

$\displaystyle\text{ if }(z,y)=$ then there exists $\displaystyle\qquad\ \
\text{there exists }0\leq(k_{j}+r_{j})\leq n\text{ s.t.\ }$

We proceed by induction on $n$.

Base Case ($n=1$):

Consider arbitrary $(z,y)\in\overline{\mathcal{G}}^{\prime}$, then, by
definition of composite flows,
$(z,y)\in\overline{\mathcal{G}}_{F^{\prime}\otimes F^{\prime\prime}}$. So,
$m=1$, $k_{1}=1$ and $r_{1}=0$.

Inductive case:

Assume as induction hypothesis that our property holds for paths of size $n$.
Assume that there exists  such that for all $0\leq i\leq n/2$:

$\displaystyle(\star)$ $\displaystyle(z,y)=$

By induction hypothesis we know that, $0\leq j\leq m_{n}/2$:

$\displaystyle\text{there exists }(s,y)=$ $\displaystyle\qquad\text{there
exists }0\leq(k_{j}+r_{j})\leq n\text{ s.t.\ }$

Case $n+1$ is odd:

Then, by $(\star)$,  and .

If $m_{n}$ is even, then . So, the property holds for $n+1$ with $m_{n+1}=m+1$
and $p_{m_{n+1}}=p_{n+1}$.

Otherwise, if $m_{n}$ is odd, then  with , for some $k$ and $r$. Additionally,
we know that .

Case :

It holds with $m_{n+1}=m+1$ and .

Case :

It holds with $m_{n+1}=m$ and .

Case $n+1$ is even:

Then, . Follows from an analogous reasoning.

We can prove analogously that the property holds for arbitrary
$(z,y)\in\overline{\mathcal{G}}_{F\otimes F^{\prime},F^{\prime\prime}}$ with
$y\in Y\cup Y^{\prime}$.

We prove analogously that $\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}\supseteq\overline{\mathcal{G}}_{F,F^{\prime}\otimes
F^{\prime\prime}}$.

###  A.3 Properties of Propagated Assumptions

Let $F$, $F^{\prime}$ and $F^{\prime\prime}$ be interfaces.

######  Proposition A.61.

If $F\sim F^{\prime}$, then $\hat{\mathcal{A}}_{F,F^{\prime}}$ is an
irreflexive relation.

######  Proof A.62.

Consider two compatible interfaces $F$ and $F^{\prime}$. Assume towards a
contradiction that there exists $(z,z)\in\hat{\mathcal{A}}_{F\rightarrow
F^{\prime}}$. By definition of propagated assumptions:

$\exists s\in X\cap Y^{\prime}\text{ s.t.\ }(z,s)\in\mathcal{A}\text{ and
}(z,s)\in\overline{\mathcal{G}}_{F,F^{\prime}}.$

Then, by $s\in Y^{\prime}$, $(z,s)\in\mathcal{A}\cap(Z_{F,F^{\prime}}\times
Y_{F,F^{\prime}})$. So, by $F\sim F^{\prime}$, it follows that
$(z,s)\notin\overline{\mathcal{G}}_{F,F^{\prime}}$.

We can prove analogously that
$(z,z)\notin\hat{\mathcal{A}}_{F^{\prime}\rightarrow F}$.

######  Lemma A.63.

Let $F_{1}$, $F_{1}^{\prime}$ and $F_{2}$ be interfaces. If
$F_{1}^{\prime}\preceq F_{1}$, then
$\hat{\mathcal{A}}_{F_{1}^{\prime},F_{2}}\subseteq\hat{\mathcal{A}}_{F_{1},F_{2}}$.

######  Proof A.64.

Assume that $F_{1}^{\prime}\preceq F_{1}$. Consider arbitrary
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F_{1}^{\prime}\rightarrow F_{2}}$. Then,
by definition of propagated assumptions, $\exists s\in X_{1}^{\prime}\cap
Y_{2}\text{ s.t.\ }(z,s)\in\mathcal{A}_{1}^{\prime}\text{ and
}(z^{\prime},s)\in\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}.$

By $F_{1}^{\prime}\preceq F_{1}$, we know that
$\mathcal{A}_{1}^{\prime}\subseteq\mathcal{A}_{1}$ and
$\overline{\mathcal{G}}_{1}^{\prime}\subseteq\overline{\mathcal{G}}_{1}$.
Then, it follows by definition of composite guarantees that
$\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}\subseteq\overline{\mathcal{G}}_{F_{1},F_{2}}$
and so $(z^{\prime},s)\in\overline{\mathcal{G}}_{F_{1},F_{2}}$. By
$(z,s)\in\mathcal{A}^{\prime}_{1}$ and
$\mathcal{A}_{1}^{\prime}\subseteq\mathcal{A}_{1}$, we have
$(z,s)\in\mathcal{A}_{1}$. So, by definition of propagated assumptions,
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F_{1},F_{2}}$. So,
$\hat{\mathcal{A}}_{F_{1}^{\prime}\rightarrow
F_{2}}\subseteq\hat{\mathcal{A}}_{F_{1},F_{2}}$.

We can prove analogously that $\hat{\mathcal{A}}_{F_{2}\rightarrow
F_{1}^{\prime}}\subseteq\hat{\mathcal{A}}_{F_{1},F_{2}}$.

######  Lemma A.65.

Let $F$, $F^{\prime}$ and $F^{\prime\prime}$ be interfaces, such that $F\sim
F^{\prime}$ and $F\otimes F^{\prime}\sim F^{\prime\prime}$.

  1. (1)

If $(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime}\rightarrow
F^{\prime\prime}}$, then $(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes
F^{\prime}\rightarrow F^{\prime\prime}}$.

  2. (2)

If $(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime\prime}\rightarrow
F^{\prime}}$, then
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime\prime}\rightarrow F\otimes
F^{\prime}}$.

  3. (3)

If $(z,z^{\prime})\in\hat{\mathcal{A}}_{F,F^{\prime}\otimes
F^{\prime\prime}}$, then $(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes
F^{\prime},F^{\prime\prime}}\cup\hat{\mathcal{A}}_{F,F^{\prime}}$.

######  Proof A.66.

Consider arbitrary interfaces $F,\ F^{\prime}\text{ and }F^{\prime\prime}$.
Assume that:  (a1) $F\sim F^{\prime}$; and  (a2) $F\otimes F^{\prime}\sim
F^{\prime\prime}$.

  1. _(1)_

Assume that $(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime}\rightarrow
F^{\prime\prime}}$. By definition of propagated assumptions (def. 3.11), there
exists $s\in X^{\prime}\cap Y^{\prime\prime}\text{ s.t.\
}(z,s)\in\mathcal{A}^{\prime}\text{ and
}(z^{\prime},s)\in\overline{\mathcal{G}}_{F^{\prime},F^{\prime\prime}}.$

By (a2), $s^{\prime}\notin Y_{F,F^{\prime}}$ and, by definition of composition
(def. 3.15), $(z,s)\in\mathcal{A}_{F\otimes F^{\prime}}$. By monotonicity of
composite flows (lemma A.12(b)), it follows that
$\overline{\mathcal{G}}_{F^{\prime},F^{\prime\prime}}\subseteq\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$. So,
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$, and by definition of propagated assumptions,
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes F^{\prime}\rightarrow
F^{\prime\prime}}$.

  2. _(2)_

Assume that $(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime\prime}\rightarrow
F^{\prime}}$. By definition of propagated assumptions (def. 3.11), there
exists $s\in X^{\prime\prime}\cap Y^{\prime}\text{ s.t.\
}(z,s)\in\mathcal{A}^{\prime\prime}\text{ and
}(z^{\prime},s)\in\overline{\mathcal{G}}_{F^{\prime},F^{\prime\prime}}.$ By
monotonicity of composite flows (Lemma A.12(b)), it follows that
$\overline{\mathcal{G}}_{F^{\prime},F^{\prime\prime}}\subseteq\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$, so
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F^{\prime\prime},F\otimes
F^{\prime}}$. Then, by $(z,s)\in\mathcal{A}^{\prime\prime}$, it follows that
$\hat{\mathcal{A}}_{F^{\prime\prime}\rightarrow F\otimes F^{\prime}}$.

  3. _(3)_

Assume that $(z,z^{\prime})\in\hat{\mathcal{A}}_{F,F^{\prime}\otimes
F^{\prime\prime}}$. We want to prove that
${(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes
F^{\prime},F^{\prime\prime}}\cup\hat{\mathcal{A}}_{F,F^{\prime}}}$.

Case $(z,z^{\prime})\in\hat{\mathcal{A}}_{F\rightarrow F^{\prime}\otimes
F^{\prime\prime}}$:

By definition of propagated assumptions (def. 3.11), there exists $s\in X\cap
Y_{F^{\prime}\otimes F^{\prime\prime}}\text{ s.t.\ }(z,s)\in\mathcal{A}\text{
and }(z^{\prime},s)\in\overline{\mathcal{G}}_{F,F^{\prime}\otimes
F^{\prime\prime}}.$ By associativity of composite flows (Lemma A.12(c)),
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$. We proceed by cases on $s\in
Y_{F^{\prime}\otimes F^{\prime\prime}}$.

Case $s\in Y^{\prime}$:

By definition of composition, $s\in Y_{F\otimes F^{\prime}}$. By suffix
property of composite flows (Lemma A.12(a)) and
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$:
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime}}\cup(\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}\circ\overline{\mathcal{G}}_{F\otimes
F^{\prime}}).$

Consider the case that $(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime}}$. Then, by $(z,s)\in\mathcal{A}$, it follows
${(z,z^{\prime})\in\hat{\mathcal{A}}_{F,F^{\prime}}}$.

Otherwise, $(z^{\prime},s)\in(\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}\circ\overline{\mathcal{G}}_{F\otimes
F^{\prime}}).$ Consider arbitrary
$(z^{\prime},s^{\prime})\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$ and $(s^{\prime},s)\in\leavevmode\nobreak\
\overline{\mathcal{G}}_{F\otimes F^{\prime}}$. Then, by Lemma A.12(a),
$s^{\prime}\in Y^{\prime\prime}$, and by (a2), $s^{\prime}\notin
Y_{F,F^{\prime}}$. Then, it must be the case that $s^{\prime}\in
X_{F,F^{\prime}}$. By $(s^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime}}$ and $(z,s)\in\mathcal{A}$, it follows that
$(z,s^{\prime})\in\hat{\mathcal{A}}_{F\rightarrow F^{\prime}}$. Then, by
definition of composition and $s^{\prime}\in X_{F\otimes F^{\prime}}$,
$(z,s^{\prime})\in\mathcal{A}_{F\otimes F^{\prime}}$. Again, by definition of
propagated assumptions,
$(z^{\prime},s^{\prime})\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$ and $s^{\prime}\in X_{F\otimes F^{\prime}}\cap
Y^{\prime\prime}$, it follows that
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes F^{\prime}\rightarrow
F^{\prime\prime}}$.

Case $s\in Y^{\prime\prime}$:

By (a2), $s\notin Y_{F\otimes F^{\prime}}$. Then, by definition of
composition, ${(z,s)\in\mathcal{A}_{F\otimes F^{\prime}}}$. So, by
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$ and definition of propagated assumptions,
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes F^{\prime}\rightarrow
F^{\prime\prime}}$.

Case $(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime}\otimes
F^{\prime\prime}\rightarrow F}$:

By definition of propagated assumptions (def. 3.11), there exists $s\in
X_{F^{\prime}\otimes F^{\prime\prime}}\cap Y$ s.t.
$(z,s)\in\mathcal{A}_{F^{\prime}\otimes F^{\prime\prime}}\text{ and
}(z^{\prime},s)\in\overline{\mathcal{G}}_{F^{\prime}\otimes
F^{\prime\prime},F}.$ By associativity of composite flows (Lemma A.12(c)) and
(a1), $(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$. We proceed now by cases on
$(z,s)\in\mathcal{A}_{F^{\prime}\otimes F^{\prime\prime}}$.

Case $(z,s)\in\mathcal{A}^{\prime}$:

By $s\in Y$ and definition of composition, $s\in Y_{F,F^{\prime}}$. Then, by
suffix property of composite flows (Lemma A.12(a)),
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime}}\cup(\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}\circ\overline{\mathcal{G}}_{F\otimes
F^{\prime}}).$ The rest is analogous to the case
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F\rightarrow F^{\prime}\otimes
F^{\prime\prime}}$ with $s\in Y^{\prime}$.

Case $(z,s)\in\mathcal{A}^{\prime\prime}$:

By $(z^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes
F^{\prime},F^{\prime\prime}}$, then
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F^{\prime\prime}\rightarrow F\otimes
F^{\prime}}$.

Case $(z,s)\in\hat{\mathcal{A}}_{F^{\prime},F^{\prime\prime}}$:

By previous lemmas A.65(1) and A.65(2), $(z,s)\in\hat{\mathcal{A}}_{F\otimes
F^{\prime},F^{\prime\prime}}$. Then, by
$(z^{\prime},s)\in\overline{\mathcal{G}}_{F^{\prime}\otimes
F^{\prime\prime},F}$ and definition of propagated assumptions,
$(z,z^{\prime})\in\hat{\mathcal{A}}_{F\otimes F^{\prime},F^{\prime\prime}}$.

###  A.4 Proof for Proposition 3.20

_Let $F$ and $F^{\prime}$ be interfaces. $F\sim F^{\prime}$ iff
$F^{\prime}\sim F$, and $F\otimes F^{\prime}=F^{\prime}\otimes F$._

######  Proof A.67.

By commutativity of union and intersection of sets:

  * •

$\mathcal{G}_{F,F^{\prime}}=Y\cup Y^{\prime}=Y^{\prime}\cup
Y=\mathcal{G}_{F^{\prime},F}$;

  * •

$X_{F,F^{\prime}}=(X\cup X^{\prime})\setminus Y_{F,F^{\prime}}=(X^{\prime}\cup
X)\setminus Y_{F^{\prime},F}=X_{F^{\prime},F}$;

  * •

$\hat{\mathcal{A}}_{F,F^{\prime}}=\hat{\mathcal{A}}_{F\rightarrow
F^{\prime}}\cup\hat{\mathcal{A}}_{F^{\prime}\rightarrow
F}=\hat{\mathcal{A}}_{F^{\prime}\rightarrow
F}\cup\hat{\mathcal{A}}_{F\rightarrow
F^{\prime}}=\hat{\mathcal{A}}_{F^{\prime},F}$;

  * •

$\mathcal{A}_{F,F^{\prime}}=\mathcal{A}\cup\mathcal{A}^{\prime}\cup\hat{\mathcal{A}}_{F,F^{\prime}}\cap(Z_{F,F^{\prime}}\times
X_{F,F^{\prime}})=$

$\mathcal{A}^{\prime}\cup\mathcal{A}\cup\hat{\mathcal{A}}_{F^{\prime},F}\cap(Z_{F^{\prime},F}\times
X_{F^{\prime},F})=\mathcal{A}_{F^{\prime},F}$.

  * •

By Proposition A.8,
$\overline{\mathcal{G}}_{F,F^{\prime}}=\overline{\mathcal{G}}_{F^{\prime},F}$.

  * •

$\mathcal{P}_{F,F^{\prime}}=\mathcal{P}\cup\mathcal{P}^{\prime}\cup\mathcal{P}^{\mathcal{A}_{F,F^{\prime}},\mathcal{G}_{F,F^{\prime}}}=\mathcal{P}^{\prime}\cup\mathcal{P}\cup\mathcal{P}^{\mathcal{A}_{F^{\prime},F},\mathcal{G}_{F^{\prime},F}}=\mathcal{P}_{F^{\prime},F}$.

Thus, $F\otimes F^{\prime}=F^{\prime}\otimes F$.

Additionally, we can prove analogously that $F\sim F^{\prime}$ iff
$((\mathcal{A}^{\prime}\cup\mathcal{A})\cap(Z_{F^{\prime},F}\times
Y_{F^{\prime},F}))\subseteq\mathcal{G}_{F^{\prime},F}$. So, $F\sim F^{\prime}$
iff $F\sim F^{\prime}$.

###  A.5 Proof for Theorem 3.19

_Let $F$ and $F^{\prime}$ be well-formed interfaces. If $F\sim F^{\prime}$,
then $F\otimes F^{\prime}$ is a well-formed interface._

######  Proof A.68.

Consider arbitrary well-formed interfaces $F$ and $F^{\prime}$. Assume that
$F\sim F^{\prime}$.

We start by proving that each relation in the tuple is a no-flow.

By definition of no-flow relation, we need to prove that they are all
irreflexive relations. By definition of interface and Proposition A.61,
$\mathcal{A}_{F,F^{\prime}}$ is an irreflexive relation. By Proposition A.10,
$\overline{\mathcal{G}}_{F,F^{\prime}}$ is a reflexive relation, and so
$\mathcal{G}_{F,F^{\prime}}$ is an irreflexive relation. Finally, by
$\mathcal{P}^{\mathcal{A}_{F,F^{\prime}},\mathcal{G}_{F,F^{\prime}}}\subseteq\mathcal{G}_{F,F^{\prime}}$
and definition of interface, $\mathcal{P}_{F,F^{\prime}}$ is irreflexive, as
well.

We prove now that it satisfies the well-formed property:

$(\text{Id}_{Y_{F,F^{\prime}}}\cup\overline{\mathcal{A}}_{F,F^{\prime}})\circ(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{A}}_{F,F^{\prime}})^{*}\circ\overline{\mathcal{G}}_{F,F^{\prime}}\cap\overline{\mathcal{P}}_{F,F^{\prime}}=\emptyset.$

Consider arbitrary
$(z,z^{\prime})\in(\text{Id}_{Y_{F,F^{\prime}}}\cup\overline{\mathcal{A}}_{F,F^{\prime}})\circ(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{A}}_{F,F^{\prime}})^{*}\circ\overline{\mathcal{G}}_{F,F^{\prime}}$.
Then, $z^{\prime}\in Y_{F,F^{\prime}}$. By definition of derived properties,
$(z,z^{\prime})\notin\mathcal{P}^{\mathcal{A}_{F,F^{\prime}},\mathcal{G}_{F,F^{\prime}}}$.
So, we are missing to prove that
$(z,z^{\prime})\notin\mathcal{P}\cup\mathcal{P}^{\prime}$.

Lets consider the case that $z^{\prime}\in Y$. Then, by $F\sim F^{\prime}$,
$z^{\prime}\notin Y^{\prime}$. Thus, $(z,z^{\prime})\notin Z^{\prime}\times
Y^{\prime}$ and, by definition of interface,
$(z,z^{\prime})\notin\mathcal{P}^{\prime}$. Moreover, by Lemma A.69 and $F\sim
F$,
$(z,z^{\prime})\in((\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{*}\circ\overline{\mathcal{G}})$.
Hence, by $F$ being well-formed, $(z,z^{\prime})\notin\mathcal{P}$, as well.

The case for $z^{\prime}\in Y^{\prime}$ is analogous.

In the lemmas below we prove that any alternated path in
$\overline{\mathcal{A}}_{F,F^{\prime}}$ and
$\overline{\mathcal{G}}_{F,F^{\prime}}$ from a variable of $F$ or $F^{\prime}$
to an output variable of the same interface can be translated to a path using
only the complement of that interface’s assumptions and guarantees.

######  Lemma A.69.

Let $F$ and $F^{\prime}$ be interfaces s.t. $F\sim F^{\prime}$, and
$(z,z^{\prime})\in Z\times Y$.

If
$(z,z^{\prime})\in(\text{Id}_{Z_{F,F^{\prime}}}\cup\overline{\mathcal{A}}_{F,F^{\prime}})\circ(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{A}}_{F,F^{\prime}})^{*}\circ\overline{\mathcal{G}}_{F,F^{\prime}}$,
then
$(z,z^{\prime})\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{*}\circ\overline{\mathcal{G}}.$

######  Proof A.70.

Consider arbitrary interfaces $F$ and $F^{\prime}$ and assume that $F\sim
F^{\prime}$. Additionally, consider arbitrary $(z,z^{\prime})\in Z\times Y$.
We prove by induction that, for all $n\in\mathbb{N}$:

if
$\displaystyle(z,z^{\prime})\in(\text{Id}_{Z_{F,F^{\prime}}}\cup\overline{\mathcal{A}}_{F,F^{\prime}})\circ(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{A}}_{F,F^{\prime}})^{n}\circ\overline{\mathcal{G}}_{F,F^{\prime}},$
then
$\displaystyle(z,z^{\prime})\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{n}\circ\overline{\mathcal{G}}.$

Base case $n=0$: It holds by Lemma A.71, proved below.

Induction step: Assume by induction hypothesis (IH) that the statement holds
for $n$.

Consider arbitrary:
$(z,z^{\prime})\in(\text{Id}_{Z_{F,F^{\prime}}}\cup\overline{\mathcal{A}}_{F,F^{\prime}})\circ(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{A}}_{F,F^{\prime}})^{n+1}\circ\overline{\mathcal{G}}_{F,F^{\prime}}$.
Then, by application of the induction hypothesis:
$(z,z^{\prime})\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{n}\circ\overline{\mathcal{G}}\circ\overline{\mathcal{A}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}_{F,F^{\prime}}$.

Consider arbitrary
$(z,s)\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{n}\circ\overline{\mathcal{G}}$,
$(s,s^{\prime})\in\overline{\mathcal{A}}_{F,F^{\prime}}$ and
$(s^{\prime},z^{\prime})\in\overline{\mathcal{G}}_{F,F^{\prime}}$. Then,
$(s,z^{\prime})\in Z\times Y$ and, by Lemma A.71,
$(s,z^{\prime})\in\overline{\mathcal{A}}\circ\overline{\mathcal{G}}$. Hence
$(z,z^{\prime})\in(\text{Id}_{Z}\cup\overline{\mathcal{A}})\circ(\overline{\mathcal{G}}\circ\overline{\mathcal{A}})^{n+1}\circ\overline{\mathcal{G}}$.

######  Lemma A.71.

_Let $F$ and $F^{\prime}$ be interfaces s.t. $F\sim F^{\prime}$. Let
$(z,z^{\prime})\in Z\times Y$._

  1. (a)

If $(z,z^{\prime})\in\overline{\mathcal{G}}_{F,F^{\prime}}$, then
$(z,z^{\prime})\in\overline{\mathcal{G}}\cup(\overline{\mathcal{A}}\circ\overline{\mathcal{G}})$.

  2. (b)

If
$(z,z^{\prime})\in\overline{\mathcal{A}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}_{F,F^{\prime}}$,
then $(z,z^{\prime})\in\overline{\mathcal{A}}\circ\overline{\mathcal{G}}$.

######  Proof A.72.

Consider arbitrary interfaces $F$ and $F^{\prime}$. Assume that $F\sim
F^{\prime}$. Additionally, consider arbitrary $(z,z^{\prime})\in Z\times Y$.

  1. (a)

Assume that $(z,z^{\prime})\in\overline{\mathcal{G}}_{F,F^{\prime}}$. By
$z^{\prime}\in Y$ and Proposition A.12(a),
$(z,z^{\prime})\in\overline{\mathcal{G}}\cup(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{G}})$.

The case that $(z,z^{\prime})\in\overline{\mathcal{G}}$ is trivial.

Consider now the case that
$(z,z^{\prime})\in(\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{G}})$.
Consider arbitrary $(z,s)\in\overline{\mathcal{G}}_{F,F^{\prime}}$ and
$(s,z^{\prime})\in\overline{\mathcal{G}}$. We know by Proposition A.12(a) that
$s\in Y^{\prime}$. Then, by $F\sim F^{\prime}$, $(z,s)\in
Z_{F,F^{\prime}}\times Y_{F,F^{\prime}}$ and
$(z,s)\in\overline{\mathcal{G}}_{F,F^{\prime}}$, it follows that
$(z,s)\notin((\mathcal{A}\cup\mathcal{A}^{\prime})\cap Z_{F,F^{\prime}}\times
Y_{F,F^{\prime}})$. So, in particular, $(z,s)\notin\mathcal{A}$. Hence,
$(z,z^{\prime})\in\overline{\mathcal{A}}\circ\overline{\mathcal{G}}$.

  2. (b)

Assume that
$(z,z^{\prime})\in\overline{\mathcal{A}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}_{F,F^{\prime}}$.
By $z^{\prime}\in Y$, we proceed by cases w.r.t. Proposition A.12(a).

If
$(z,z^{\prime})\in\overline{\mathcal{A}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}$,
then, there exists $(z,s)\in\overline{\mathcal{A}}_{F,F^{\prime}}$ and
$(s,z^{\prime})\in\overline{\mathcal{G}}$. As
$(z,s)\in\overline{\mathcal{A}}_{F,F^{\prime}}$, then $s\in X_{F,F^{\prime}}$,
and by $(s,z^{\prime})\in\overline{\mathcal{G}}$, $s\in Z$. Thus, by
definition of variables between interfaces, $s\in X$. By definition of
composite assumptions, $(z,s)\notin\mathcal{A}_{F,F^{\prime}}$, and as a
consequence $(z,s)\notin\mathcal{A}$. So, $(z,s)\in\overline{\mathcal{A}}$.

If
$(z,z^{\prime})\in\overline{\mathcal{A}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}_{F,F^{\prime}}\circ\overline{\mathcal{G}}$,
then there exists $(z,s)\in\overline{\mathcal{A}}_{F,F^{\prime}}$,
$(s,s^{\prime})\in\overline{\mathcal{G}}_{F,F^{\prime}}$ and
$(s^{\prime},z^{\prime})\in\overline{\mathcal{G}}$. By Proposition A.12(a), we
know that $s^{\prime}\in Y^{\prime}$. Additionally, by $F\sim F^{\prime}$ and
$s^{\prime}\in Z$, then $s^{\prime}\in X$. Assume towards a contradiction that
$(z,s^{\prime})\in\mathcal{A}$. Then, by definition of propagated assumptions
and $(s,s^{\prime})\in\overline{\mathcal{G}}_{F,F^{\prime}}$, we have
$(z,s)\in\hat{\mathcal{A}}_{F,F^{\prime}}$. This contradicts the fact that
$(z,s)\in\overline{\mathcal{A}}_{F,F^{\prime}}$. Thus,
$(z,s^{\prime})\notin\mathcal{A}$ and so
$(z,z^{\prime})\in\overline{\mathcal{A}}\circ\overline{\mathcal{G}}$.

###  A.6 Proof for Theorem 3.21

_Let $F,\ G$ and $I$ be interfaces. If $F\sim G$ and $F\otimes G\sim I$, then
$G\sim I$ and $F\sim G\otimes I$._

######  Proof A.73.

Consider arbitrary interfaces $F,\ G\text{ and }I$. Assume that:  (a1) $F\sim
G$; and  (a2) $F\otimes G\sim I$.

We start by proving that $G\sim I$.

From (a1), (a2) and Lemma A.1, it follows that $Y_{G}\cap Y_{I}=\emptyset$,
i.e. $G$ and $I$ are composable. We are missing to prove that:
$((\mathcal{A}_{G}\cup\mathcal{A}_{I})\cap(Z_{G,I}\times
Y_{G,I}))\subseteq\mathcal{G}_{G,I}.$ Let $(z,s)\in X_{G,I}\times Y_{G,I}$ and
$(z,s)\in\mathcal{A}_{G}\cup\mathcal{A}_{I}$. Note that by (a2), $s\notin
Y_{F}$. We want to prove that $(z,s)\in\mathcal{G}_{G,I}$. As $s\notin Y_{F}$
and by definition of composition, if $(z,s)\in\mathcal{A}_{G}$, then
$(z,s)\in\mathcal{A}_{F\otimes G}$. So, it follows that
$(z,s)\in\mathcal{A}_{F\otimes G}\cup\mathcal{A}_{I}$. Then, by (a2), we know
that $(z,s)\in\mathcal{G}_{F\otimes G,I}$. By monotonicity of composite flows
(Lemma A.12(b))
$\overline{\mathcal{G}}_{G,I}\subseteq\overline{\mathcal{G}}_{F\otimes G,I}$.
Then, it follows that $(z,s)\in\mathcal{G}_{G,I}$.

We prove now that $F\sim G\otimes I$.

From (a1), (a2) and Lemma A.1, it follows that $Y_{F}\cap Y_{G\otimes
I}=\emptyset$, i.e. $F$ and $G\otimes I$ are composable. We are missing to
prove that: $((\mathcal{A}_{F}\cup\mathcal{A}_{G\otimes I})\cap(X_{F,{G\otimes
I}}\times Y_{F,{G\otimes I}}))\subseteq\mathcal{G}_{F,G\otimes I}.$

Let $(z,s)\in X_{F,G\otimes I}\times Y_{F,G\otimes I}$ and
$(z,s)\in\mathcal{A}_{F}\cup\mathcal{A}_{G\otimes I}$. We prove
$(z,s)\in\mathcal{G}_{F,G\otimes I}$ by cases.

Case $(z,s)\in\mathcal{A}_{F}$ and $s\in Y_{G}$:

Assume towards a contradiction that $(z,s)\notin\mathcal{G}_{F,G\otimes I}$.
So, $(z,s)\in\overline{\mathcal{G}}_{F,G\otimes I}$. By associativity of
composite flows (Lemma A.12 (c)), $(z,s)\in\overline{\mathcal{G}}_{F\otimes
G,I}$. By definition of composition, then $s\in Y_{F\otimes G}$. Thus, by (a1)
and $(z,s)\in\mathcal{A}_{F}$, $(\star)(z,s)\in\mathcal{G}_{F,G}$.
Additionally, by suffix property of composite flows (Lemma A.12 (a)),
$(z,s)\in\overline{\mathcal{G}}_{F\otimes
G}\cup(\overline{\mathcal{G}}_{F\otimes
G,I}\circ\overline{\mathcal{G}}_{F\otimes G})$.

If $(z,s)\in\overline{\mathcal{G}}_{F\otimes G}$, then we have a contradiction
with $(\star)$.

Otherwise, there exists $s^{\prime}\in Y_{I}$ s.t.:
$(\star\star)(z,s^{\prime})\in\overline{\mathcal{G}}_{F\otimes G,I}\text{ and
}(s^{\prime},s)\in\overline{\mathcal{G}}_{F\otimes G}.$ By
$(z,s)\in\mathcal{A}_{F}$, $(s^{\prime},s)\in\mathcal{G}_{F\otimes G}$ and
definition of propagated assumptions,
$(z,s^{\prime})\in\hat{\mathcal{A}}_{F,G}$. So, by $s^{\prime}\in X_{F\otimes
G}$ and definition of composition, $(z,s^{\prime})\in\mathcal{A}_{F\otimes
G}$. As $s^{\prime}\in X_{F\otimes G}\cap Y_{I}$ and by (a2),
$(z,s^{\prime})\in\mathcal{G}_{F\otimes G,I}$. This contradicts
$(\star\star)$.

Hence $(z,s)\notin\overline{\mathcal{G}}_{F,G\otimes I}$, i.e.
$(z,s)\in\mathcal{G}_{F,G\otimes I}$.

Case $(z,s)\in\mathcal{A}_{F}$ and $s\in Y_{I}$:

By definition of composition and (a2), $(z,s)\in\mathcal{G}_{F\otimes G,I}$.
And by associativity of composite flows (Lemma A.12(c)),
$(z,s)\in\mathcal{G}_{F,G\otimes I}$.

Case $(z,s)\in\mathcal{A}_{G\otimes I}$:

Case $(z,s)\in\mathcal{A}_{I}$:

By (a2), $(z,s)\in\mathcal{G}_{F\otimes G,I}$. And by associativity of
composite flows (Lemma A.12(c)), $(z,s)\in\mathcal{G}_{F,G\otimes I}$.

Case $(z,s)\in\mathcal{A}_{G}$:

From an analogous reasoning to the case that $(z,s)\in\mathcal{A}_{F}$, it
follows that $(z,s)\in\mathcal{G}_{F,G\otimes I}$.

###  A.7 Proof for Corollary 3.23

_If $F\sim G$ and $F\otimes G\sim I$, then_ $(F\otimes G)\otimes
I=F\otimes(G\otimes I).$

######  Proof A.74.

Assume that $\star$ $F\sim G$ and $F\otimes G\sim I$. Then, by theorem 3.21,
it follows that: $\star\star$ $G\sim I$ and $F\sim G\otimes I$. By definition
of composition, it is easy to prove that: ($\dagger$) $X_{F\otimes
G,I}=X_{F,G\otimes I}$, $Y_{F\otimes G,I}=Y_{F,G\otimes I}$, and $Z_{F\otimes
G,I}=Z_{F,G\otimes I}$. And, by Lemma A.12(c), $\mathcal{G}_{F\otimes
G,I}=\mathcal{G}_{F,G\otimes I}$.

We prove now that $\mathcal{A}_{F\otimes G,I}=\mathcal{A}_{F,G\otimes I}$.

$\displaystyle\mathcal{A}_{F\otimes G,I}\quad\overset{\text{Def.
\ref{def:i:composition}}}{=}$
$\displaystyle(\mathcal{A}_{F}\cup\mathcal{A}_{G}\cup\hat{\mathcal{A}}_{F,G}\cup\mathcal{A}_{I}\cup\hat{\mathcal{A}}_{F\otimes
G,I})\ \cap(Z_{F\otimes G,I}\times X_{F\otimes G,I})\underset{\text{Lemma
}\ref{lemma:composition}\ref{lemma:composition:propagate}}{\overset{(\star),(\star\star)}{=}}$
$\displaystyle(\mathcal{A}_{F}\cup\mathcal{A}_{G}\cup\hat{\mathcal{A}}_{F,G}\cup\mathcal{A}_{I}\cup\hat{\mathcal{A}}_{F,G\otimes
I}\cup\hat{\mathcal{A}}_{G,I})\ \cap(Z_{F\otimes G,I}\times X_{F\otimes
G,I})\underset{\text{Lemma
}\ref{lemma:composition}\ref{lemma:composition:propAGI}-\ref{lemma:composition:propAIG}}{\overset{(\star),(\star\star)}{=}}$
$\displaystyle(\mathcal{A}_{F}\cup\mathcal{A}_{G}\cup\mathcal{A}_{I}\cup\hat{\mathcal{A}}_{F,G\otimes
I}\cup\hat{\mathcal{A}}_{G,I})\ \cap(Z_{F\otimes G,I}\times X_{F\otimes
G,I})\overset{(\dagger)}{=}$
$\displaystyle(\mathcal{A}_{F}\cup\mathcal{A}_{G}\cup\mathcal{A}_{I}\cup\hat{\mathcal{A}}_{F,G\otimes
I}\cup\hat{\mathcal{A}}_{G,I})\ \cap(Z_{F,G\otimes I}\times X_{F,G\otimes
I})\qquad\ \ \overset{\text{Def. \ref{def:i:composition}}}{=}$
$\displaystyle(\mathcal{A}_{F}\cup\mathcal{A}_{G\otimes
I}\cup\hat{\mathcal{A}}_{F,G\otimes I})\cap(Z_{F,G\otimes I}\times
X_{F,G\otimes I})\qquad\ \ \ \overset{\text{Def. \ref{def:i:composition}}}{=}$
$\displaystyle\mathcal{A}_{F,G\otimes I}.$

Finally, we prove that $\mathcal{P}_{F\otimes G,I}=\mathcal{P}_{F,G\otimes
I}$.

Note that by our previous results, it follows that:
$\mathcal{P}^{\mathcal{A}_{F\otimes G,I},\mathcal{G}_{F\otimes
G,I}}=\mathcal{P}^{\mathcal{A}_{F,G\otimes I},\mathcal{G}_{F,G\otimes I}}$.

$\displaystyle\mathcal{P}_{F\otimes G,I}\overset{\text{Def.
\ref{def:i:composition}}}{=}$ $\displaystyle\mathcal{P}_{F\otimes
G}\cup\mathcal{G}_{I}\cup\mathcal{P}^{\mathcal{A}_{F\otimes
G,I},\mathcal{P}_{F\otimes G,I}}\overset{\text{Def.
\ref{def:i:composition}}}{=}$
$\displaystyle\mathcal{P}_{F}\cup\mathcal{P}_{G}\cup\mathcal{P}^{\mathcal{A}_{F\otimes
G},\mathcal{P}_{F\otimes
G}}\cup\mathcal{P}_{I}\cup\mathcal{P}^{\mathcal{A}_{F\otimes
G,I},\mathcal{P}_{F\otimes G,I}}\underset{\text{Lemma
\ref{lemma:mono:g}}}{\overset{(\star),(\star\star)}{=}}$
$\displaystyle\mathcal{P}_{F}\cup\mathcal{P}_{G}\cup\mathcal{G}_{I}\cup\mathcal{P}^{\mathcal{A}_{F\otimes
G,I},\mathcal{P}_{F\otimes G,I}}\ \ \overset{}{=}$
$\displaystyle\mathcal{P}_{F}\cup\mathcal{P}_{G}\cup\mathcal{P}_{I}\cup\mathcal{P}^{\mathcal{A}_{F,G\otimes
I},\mathcal{P}_{F,G\otimes I}}\underset{\text{Lemma
\ref{lemma:mono:g}}}{\overset{(\star),(\star\star)}{=}}$
$\displaystyle\mathcal{P}_{F}\cup\mathcal{P}_{G}\cup\mathcal{P}_{I}\cup\mathcal{P}^{\mathcal{A}_{F,G\otimes
I},\mathcal{P}_{F,G\otimes I}}\cup\mathcal{P}^{\mathcal{A}_{G\otimes
I},\mathcal{P}_{G\otimes I}}\overset{\text{Def. \ref{def:i:composition}}}{=}$
$\displaystyle\mathcal{P}_{F,G\otimes I}.$

###  A.8 Proof for Theorem 3.28

_Let $F_{1}^{\prime}$, $F_{1}$ and $F_{2}$ be well-formed interfaces. If
$F_{1}^{\prime}\preceq F_{1}$ and $F_{1}\sim F_{2}$, then $F_{1}^{\prime}\sim
F_{2}$ and $F_{1}^{\prime}\otimes F_{2}\preceq F_{1}\otimes F_{2}$. _

######  Proof A.75.

Assume that $F_{1}^{\prime}\preceq F_{1}$ and $F_{1}\sim F_{2}$. Then, by
$F_{1}^{\prime}\preceq F_{1}$:  (r1)
$\mathcal{A}_{1}^{\prime}\subseteq\mathcal{A}_{1}$;  (r2)
$\mathcal{G}_{1}\subseteq\mathcal{G}_{1}^{\prime}$;  (r3)
$\mathcal{P}_{1}\subseteq\mathcal{P}_{1}^{\prime}$.

We start by proving that $F_{1}^{\prime}\sim F_{2}$.

By (r1),
$(\mathcal{A}_{1}^{\prime}\cup\mathcal{A}_{2})\subseteq(\mathcal{A}_{1}\cup\mathcal{A}_{2})$.
By definition of composite flows and (r2),
$(\dagger)\mathcal{G}_{F_{1},F_{2}}\subseteq\mathcal{G}_{F_{1}^{\prime},F_{2}}$.
Then, by $F_{1}\sim F_{2}$, we have:
$(\mathcal{A}_{1}^{\prime}\cup\mathcal{A}_{2})\cap(X_{F_{1},F_{2}}\times
Y_{F_{1},F_{2}})\subseteq\mathcal{G}_{F_{1}^{\prime},F_{2}}.$ So,
$F_{1}^{\prime}\sim F_{2}$.

We prove now that $F_{1}^{\prime}\otimes F_{2}\preceq F_{1}\otimes F_{2}$.

By our results above for the assumptions and guarantees composite, we are only
missing to prove that $\mathcal{P}_{F_{1}\otimes
F_{2}}\subseteq\mathcal{P}_{F_{1}^{\prime}\otimes F_{2}}$.

Consider arbitrary $(z,y)\in\mathcal{P}_{F_{1}\otimes F_{2}}$. If
$(z,y)\in\mathcal{P}_{1}\cup\mathcal{P}_{2}$, then, by (r3), if follows that
$(z,y)\in\mathcal{P}_{1}^{\prime}\cup\mathcal{P}_{2}$.

If $(z,y)\in\mathcal{P}^{\mathcal{A}_{F_{1}\otimes
F_{2}},\mathcal{G}_{F_{1}\otimes F_{2}}}$, then, by definition of derived
properties:

  1. (i)

$(z,y)\in\mathcal{G}_{F_{1}\otimes F_{2}}$, and

  2. (ii)

$(z,y)\notin(\text{Id}_{Z_{F_{1},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1},F_{2}}\circ\overline{\mathcal{A}}_{F_{1},F_{2}})^{*}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}$.

By $\mathcal{G}_{F_{1},F_{2}}\subseteq\mathcal{G}_{F_{1}^{\prime},F_{2}}$,
then $(z,y)\in\mathcal{G}_{F_{1}^{\prime},F_{2}}$, as well. We prove by
induction that for all $n\in\mathbb{N}$ and
$(z,y)\in\mathcal{G}_{F_{1},F_{2}}$:

$\displaystyle\text{ if
}(z,y)\notin(\text{Id}_{Z_{F_{1},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1},F_{2}}\circ\overline{\mathcal{A}}_{F_{1},F_{2}})^{n}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}$
$\displaystyle\text{ then
}(z,y)\notin(\text{Id}_{Z_{F_{1}^{\prime},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})^{n}\circ\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}.$

Consider arbitrary $(z,y)\in\mathcal{G}_{F_{1},F_{2}}$.

Base case $n=0$:  Note that $(z,y)\notin\overline{\mathcal{G}}_{F_{1},F_{2}}$.
Assume that
$(z,y)\notin(\overline{\mathcal{A}}_{F_{1},F_{2}}\circ\overline{\mathcal{G}}_{F_{1},F_{2}})$.
Then, for all $(z,s)\in\overline{\mathcal{A}}_{F_{1},F_{2}}$ there exists
$(s,y)\notin\overline{\mathcal{G}}_{F_{1},F_{2}}$. By $F_{1}^{\prime}\preceq
F_{1}$ and Lemma A.63, we have
$(\dagger\dagger)\mathcal{A}_{F_{1}^{\prime}\otimes
F_{2}}\subseteq\mathcal{A}_{F_{1}\otimes F_{2}}$. So, it follows from
$(\dagger)$ and $(\dagger\dagger)$, that for all
$(z,s)\in\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}}$ there exists
$(s,y)\in\mathcal{G}_{F_{1}^{\prime},F_{2}}.$ Thus,
$(z,y)\notin\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}$,
as well.

Induction step: We assume as induction hypothesis that the statement holds for
$n$. Consider arbitrary:
$(z,y)\notin(\text{Id}_{Z_{F_{1},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1},F_{2}}\circ\overline{\mathcal{A}}_{F_{1},F_{2}})^{n+1}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}.$

By induction hypothesis,

$\displaystyle(z,y)\notin(\text{Id}_{Z_{F_{1}^{\prime},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})^{n}\circ\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{A}}_{F_{1},F_{2}}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}.$

Then, for all
$(z,s)\in(\text{Id}_{Z_{F_{1}^{\prime},F_{2}}}\cup\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})\circ(\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}\circ\overline{\mathcal{A}}_{F_{1}^{\prime},F_{2}})^{n}\circ\overline{\mathcal{G}}_{F_{1}^{\prime},F_{2}}$
there
exists$(s,y)\notin\overline{\mathcal{A}}_{F_{1},F_{2}}\circ\overline{\mathcal{G}}_{F_{1},F_{2}}$.
By the same reasoning applied to the base case, it follows that for all