Information Technology Reference
In-Depth Information
low-level user who is supposed to know the entire system can construct the
bunch
B
S
(
u
)=
and possibly deduce some information
about what happened or what will happen at the high-level. When there is no
ambiguity, we will write
B
(
u
) instead of
B
S
(
u
). For every
u
such that
B
(
u
)is
non empty,
B
(
u
) is supposed to be measurable and without lost of generality
the measure
Pr
S
(
B
(
u
)) is supposed to be positive. A projection
u
{
λ
∈
Tr
|
u
is a prefix of
λ
|L
}
L
∗
such
∈
that
B
(
u
) is non empty is called
possible
.
3
Global Information Flow
Depending on the level of information we are interested in, we introduce an
abstraction function
φ
:
L → L
∪{}
,where
L
is some set with
|L
|≤|L|
and
L
)
ω
.Weextend
φ
on
H
as
the identity, and then on
E
ω
in a classical way. Notice that it is possible that an
infinite trace of
E
ω
has an image which is finite.
A property of abstraction level
φ
is a subset of (
H
express properties as sets of infinite traces on (
H
∪
L
)
∞
. We consider only
∪
properties
P
such that
φ
−
1
(
P
)
Tr
is a measurable subset of
Tr
. By abuse
of notation we write
Pr
S
(
P
)=
df
Pr
S
(
φ
−
1
(
P
)
∩
∩
Tr
), and write
P
instead of
φ
−
1
(
P
)
∩
Tr
everytime we compute probabilities, e.g., in
Pr
(
P
∩
A
)or
Pr
(
P
|
A
).
Definition 2.
Given a system S, the quantity of information flow for a prop-
erty P of abstraction level φ is the value IF
(
P, S
)=
max
u,v
|
Pr
S
(
P
|
B
(
u
))
−
L
∗
.
AsystemS is without information flow for a property P of abstraction level
φ if IF
(
P, S
)=0
.
Pr
S
(
P
|
B
(
v
))
|
for all possible u, v
∈
We can also consider a “qualitative” version of this definition:
Definition 3.
AsystemS is without qualitative information flow for a prop-
erty P of abstraction level φ if for every u
L
∗
such that B
(
u
)
is non-empty,
∈
Pr
S
(
P
)
=0
→
Pr
S
(
P
|
B
(
u
))
=0
.
Definition 4.
A system is without information flow for a given abstraction level
if it is without information flow for all properties of this level.
We will consider three abstraction functions which are of interest in an ob-
vious way. If
L
=
L
and
φ
is identity, i.e., there is no abstraction, we will speak
of
general
information flow. If
L
is a singleton
{l}
,and
φ
(
l
i
)=
l
for every
L
)
ω
expresses what happens on the high-level, as well
as whether two high-level events have been separated by a low-level event or
not (the identity of this low-level event does not matter). In this second case we
speak of
sequential
information flow. Finally, if
L
=
l
i
∈
L
,atraceon(
H
∪
{
τ
}
and
φ
(
τ
)=
τ
,
φ
(
l
i
)=
for every
l
i
, that is we are interested only in the projection on the
high-level of a trace, we will speak of
high-level
information flow.
The intuition behind this hierarchy of abstractions stems from the fact that
we may be interested whether an event
x
is followed by an event
y
,inother
words, in the presence of the pattern
xy
in a system trace.
∈
L
\{
τ
}
