Information Technology Reference
In-Depth Information
feasible in general because there are too many possible initial states to consider
for the safety property to be checked. In the following, we develop an abstract,
rewriting logic Java semantics that allows us to statically analyze global non-
interference. Similar to [2], the purpose of the abstract semantics is to correctly
approximate the extended computations in a finite way. Given the extended
Java semantics, where there are concrete labeled values, we simply get rid of
the values in the abstract semantics, and use their confidentiality labels as the
abstract values instead.
In the following, we develop an abstract version of the extended rewriting
logic semantics of Java developed in Section 4, which we describe by the rewrite
theory
R
Java
#
=(
Σ
Java
#
,E
Java
#
,R
Java
#
),
E
Java
#
=
Δ
Java
#
B
Java
#
and its
corresponding
→
Java
#
rewriting relation. As in Section 4, our approach for the
abstract Java semantics consists of modifying the original theory
R
Java
E
(taking
advantage of its modularity) by abstracting the domain to
Labels
LabelChange
and introducing approximate versions of the Java constructions and operators
tailored to this domain.
An
abstract interpretation
(or abstraction) [9] of the program semantics is
given by an
upper closure operator
α
:
℘
(
State
)
∪
→
℘
(
State
), which is
mono-
tonic
(for all
SSt
1
,SSt
2
∈
℘
(
State
),
SSt
1
⊆
SSt
2
implies
α
(
SSt
1
)
⊆
α
(
SSt
2
)),
idempotent
(for all
SSt
∈
℘
(
State
),
α
(
SSt
)
⊆
α
(
α
(
SSt
))), and
extensive
(for
all
SSt
∈
℘
(
State
),
SSt
⊆
α
(
SSt
)). In our framework, each Java program
state
St
∈
State
is abstracted by its closure
α
(
{
St
}
). Our abstraction function
α
:
℘
(
State
E
)
℘
(
State
E
) is a simple homomorphic extension to sets of states
of the function 2
nd
:
Value
→
×
(
Labels
∪
LabelChange
)
→
(
Labels
∪
LabelChange
),
meaning that we disregard the actual values of data.
In the abstract Java semantics, several alternative computation steps of
→
Java
E
are mimicked by a single abstract computation step of
→
Java
#
, reflecting the fact
that several distinct behaviors are compressed into a single abstract state (i.e.
set of states). The instrumentalization of the Java semantics for dealing with a
set of states instead of one single state implicitly means too many modifications.
Therefore, we adopt a different approach. When several
→
Java
E
rewrite steps are
mimicked by a single abstract rewriting state leading to an abstract Java state,
and those rewrite steps apply different rules or equations, we use concurrency
at the Maude level. Despite the fact that our extended Java semantics contains
only equations and no rules, the abstract Java semantics does contain rules in
R
Java
#
to reflect the different possible evolutions of the system.
The abstract semantics is mainly a straightforward extension of the extended
semantics. The only difference is that any set of equations that was confluent
and terminating in the extended semantics but might become non confluent
or non terminating in the abstract semantics is transformed into rules. As a
representative example, the abstract rules associated to two of the equations of
the extended semantics of the if-then-else statement are shown in Figure 8.
Now, we are ready to formalize the abstract rewriting relation
→
Java
#
,which
intuitively develops the idea of applying only one rule or equation from the
concrete Java semantics to an abstract Java state while exploring the different
