Information Technology Reference
In-Depth Information
Table 1.
Narrow and Abstract Non-Interference
[
η
]
P
(
ρ
)if
∀h
1
,h
2
∈
V
H
, ∀l
1
,l
2
∈
V
L
.η
(
{l
1
}
)=
η
(
{l
2
}
)
⇒ ρ
(
{
P
(
h
1
,l
1
)
L
}
)=
ρ
(
{
P
(
h
2
,l
2
)
L
}
)
H
, ∀l ∈
V
L
.ρ
(
))
L
)=
ρ
(
))
L
)
(
η
)
P
(
φ
[]
ρ
)if
∀h
1
,h
2
∈
V
P
(
φ
(
{h
1
}
)
,η
(
{l}
P
(
φ
(
{h
2
}
)
,η
(
{l}
public data, the attackers can only observe
properties
of public data, namely
ab-
stract semantics
of the program. For this reason we model attackers by means of
abstract domains. Formally, the
lattice of abstract domains
of a concrete domain
C
is isomorphic to the lattice
uco
(
C
) of all the upper closure operators on
C
[8].
An
upper closure operator
is monotone, idempotent,
and extensive
1
.The
model of an attacker
, also called
attacker
, is therefore a pair
of abstractions
ρ
:
C → C
on a poset
C
L
)), representing what an observer can
see about, respectively, the input and output of a program. The notion of
nar-
row (abstract) non-interference
(NANI), denoted
[
η
]
η, ρ
,with
η, ρ ∈
uco
(
℘
(
V
(
ρ
)
, is given in Table 1. It
says that if the attacker is able to observe the property
P
η
of public input, and
ρ
the property
of public output, then no information flow concerning the pri-
vate input is observable from the public output. The problem with this notion is
that it may introduce
deceptive flows
[14], generated by different public outputs
due to different public inputs with the same
η
property. Consider, for instance,
[
Par
]
l
:=
l ∗h
2
(
Sign
)
2
, then we can observe a variation of the output's sign due to
the existence of both negative and positive even numbers, revealing flows not due
to private data, since
cannot affect the sign of the result. Most known mod-
els for weakening non-interference (e.g., PER model [23]) and for declassifying
information (e.g., robust declassification [29]) corresponds to instances of NANI
[14,17]. In order to avoid deceptive interference we introduce a weaker notion of
non-interference. In this case, the
set
of all the elements sharing property
h
η
is
used as the public input. Moreover we consider also a property
φ ∈
uco
(
℘
(
V
H
)),
modeling the private property that has not to be observed by the attacker
η, ρ
.
This notion, denoted
(
η
)
P
(
φ
[]
ρ
)
, is called
abstract non-interference
(ANI) and
is defined in Table 1.
Note that
[
id
]
(
id
)
models exactly (standard) non-interference. Moreover,
we have that abstract non-interference is a weakening of both, standard and
narrow non-interference:
[
id
]
P
(
φ
[]
ρ
)
,
while standard non-interference is not stronger than the narrow version, due to
deceptive interference. In [14], two methods for deriving the most concrete output
observation for a program, given the input one, for both narrow and abstract
non-interference are provided. In particular the idea is that of abstracting in the
same object all the elements that, if distinguished, would generate a visible flow.
These most concrete output observations, that are not able to get information
from the program
P
⇒
P
(
φ
[]
ρ
)
and
[
η
]
P
⇒
P
(
id
)
(
η
)
(
ρ
)
(
η
)
P
observing
η
in input, are, respectively, denoted
[
η
]
P
(
id
)
L
)).
and
(
η
)
P
(
φ
[]
id
)
,bothin
uco
(
℘
(
V
1
∀x ∈ C. x ≤
C
ρ
(
x
).
2
Note that
Par
de
=
{,ev,od,⊥}
and
Sign
de
=
{,
0+
, −, ⊥}
.
