Information Technology Reference
In-Depth Information
In particular, for example, we can have the trace
,
,
,
,
.
,
.
,
.
...
begin-c
2
end-c
4
cloche
5
cloche
5
6
cloche
6
3
begin-c
8
3
whose projection
, on the low-level
actions, is not the one described above. This means that in this system there is
interference.
Consider the attacker abstraction
begin-c
,
2
end-c
,
4
begin-c
,
6
.
3
end-c
,
8
.
3
α
low
, defined in Sec. 3.2, the interference
L
H
. We define the family of abstractions
abstraction
α
L
and the language
α
n
,
with
n ∈
N
, as follows:
)=
τ ∈L
∀σ
i
,t
i
, σ
j
,t
j
∈τ.i
j, σ
i
,σ
j
∈
H
⇒ t
i
− t
j
|≥n
α
n
(
L
=
L
H
where each map
). Then the notion of non-
interference introduced in [2] for timed automata can be specified as follows:
α
n
is additive and
=
α
n
(
L
α
low
◦
α
n
(
L
)=
α
low
◦
α
L
◦
α
n
(
L
),
where
α
L
◦
α
n
=
α
L
. Note that, in this case,
α
OBS
=
α
n
◦
α
T
.
Theorem 4.
A timed automaton, with timed language
L
, satisfies n-non inter-
ference iff
α
low
◦
α
n
(
L
)=
α
low
◦
α
L
◦
α
n
(
L
)
.
4
Deriving GANI Attackers
In this section, we generalize the construction to GANI of the most powerful
attacker [14]. Let
A
be a system and let
α
OBS
and
α
INT
be abstractions defining
the chosen notion of non-interference for which
A
results insecure whenever
observed by the attacker modeled by
α
ATT
.Aswesaid,
α
OBS
and
α
INT
depend on the
definition of non-interference that we chose, while
α
ATT
depends on what we decide
to observe about the computation. Therefore if non-interference is not satisfied,
i.e., the system is not secure as regards the chosen notion of non-interference,
we can think of further abstracting the attacker abstraction in order to achieve
security. The resulting abstraction provides a certificate of the security level of
the system
A
with respect to the fixed observation and private abstractions. In
order to find an abstraction that makes equal the sets
α
ATT
◦
α
OBS
and
α
ATT
◦
α
INT
◦
α
OBS
we have to merge elements in both sets in order to make them contain the
same new abstract objects. Hence, given a security policy determined by what
is observable (
α
OBS
), and what at most the attacker should observe (
α
INT
◦
α
OBS
), we
derive
from the program
the most concrete harmless attacker
α
ATT
for the given
policy. Namely, we derive the minimal abstraction necessary in order to make
GANI hold. Note that, in abstract non-interference [14] there is a clear criterion
for collecting elements in order to build the abstraction: abstracting to the same
object all the elements resulting from computations that differ only for private
inputs. The corresponding construction for GANI is provided by the relation
max
max
for defining the sets
of objects that need to have the same abstraction in order to achieve secrecy.
defined in the previous section. Hence, we use
