Information Technology Reference
In-Depth Information
If
x
and
y
are both high-level events, this property cannot be expressed
using the definition of high-level information flow, since any intervening low-
level events are projected out by the abstraction. However, it can be expressed
as a sequential property: (
H
)
ω
.
If one of the events (say
x
) is low-level and the other one high-level, the
property can no longer be expressed by a sequential property, since the identity
of
y
is lost by abstraction to
l
. However, the presence of the pattern
xy
can still be
expressed as a general property: (
H
)
∗
xy
(
H
∪{
l
}
∪{
l
}
L
)
ω
. This motivates considering
properties which preserve full information for both high- and low-level events.
Another example to motivate our framework is the following. Consider a
program where variables are classified as low (observable by low level users) or
high. The system consists of the set of executions of the program. A regular
property like ”during every time duration
t
(the duration is measured by the
number of events and
t
is a fixed integer), the high level variable
x
is updated
at least once”, in other words, it is impossible that there exists a time duration
t
without an update of variable
x
can be of interest, and one can require that
the system does not suffer information flow for this property.
Let
L
0
=
L
∪
L
)
∗
xy
(
H
∪
\{
τ
}
.
L
0
)
∗
τ
ω
for the set of all infinite words formed
by actions from
H
and
L
. This is a superset of the set of system traces:
Tr
L
0
)
ω
We write
E
=(
H
∪
∪
(
H
∪
.
In the following, low level actions are denoted
a, b, ...
, sequences of low-level
actions
u, v, ...
, sequences of high-level actions
α, β, ...
and traces
λ
,
λ
, ...
.
Let
S
=(
E, H, L,Tr ,µ
) be a system and
T
be the associated probabilistic
tree. We define:
⊆E
(
H
∗
)
n
H
n
(
Tr
)=
{
(
α
1
, ..., α
n
)
∈
|∃
a
1
...a
n
∈
Lα
1
a
1
α
2
a
2
...α
n
a
n
∈
Pref
(
Tr
)
}
.
H
n
(
Tr
)=
(
H
∗
)
n−
1
H
ω
{
(
α
1
, ..., α
n
)
∈
|∃a
1
...a
n−
1
∈ Lα
1
a
1
α
2
a
2
...α
n
∈ Tr }
.
∈ L
n
|∃ α
1
...α
n
∈ H
∗
α
1
a
1
α
2
a
2
...α
n
a
n
∈ Pref
(
Tr
)
L
n
(
Tr
)=
{
(
a
1
, ..., a
n
)
}
.
H
∗
,a
i
∈
Tr
n
=
{
α
1
a
1
α
2
a
2
...α
n
a
n
∈
Pref
(
Tr
)
|
α
i
∈
L
}
.
We give below a characteristic property for a system
S
to be without sequen-
tial information flow. For this we need to introduce some technical terms related
to the probabilistic tree
T
.
We color edges labeled by a high-level action black and edges labeled by
a low-level action red. We are interested in the set of sequences of high-level
actions (including the empty word) which can occur starting from a node
x
.To
make this set of sequences more explicit we build for each such node
x
a”black”
probabilistic tree
T
x
in the following way: we keep only the black edges reachable
in
T
from
x
,andforeachnode
y
(including
x
) accessible from
x
by a black path,
we add a node
y
andanedge(
y, y
) labelled by
and with a probability equal
to the sum
p
of the probabilities of red edges starting from
y
in
T
.Thetree
T
x
is a probabilistic tree which has the following meaning: the probability of a path
in
T
x
starting from
x
labelled by
α
(without
labels) is exactly the probability
that the sequence of high-level actions
α
occurs from
x
; the probability of a path
in
T
x
starting from
x
labelled by
α
and ending in a leaf is the probability that
from
x
the sequence of actions
α
followed by a low-level action occurs.
