Information Technology Reference
In-Depth Information
The definition above is based on the observation that if a
computation
has a
maximal partial computation in common with what can be surely observed by
the attacker, then it is in those points, where the common partial computations
end, that some private action has interfered in the computation.
Example 1.
Let
A
be a system, if
α
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
max
1
→
2
→
3,
1
→
2
→
4
max
1
→
2
→
3and1
→
3
→
2
max
1
→
3
→
2.
3.1
Abstract Non-interference as GANI
In this section, we show that abstract non-interference [14], which general-
izes standard non-interference [5,15], is an instance of GANI. For determinis-
tic programs the standard denotational semantics is given as the abstraction
approximating traces with input/output relations (functions for deterministic
programs) [6]
3
.Let
X
be a set of traces, the denotational semantics is defined:
λσ
.
σ
σ ∈ X, |σ| <ω
∪
⊥
|σ|
ω
,where
α
D
(
X
=
σ
and
σ
denote
)=
σ
respectively the initial and the final states of the trace
. Given two closures
α
φ
φ ∈
V
H
)and
η ∈
V
L
), we define the abstraction
Σ → Σ
−→
uco
(
uco
(
:(
)
℘
(
℘
(
Σ
)
× ℘
(
Σ
)) such that for any
f
:
Σ −→ Σ
:
S
=
)=
S
,S
))
α
φ
φ
h
,η
l
,h ∈
V
H
,l ∈
V
L
S
=
f
φ
h
,η
l
(
f
(
)
(
)
(
(
)
(
The idea is to abstract denotational input/output semantics to the set of all the
possible associations between the corresponding input/output abstract states. In
this way, we model the observation made by the attacker, which consists precisely
in the ability to observe input/output abstract values. Consider the function
C
H
:
℘
V
H
)
−→
V
H
that uniquely chooses an element in the domain of values
V
H
.
(
∀h
1
,h
2
.
ρ
P
φ
h
1
)
,η
l
)
L
)=
ρ
P
φ
h
2
)
,η
l
)
L
)is
Note that the equation
(
(
(
(
)
(
(
(
(
)
∀h
ρ
P
φ
h
,η
l
)
L
)=
ρ
P
φ
C
H
(
V
H
))
,η
l
)
L
).
equivalent to the equation
.
(
(
(
)
(
)
(
(
(
(
)
Therefore abstract non-interference can be formulated as follows:
H
))
L
)=
H
))
))
L
)
∀h ∈
V
.ρ
(
P
(
φ
(
h
)
,η
(
l
ρ
(
P
(
φ
(
C
H
(
V
,η
(
l
At this point, we can define the
interference
abstraction
α
ANI
:
℘
(
℘
(
Σ
)
× ℘
(
Σ
))
−→ ℘
)), which selects only the observation with the fixed private
input, hence for any
(
℘
(
Σ
)
× ℘
(
Σ
F∈℘
(
℘
(
Σ
)
× ℘
(
Σ
)):
)=
S
,S
∈F
∃l ∈
V
α
ANI
(
F
L
.S
=
φ
(
C
H
(
V
H
))
,η
(
l
)
In order to obtain abstract non-interference, we assume that the attacker may
observe only the
abstraction of the low output. This process is encoded by
the attacker abstraction, which depends upon the input/output abstractions
η, ρ ∈
ρ
α
ρη
uco
(
℘
(
V
L
)), i.e.,
ATT
:
℘
(
℘
(
Σ
)
× ℘
(
Σ
))
−→ ℘
(
℘
(
V
L
)
× ℘
(
V
L
)) where
)=
η
X
H
,X
L
, Y
H
,Y
L
∈ F
α
ρη
ATT
(
F
(
X
L
)
,ρ
(
Y
L
)
Then, we can specify abstract non-interference in the following theorem.
3
For deterministic systems the trace semantics coincides with the tree semantics.
