Information Technology Reference
In-Depth Information
introduced for timed automata in [2] are again instances of GANI. In all these
constructions, the model of an attacker is specified as an abstract interpretation
of the system semantics. This is a key point in order to introduce systematic
methods for deriving attackers by transforming abstract domains. We general-
ize the method introduced in [14] to derive harmless attackers for GANI, i.e.,
abstractions of the semantics of systems which guarantee non-interference.
This is not the first attempt neither for deriving general schemes for security
policies [12], nor for trying to bridge language-based and process-calculi secu-
rity [13,16,20]. In particular, in [12] the authors provide a uniform method for
defining computer security properties for process algebras, obtaining a quite flex-
ible schema for reasoning about different properties. What we do in this paper is
something similar since the aim is the same, but in a more general context which
ranges from language based-security to process algebras, to timed automata. The
problem of studying the link between language-based and process calculi secu-
rity is well known in literature. In particular, recently [13] this problem has been
approached by transforming imperative language in a CCS-like process calculus,
and by defining a notion of BNDC which corresponds for imperative languages to
the standard notion of non-interference. In our case, we don't have to transform
programs, since we consider a general model that can cope with both imperative
programming languages and process algebras.
2
Information Flows in Language-Based Security
Non-interference can be naturally expressed by using semantic models of pro-
gram execution. This idea goes back to Cohen's work on
strong dependency
[5], which uses denotational semantics for modeling how information can be
transmitted among variables during the execution of programs. Therefore non-
interference for programs essentially means that
“a variation of confidential
(high or private) input does not cause a variation of public (low) output”
[22].
When this happens, we say that the program has only
secure information flows
[3,5,9,18,26]. This situation has been modeled by considering the denotational
(input/output) semantics
. In particular, we consider pro-
grams where data are typed as private (
H
) or public (
L
). Program states in
P
of the program
P
Σ
are functions (represented as tuples) mapping variables in the set of values
V
.If
v ∈
V
n
, we abuse notation by writing
T
∈{
H
,
L
}
,
n
=
|{x ∈
Var
(
P
)
|x
:
T
}|
,and
T
when
v ∈
V
is a value for the variables with security type
T
.Moreover,we
assume that any input
v
H
=
s
, can be seen as a pair (
h, l
), where
s
h
is a value
s
L
=
l
for private data and
is a value for public data. In this case, (standard)
non-interference
can be formulated as follows:
A program
P
is
secure
if
∀
input
s, t . s
L
=
t
L
⇒
(
P
(
s
))
L
=(
P
(
t
))
L
.
This problem has been formulated also as a
Partial Equivalence Relation
(PER)
[17,23]. In [14], the notion of abstract non-interference is introduced for mod-
eling both weaker attack models, and declassification. The idea is that, instead
of observing the concrete semantics of programs, namely the concrete values of
