Information Technology Reference
In-Depth Information
Conversely, suppose that
Noninference
(
S
)holds.Let
λ
∈
Tr
,and
u
=
λ
|L
.
L
∗
such that
Pr
S
(
NonInf ,v
)=0and
B
(
v
) is non-empty. There exists some
λ
in
B
(
v
), and the projection
w
of
λ
on
L
belongs to
Tr
and
v
is a prefix of
w
.So,
Pr
S
(
NonInf ,w
)
>
0, but
Pr
S
(
NonInf ,v
)
> Pr
S
(
NonInf ,w
), a contradiction.
No qualitative general information flow for the property
NonInf
can occur.
Then
Pr
S
(
NonInf
)
=0,since
u
is also in
Tr
. Suppose there exists some
v
∈
Moreover, we can quantify the degree of noninference by measuring the maxi-
mal value of
L
∗
.
|
Pr
S
(
NonInf
)
−
Pr
S
(
NonInf
|
B
(
u
))
|
for all non-empty
B
(
u
),
u
∈
2. Separability
Separability is aimed to express a complete independence between the se-
quences of actions at high and low level:
Separability
(
S
)
λ
∈
Tr interl
(
λ
|L
0
,λ
|H
)
τ
Tr
.
Again this security property can be expressed in terms of qualitative sequen-
tial information flow for some set of properties. For each
ξ
1
, ..., ξ
n
≡∀
λ
∈
Tr
∀
∈
H
∗
,let
∈
)
∗
:
Sep
ξ
1
,...,ξ
n
(
λ
)holdsiff
λ
=
ξ
1
lξ
2
l...ξ
p
lξ
p
+1
ξ
p
+2
...ξ
n
l
for some
p
Sep
ξ
1
,...,ξ
n
be the following predicate defined on (
H
∪{
l
}
≤
n
.
Theorem 7.
For a probabilistic system S, Separability
(
S
)
holds iff for any prop-
erty Sep
ξ
1
,...,ξ
n
,whereξ
1
...ξ
n
=0
and there is no
qualitative sequential information flow for these properties.
∈
Tr
|H
,Pr
S
(
Sep
ξ
1
,...,ξ
n
)
Proof.
Suppose
Separability
(
S
) holds. Consider the property
Sep
ξ
1
,...,ξ
n
for
some
ξ
1
, ..., ξ
n
∈
Tr
|H
. Suppose
Pr
S
(
Sep
ξ
1
,...,ξ
n
)=0.Let
v
=
a
1
a
2
...a
p
be the
projection on
L
of some trace in
Tr
.If
p
≥
n
then
ξ
1
a
1
ξ
2
a
2
...ξ
n
a
n
a
n
+1
...a
p
∈
Tr
,
and if
p<n
then
ξ
1
a
1
ξ
2
a
2
...ξ
p
a
p
ξ
p
+1
...ξ
n
Tr
. The two cases contradict
Pr
S
(
Sep
ξ
1
,...,ξ
n
) = 0. Suppose that for some
ξ
1
...ξ
n
∈
Tr
|H
,thereisqual-
itative sequential information flow for property
Sep
ξ
1
,...,ξ
n
. This means that
Pr
S
(
Sep
ξ
1
,...,ξ
n
)
∈
L
+
=0andthereexists
u
∈
with
Pr
S
(
Sep
ξ
1
,...,ξ
n
|
B
(
u
)) = 0
and
B
(
u
)isnon-empty.
Let
v
=
a
1
a
2
...a
p
be the projection on
L
of some trace in
B
(
u
). If
p
≥
n
then
ξ
1
a
1
ξ
2
a
2
..., ξ
n
a
n
a
n
+1
...a
p
∈
Tr
which contradicts
Pr
S
(
Sep
ξ
1
,...,ξ
n
|
B
(
u
)) = 0. If
p<n
then
ξ
1
a
1
ξ
2
a
2
..., ξ
p
a
p
ξ
p
+1
...ξ
n
∈
Tr
which contradicts again the fact that
Pr
S
(
Sep
ξ
1
,...,ξ
n
B
(
u
)) = 0.
Conversely, suppose there is no qualitative sequential information flow for
any property
Sep
ξ
1
,...,ξ
n
,where(
ξ
1
, ..., ξ
n
)
|
H
n
(
Tr
)andthereexists
λ, λ
∈
∈
Tr
interl
(
λ
|L
0
,λ
|H
)
τ
such that
ν
and
ν
Tr
.
The trace
ν
can be written
ξ
1
a
1
ξ
2
a
2
...ξ
n−
1
a
n−
1
ξ
n
τ
,where
ξ
∈
∈
H
∗
,and
a
i
∈
∈
L
0
.Thus
Pr
S
(
Sep
ξ
1
,...,ξ
n
B
(
a
1
a
2
...a
n−
1
τ
)) = 0 with
B
(
a
1
a
2
...a
n−
1
τ
)non-
empty since
a
1
a
2
...a
n−
1
τ
=
λ
|H
. Therefore
Pr
S
(
Sep
ξ
1
,...,ξ
n
)mustbeequalto
zero since there is no information flow for this property.
|
3. Noninterference
Noninterference is a security property introduced by Goguen and Meseguer
[5] and generalized by McCullough [11]. It demands that a low-level user cannot
infer that any sequence of high-level inputs has (not) occurred. Let
HI
⊂
H
(resp.
HO
) is the set of high-level input (resp. output) actions. We have
HI
∩
HO
=
∅
.
