Information Technology Reference
In-Depth Information
3
Generalized Abstract Non-interference
In this section, we introduce a generalization of abstract non-interference, called
generalized abstract non-interference
(shortly GANI), which subsumes many of
the known notions of non-interference based on tree-like computations and au-
tomata. Abstract interpretation plays a key role in this generalization: The ab-
straction represents here both what an attacker may observe about a computa-
tion (as in abstract non-interference) and which aspects of the computation are
relevant for checking non-interference, aspects determined by the specific notion
of non-interference that we have to enforce on the system. Non-interference cor-
responds to asking that relevant (confidential) aspects of the computation have
no effects on what an attacker observes of the computation. Moreover, what an
attacker may observe is indeed composed by two aspects: what the particular
notion of non-interference
allows
to observe, and what effectively the attacker
can
observe. In the following, we consider computational systems
S
modeled by
their tree semantics
.The
corresponding trace and I/O denotational semantics are, respectively, denoted
by
{| S|}
, i.e., the set of all the trees of computations of
S
.
We define generalized non-interference by means of three abstractions in the
standard framework of abstract interpretation, i.e., additive functions, each one
with a specific and precise meaning, depending on the given notion of non-
interference, and depending on the attacker model. The chosen policy of non-
interference decides two of these abstractions:
α
OBS
:
| S|
and
S
α
OBS
abstracts the tree semantics in the model used
in the notion of non-interference that has to be enforced. Note that, the ab-
straction level chosen for defining non-interference corresponds to
delegating
particular parts
(i.e., aspects)
of the system to release information
[24]. For
instance, if we want to check standard non-interference for imperative pro-
gramming languages, then
The first abstraction
α
OBS
corresponds to the denotational semantics ab-
straction of the computational tree. We call this abstraction the
observation
abstraction
. Such an abstraction extracts always an observational property
from semantic trees, e.g., all the computational traces, the I/O relations,
etc.;
α
INT
:
The second abstraction
α
INT
characterizes the maximal amount of informa-
tion that an attacker should observe, in the chosen policy. This abstraction
regulate what information may be released
[24]. For example, if we have to
check non-interference in
[10], then we want the computations where pri-
vate actions are hidden to be equivalent to the computations where private
actions are avoided. Namely the set of all the computations where private
actions are avoided is the maximal information that the attacker is allowed
to observe. In this case
Spa
α
INT
selects only those computations where private
actions are not executed. This abstraction, called
interference abstraction
,
forgets about all information which should not be observed by an attacker.
Such an abstraction always selects the subset of the possible computations
that we allow the attacker to observe, namely it is such that for each
X
in
its domain,
α
INT
(
X
)
⊆ X
.
