Information Technology Reference
In-Depth Information
P
Java
,St
1
→
Java
E
St
E
and
St
E
[
var
]=
Val,
Low
for a value
High
Val
.
From Lemma 1 we derive that strong non-interference implies non-interference,
as given by the following result.
Theorem 1 (Strong Non-Interference Soundness).
Given a Java program
P
Java
,if
P
Java
is strongly non-interferent (Definition 3), then
P
Java
is non-
interferent (Definition 2).
The
following
example
illustrates the
mechanization of
our
verification
methodology.
Example 6.
Consider again the Java program of Example 1. Now, we compute
the final state in the extended Java program execution for
EX1-MAUDE
(for sim-
plicity we show only the value of variable
extraBalance
).
search in PGM-SEMANTICS-EXTENDED :
java((preprocess(EX1-MAUDE) noType .
'main < new string [i(0)] > noVal))
=>! M:Store .
Solution 1 M:Store --> store([l(6),<bool(false),Low >> High>] ...)
No more solutions.
The execution for
EX2-MAUDE
will also contain the label
Low
High
for variable
extraBalance
.
In other words, we transform non-interference into a stronger property which
can be effectively checked in the extended semantics. Obviously, we are not able
to certify the security of all the programs that are secure, as shown in Example 7.
Example 7.
Consider the following Java program borrowed from [23].
class Testclass { static int low=0, high; //@ setLabel(high, High);
public static void main(String[] args) {high = Integer.parseInt(args[0]);
low = high; low = low - high;} }
Apparently, there is an explicit flow from variable
high
to variable
low
through
the two assignment statements. However for any execution, when program ends,
the value of variable
low
is always
0
so that the variable
low
does not depend
on the variable
high
.AccordingtoDefinition2,theprogram is non-interferent.
However, we give a false positive by using our notion of strong non-interference
since the assignment “
low
=
high
”assignstothevariable
low
a high confiden-
tiality label
Low
High
and the last statement “
low
=
low
−
high
”doesnot
revert the label back to
low
.
The program of Example 7 cannot be verified by traditional type inference
approaches [22,26,4] either, since they fail to verify (type check) any program
with temporary breaches, e.g. Examples 4 and 7 above, whereas Example 4 is
effectively verified by using our methodology.
5 Approximating Non-interference by Using an Abstract
Semantics
The extended, instrumented Java semantics defined so far allows us to develop
a technique for proving non-interference. However, this technique is still not
