Information Technology Reference
In-Depth Information
Hence,
) the following set collects all the trees that have to
be indistinguishable from the tree
∀σ ∈ α
INT
◦
α
OBS
(
{| A|}
:
Υ
(
σ
)=[
σ
]
de
=
δ ∈ α
OBS
(
{| A|}
)
δ
max
σ
σ
Example 2.
Consider a system
A
,ifwehave
α
OBS
(
{| A|}
)=
{
1
→
2
→
3
,
1
→
2
→
4
,
1
→
3
→
2
}
and
α
INT
◦α
OBS
(
{| A|}
)=
{
1
→
2
→
3
,
1
→
3
→
2
}
then [1
→
2
→
3] =
{
)=
{
1
→
2
→
4
,
1
→
2
→
3
,
1
→
5
→
3
,
3
→
5
→
4
,
1
→
2
→
5
,
1
→
3
→
2
,
3
→
2
→
1
}
and
α
INT
◦α
OBS
(
{| A|}
)=
{
1
→
2
→
3
,
1
→
3
→
2
,
3
→
2
→
1
}
then [1
→
2
→
3] =
{
1
→
5
→
3
,
1
→
2
→
3
,
1
→
2
→
4
}
,[1
→
3
→
2] =
{
1
→
5
→
3
,
1
→
3
→
2
}
and,
finally, [3
→
2
→
1] =
{
3
→
2
→
1
,
3
→
5
→
4
}
.
1
→
2
→
3
,
1
→
2
→
4
}
,[1
→
3
→
2] =
{
1
→
3
→
2
}
.While,ifwehave
α
OBS
(
{| A|}
Similarly to [14], we define the set
D
{| A|}
collecting all computations that may fail
secrecy, and
Irr
{| A|}
collecting all computations for which secrecy cannot fail.
]
σ ∈ α
INT
◦
α
OBS
(
=
[
)
D
{| A|}
σ
{| A|}
=
X
∀σ ∈ α
INT
◦
α
OBS
(
])
{| A|}
)
.X ∈↑
([
σ
Irr
{| A|}
The predicate
Secr
{| A|}
, which characterizes all the elements that should be con-
tained in the abstraction modeling the most concrete harmless attacker, is de-
fined as
Secr
{| A|}
(
X
)iff
∀σ ∈ α
INT
◦
α
OBS
(
{| A|}
)
.
(
∃Z ∈
[
σ
]
.Z ⊆ X ⇒∀W ∈
[
σ
]
.W ⊆ X
)
)
is the most concrete abstraction that enforces the notion of GANI to hold, w.r.t.
the relation
=
X
Secr
{| A|}
(
def
X
Following the construction in [14], we can prove that
S{|A|}
max
.
Theorem 5.
Let
A
be a system.
S{|A|}
is the most concrete abstraction such
that
∀σ ∈ α
INT
◦
α
OBS
(
{| A|}
)
, ∀δ ∈ α
OBS
(
{| A|}
)
.δ
max
σ ⇒S A|}
(
δ
)=
S{|A|}
(
σ
)
.
Proposition 1.
S
(
{| A|}
)=
S
(
↑
(
D
{| A|}
))
∪
Irr
{| A|}
.
5Con lu on
We introduced GANI as a generalization of abstract non-interference for au-
tomata and concurrent systems. We believe that the combination of abstract
interpretation and non-interference may provide advanced techniques for an-
alyzing, in a
modular
way, how sub-components of complex systems interact
during computation and how, analyses at different levels of abstraction can be
combined in a useful way. On one side, abstract interpretation has been proved
to be the most appropriate framework for reasoning about properties of compu-
tations at different levels of abstraction. On the other side, strong-dependency,
and in particular non-interference, is the most appropriate notion to disclose
information-flows among sub-components of a system, when a variation of some
of them can be conveyed to the others. GANI is intended to bridge these two
