Information Technology Reference
In-Depth Information
izes information flow is defined in [8] by giving a definition of secrecy in multi-
agent systems, using a modal logic of knowledge in a state-based model. This
generalizes several existing approaches and can be extended to probabilistic se-
curity. Their parameterization stems from defining formulas (knowledge) of what
must be kept secret, thus providing a fine-grained way of characterizing security
requirements. Since the approach is state-based, our model appears complemen-
tary in that it can talk about both past and future evolution of the system.
Other perspectives on information flow include that of [2] which offers a
variety of characterizations of non-interference, expressed in Hoare logics and
CTL; however, the variety is not given by parameterization, but language as-
pects such as sequential vs. concurrent, or termination sensitivity. Closer to a
parametric view is the approach of [4], where the parameter is an observable
property (an abstraction) of the public observations of a program. Thus, the at-
tacker is a data-flow analyzer,andcanbespecifiedinanabstract interpretation
framework. Both approaches deal with much more specific systems, described in
particular programming languages, and the class of expressed properties, though
parameterized to some extent, is not as general.
Beyond the possibilistic approaches, [3] analyzes quantitative information
flow for a simple imperative language from a semantic point of view, whereas [15]
replace indistinguishability in the formalization of non-interference by similarity
based on the notion of distance, in a process-algebraic setting. In comparison,
we also define quantity of information flow based on the distance between the
probability of a property given an observation.
Our approach to parameterization allows properties that range from the gen-
eral to the entirely system-specific. Thus we can select the granularity (a partic-
ular trace set or even a single trace) with respect to which information flow is
analyzed. Alternatively, quantifying over classes of such properties, we can still
obtain and reason about several of the classic definitions of information flow.
Paper Outline.
We first introduce the mathematical model of probabilistic event
systems which we use throughout the paper. Section 3 gives property-based de-
finitions for three classes of probabilistic information flow, and theorems char-
acterizing systems that conform to these notions. These results are extended in
Section 4 to properties which distinguish between past and future with respect
to the reference point defined by the observation. Section 5 shows how some of
the classic definitions of information flow can be expressed in this formalism.
2
Probabilistic Event Systems
Notations
Given a finite alphabet
A
,welet
A
∗
(resp.
A
ω
) denote the set of finite (resp.
infinite) sequences (or traces) over this alphabet. The set
A
∞
is the union of
A
∗
and
A
ω
. The empty sequence is denoted
. Given a sub-alphabet
A
⊂
A
and a
trace
λ
,
λ
|A
denotes the projection of
λ
onto this sub-alphabet. If
λ
is a finite
non-empty trace,
last
(
λ
) denotes the last letter of
λ
.
