Information Technology Reference
In-Depth Information
interl
(
HI
∗
,λ
|L
0
)
∀
λ
∈
Tr
∀
γ
∈
∃
δ
∈
LLES
(
λ, S
)
γ
=
δ
|L
0
∪HI
HI
∗
let
Noninter
µ
1
,...,µ
n
=
interl
(
HO
∗
,µ
1
lµ
2
l...µ
n
l
)
For each
µ
1
, ..., µ
n
∈
×
l
)
ω
. In a similar way to Theorem 7, one can prove
(
H
∪
Theorem 8.
For a given probabilistic system S, Noninterference
(
S
)
holds iff
for each n,foreachµ
1
, ..., µ
n
HI
∗
Pr
S
(
Noninter
µ
1
,...,µ
n
,u
)
∈
=0
for every
L
n
such that B
(
u
)
is non-empty.
u
∈
6Con lu on
We have studied probabilistic information flow from a point of view parame-
terized by user-specified properties of interest. A property is a set of system
traces, possibly viewed through an abstraction function. Our definitions support
a range of property classes, e.g., referring to high-level events only, or high-level
sequences separated by low-level events. We also allow specifications where a
distinction is made between the past and future fragments of a trace. In this
way, we can define (absence of) information flow for a given property, or for an
entire set of properties of a given class.
We have given theorems that characterize the structure of systems for which
absence of information flow according to these notions is guaranteed: for instance,
a certain isomorphism between probabilistic trees is needed for properties which
can distinguish subsequences of high-level events separated by low-level ones. We
have also shown how several classic notions of possibilistic information flow (non-
inference, noninterference and separability) can be expressed using qualitative
versions of our definitions.
We believe that this property-specific fashion of characterizing information
flow is useful because it can be adapted to the particularities of the system
under analysis. In many cases, a mere division into high- and low-level events
and a single definition of information flow policy may not be enough, whereas
our approach allows for a finer granularity of reasoning depending on the
property.
An issue for future research is to apply this framework in the case where
systems and properties are explicitly given as Markov chains and regular lan-
guages, respectively, and to investigate the decidability of the above notions of
information flow in this setting.
Acknowledgements.
We are grateful to Anatol Slissenko for the numerous and
fruitful discussions of the approach studied in this paper.
References
1. Aldini, A., Bravetti, M., Gorrieri, R.: A process-algebraic approach for the analysis
of probabilistic noninterference. Journal of Computer Security, 12 (2004) 191-246
2. Barthe, G., D'Argenio, P.R., Rezk, T.: Secure information flow by self-composition.
17th IEEE Computer Security Foundations Workshop. IEEE Computer Society
(2004) 100-114
