Information Technology Reference
In-Depth Information
We define program non-interference by using an equivalence =
Low
relation-
ship between states [20,22,4]. Roughly speaking, non-interference establishes that
any two terminating runs of a program that start from indistinguishable initial
states produce indistinguishable final states.
Definition 1 (State equality [20]).
Given a Java program
P
Java
,twostates
St
1
and
St
2
for
P
Java
are
indistinguishable
at the confidentiality level
Low
,writ-
ten
St
1
=
Low
St
2
, if for all
var
Low
(
P
Java
)
,St
1
[
var
]=
St
2
[
var
]
.
What the attacker can see from a final state is determined by a relation
∈
≈
Low
.Two
executions of a program
P
Java
are related by
≈
Low
if they are indistinguishable
to the attacker [20]. The notion of non-interference is therefore parametric on
≈
Low
. A program is non-interferent if, whenever different initial program states
are indistinguishable at level
Low
, this implies that the corresponding final states
are also indistinguishable at level
Low
.
Definition 2 (Non-interference [20]).
A Java program
P
Java
is
non-interferent
if for every pair of different program initial states
St
1
and
St
2
,
and
St
1
,
St
2
for
their
corresponding
final
program
states
such
that
P
Java
,St
1
→
Java
St
1
P
Java
,St
2
→
Java
St
2
and
, we have that
St
1
=
Low
St
2
implies
St
1
≈
Low
St
2
.
In this paper, we follow the standard approach in the literature that considers
St
≈
Low
St
iff
St
=
Low
St
. Then, the non-interference condition of Definition
2 is understood as the lack of any
strong dependence
[20] of
Low
-labeled variables
on any of the
High
-labeled variables.
3 The Rewriting Logic Semantics of Java
In the following, we briefly recall the rewriting logic semantics of Java that was
originally given in [12]. We refer the reader to [18] for further technical details
on rewriting logic semantics.
In [12], a su
ciently large subset of full Java 1.4 language is specified in
Maude, including inheritance, polymorphism, object references, multithreading,
and dynamic object allocation. However, Java native methods and many of the
available Java built-in libraries are not supported. The specification of Java op-
erational semantics is a rewrite theory: a triple
R
Java
=(
Σ
Java
,E
Java
,R
Java
)
where
Σ
Java
is an order-sorted
signature
;
E
Java
=
Δ
Java
B
Java
is a set of
Σ
Java
-equational
axioms
where
B
Java
are algebraic axioms such as associativity,
commutativity and unity, and
Δ
Java
is a set of terminating and confluent (mod-
ulo
B
Java
) equations. Finally,
R
Java
is a set of
Σ
Java
-rewrite rules that are not
required to be confluent nor terminating.
Intuitively, the sorts and function symbols in
Σ
Java
describe the static struc-
ture of the Java program state space as an algebraic data type; the equa-
tions in
Δ
Java
describe the operational semantics of its deterministic features;
and the rules in
R
Java
describe its concurrent features. Following the rewrit-
ing logic framework we denote by
u
→
Java
v
the fact that the concrete terms
