Information Technology Reference
In-Depth Information
Similarly, data-flow/control-flow analysis techniques are devoted to statically
discover flows of secret data into public variables [4,18,19,23]. In concurrency,
bisimulation is used to prove equivalence between computations where private
actions are hidden with respect to the same system's computations where these
actions are avoided [10]. In real-time systems trace equivalence is used to prove
that the computations where private actions are avoided are equivalent to the
same system's computations where these actions are admitted with a minimum
fixed delay, and then hidden to the attacker [2]. These notions are all based on
the same principle, which is non-interference, but they can be hardly recognized
as instances of a same construction. This is due to the fact that different aspects
of the underlying computational models become crucial in order to provide ex-
pressive enough notions of secrecy in sequential, non-deterministic, concurrent
and real-time systems. While in sequential programs we are mainly concerned
with non-interference in input/output behavior, in concurrency and in real-time
we are, respectively, mainly concerned with interleaving actions and time delays.
Standard non-interference is often too strict for any practical use in language-
based security: most programs are rejected by static control/data flow analyzers
or type checkers for non-interference. In order to adapt security policies to practi-
cal cases, it is essential to know how much an attacker may learn from a program
by (statically) analyzing its input/output behavior. This idea led to the defini-
tion of the notion of
abstract non-interference
[14], which captures a weaker
form of non-interference. Namely, non-interference is made parametric relatively
to some abstract property, formalized as an abstract interpretation [7], of the
input/output behavior. This notion however is not adequate to cope with more
complex systems like concurrent and real-time systems. In particular, as stated
in [14], abstract non-interference strongly relies upon a denotational model of
computation, which is inadequate for modeling security protocols for instance.
Main Contribution and Related Works.
In this paper, we prove that the no-
tion of abstract non-interference introduced in [14] can be generalized in order
to cope with many well-known models of secrecy in sequential, concurrent and
real-time systems and languages. This is achieved by factoring abstractions in
order to identify sub-abstractions modeling the different properties of the system
on which the notions of non-interference are based. Abstract interpretation [7]
and the theory of abstract domain transformers [8] plays a key role in this gen-
eralization: The abstraction represents here both what an attacker may observe
about a computation (as in abstract non-interference [14]) and which aspects of
the computation are relevant for checking non-interference. In this context, non-
interference corresponds to asking that the behavior of the chosen relevant as-
pects of the computation is independent from what an attacker may observe. We
prove that both narrow and abstract non-interference in [14] are instances of our
generalized abstract non-interference (GANI). Then we prove that NNI (Non-
deterministic Non-Interference), SNNI (Strong NNI), NDC (Non-Deducibility
on Compositions), BNDC (Bisimulation NDC), BNNI (Bisimulation NNI), and
BSNNI (Bisimulation SNNI) in [10] for Security Process Algebras (SPA), are all
instances of GANI. Finally, we prove that decidable notions of non-interference
