Information Technology Reference
In-Depth Information
technique. In our previous work [2], we analyzed (local) non-interference of Java
functional methods (i.e. methods that return values). However, in this paper,
we are able to analyze entire Java programs, and thus, we consider
global non-
interference
.
This paper is organized as follows. In Section 2, we recall the notion of non-
intereference and describe a mechanism to specify non-interference policies in
JML. In Section 3, we recall the specification of the Java semantics in rewriting
logic. In Section 4, we extend this semantics to handle confidential information
and formulate a non-interference certification methodology that is based on the
unreachability of undesired states in the extended semantics. In Section 5, we
develop an approximation of the extended Java semantics that produces a finite
search space for any input Java program. By using this abstract semantics (which
we implement as a source-to-source transformation of the extended semantics in
Maude) we formulate our non-interference analysis and prove its soundness. We
include some experiments in Section 6. A thorough discussion of related work is
presented in Section 7. Finally, Section 8 presents our conclusions.
2 Non-interference
A non-interference policy establishes a confidentiality level for each source pro-
gram variable of primitive datatypes. It guarantees that actual values of variables
with a higher confidentiality level do not influence the output of a variable with
a lower confidentiality level during program execution [11,15,20,23]. It is implic-
itly assumed that constants that appear in a program always have the lowest
confidentiality level (i.e., the considered program is authorized to access secret
data, but it does not contain secret data in its code).
A non-interference policy can be represented by a
partially ordered set
Labels,
≤
and a labeling function
Labeling
:
Var
→
Labels
,where
Labels
≤
is the finite set of confidentiality levels,
is a partial order between confiden-
tiality levels, and
Var
is the set of source program variables [22,4,16]. There are
usually two confidentiality levels:
Labels
=
{
Low
,
High
}
. These represent pub-
lic non-secret data (low confidentiality) and secret data (high confidentiality),
respectively.
Labels, ≤
forms a lattice where
Low
is the greatest lower bound
or
bottom
element (
⊥
),
High
is the least upper bound or
top
element (
), and
Low
<
High
.The
join
operator (
) is defined as
Low
Low
=
Low
;otherwise,
X
Y
=
High
. Enforcing non-interference means that the values of
High
-labeled
source variables cannot flow to
Low
-labeled source variables, whereas the values
of
Low
-labeled source variables can flow to
High
-labeled source variables. The
attacker model for global non-interference that we formalize below assumes that
the attacker is passive and can only see the
Low
-labeled source variables of the
Java program at the initial and final states and not at the intermediate states.
Our methodology can certify programs that have temporal breaches and are still
non-interferent.
In order to express confidentiality policies, we use the
Java modeling language
JML [17], which is a property specification language for Java modules. The text
