Information Technology Reference
In-Depth Information
These two abstractions tells us that, in general, non-interference holds whenever
the amount of information that an attacker can grasp from a computation is
precisely what, for the given notion of non-interference, that attacker is allowed
to observe about it.
Finally, we have to model the observational capability of the passive attacker
observing the system, and we consider a further abstraction
α ATT , called attacker
abstraction , which characterizes the model of the attacker, namely what it can
observe of the system behavior. In this case the attacker is passive since it cannot
interfere with the execution of the program, and it cannot control the inputs of
the system. By using these three abstractions we define generalized abstract
non-interference for the system
S
as
α ATT α OBS (
{| S|}
α ATT α INT α OBS (
{| S|}
)=
)
This equation says that, in the
model chosen by
α OBS , the maximal
amount of information that the at-
tacker is allowed to observe, deter-
mined by
{| S|}
α ATT α INT ,isexactlywhat
the attacker does observe, deter-
mined by
α OBS
α ATT . In other words, this
definition of non-interference says
that the attacker, modelled by the
abstraction
α INT
α OBS
( {| S|} )
α INT
α OBS
( {| S|} )
α ATT , cannot distinguish
between the observable computa-
tions (
α ATT
α ATT
α OBS ) and the set of only
those computations that the at-
tacker should observe (
α ATT
α OBS
( {| S|} )
=
α ATT
α INT
α OBS
( {| S|} )
α INT α OBS ).
The Generalized Non-Interference Policy. It is worth noting that this definition
of GANI in general is characterized by a possibilistic interpretation of equality
and doesn't provide an explicit notion of non-interference. Indeed, in ANI [14],
the non-interference policy states that all the computations with the same public
input has to provide the same public outputs. We can think of generalizing the
notion of non-interference by checking the equality of public observations of the
outputs for all the computations sharing a common maximal partial execution,
instead of sharing only the public input. Consider the tree semantics
{| S|}
of the
system
S
.
Asystem
S
is secure if
∀σ ∈ α INT α OBS (
{| S|}
)
, ∀δ ∈ α OBS (
{| S|}
)
.
δ max σ ⇒ α ATT (
δ
)=
α ATT (
σ
)
where the relation
max , specifies the maximal subtree which
δ
shares with an el-
ement in
α OBS (
{| S|}
). The definition above clearly, depends on the subtree relation
.Consider
σ ∈ α INT α OBS (
{| S|}
) and consider
δ ∈ α OBS (
{| S|}
):
δ max σ
if
∃π δ.π σ ∧∀π
π.π π δ, ∀σ ∈ α OBS (
π σ
=
{| S|}
)then
Search WWH ::




Custom Search