Information Technology Reference
In-Depth Information
attacker can analyze traces of computations only. By definition two systems are
trace equivalent if they accept the same language, therefore we have to make
equal the
α
ATT
de
=
α
T
abstraction of the result, namely
α
T
◦
α
low
. Finally, consider
P \
I
H
which avoids high-level inputs. Let
I
the operation
be the set of input
α
L
℘
T
Act
)
−→ ℘
T
Act
)such
actions, then we can define the abstraction:
:
(
(
)=
∀σ ∈ τ.σ∈
H
∩ I
,where
α
L
(
T ⊆
T
Act
:
T
τ ∈ T
σ ∈ τ
that for any
is a shorthand notation for
σ
being an action (node) in
τ
. Then we have that
α
L
(
{| P \
I
H
|}
=
{| P |}
). At this point, we can derive the NNI as:
α
T
◦
α
low
)
◦
α
L
(
α
T
◦
α
low
(
{| P |}
)=(
{| P |}
)
Consider now the notion of
Strong Non-deterministic Non-Interference
(SNNI)
defined in [10]:
P/
H
≈
T
P \
H
. In order to define SNNI as
an instance of the generalized abstract non-interference, we have to define the
operator
P
satisfies SNNI iff
P/
H
, that hides all the high-level actions. Let
α
L
:
℘
(
T
Act
)
−→ ℘
(
T
Act
)
∀σ ∈ τ.σ∈
L
. This defines
the interference abstraction in GANI and it is such that
)=
τ ∈ T
be the map such that
∀T ⊆
T
Act
:
α
L
(
T
{| P \
H
|}
=
α
L
(
{| P |}
).
The standard notion of SNNI introduced in [10] can be defined as
α
T
◦
α
low
(
{| P |}
)=
α
T
◦
α
low
◦
α
L
(
{| P |}
)
.
At this point, since bisimulations are equivalence relations [21], they can be
viewed as abstractions of computational trees, i.e., a tree is abstracted into
the equivalence class of all the trees bisimilar to it, then we can model both
BNNI and BSNNI. In this context, we obtain this by substituting to
α
T
,the
abstraction
α
B
, corresponding to the given chosen bisimulation, which associates
with a computation the set of all the computations bisimilar to the given one.
Consider now non-deducibility on compositions (NDC) and the bisimulation-
based NDC (BNDC) notions of non-interference. NDC is:
∀Π.P/
H
≈
T
(
P ||Π
)
\
H
,
where
is a process that can execute only high-level actions. In [10] it is
proved that NDC=SNNI, therefore also NDC can be modeled as a generalized
abstract non-interference. The situation is different when we consider BNDC,
i.e.,
Π
∀Π.P/
H
≈
B
(
P ||Π
)
\
H
, for the bisimulation relation
B
. In this case, we have
that BNDC
=BSNNI, and therefore we have to explicitly model it as general-
ized abstract non-interference. In [10] the authors also prove that BNDC can be
equivalently formalized as:
∀Π.P\
H
≈
B
(
P ||Π
)
\
H
. At this point, we note that we
α
ATT
, since in this definition it is only observable what a
low-level user (i.e., a user that can execute only low level actions) can see, which
is only the computation without high-level actions. Moreover, we have that
α
B
◦
α
L
as
have to consider
α
OBS
is the identity, since, in this case, non-interference is defined on computational
trees. Finally, we define
α
INT
noting that the semantics (computational tree) of
P ||Π
contains the semantics of
P.Π
(which doesn't execute synchronizations),
therefore we can define
α
INT
(
{| P ||Π|}
)=
{| P.Π|}
, modeling BNDC as follows:
∀Π.
(
α
B
◦
α
L
)
◦
α
INT
(
{| P ||Π|}
)=
α
B
◦
α
L
(
{| P ||Π|}
)
.
This is BNDC since in the right side of the equality
α
L
is applied to the semantics
of
P.Π
, and therefore executes only the high-level actions of
P
.
