Information Technology Reference
In-Depth Information
Previously Stored Label
≫
New Label = New Stored Label
L
≫
=
L
L
≫
=
Low
High
Low
High
≫
=
High
Low
High
Low
L
1
L
2
≫
=
L
1
L
1
L
1
L
2
≫
=
L
1
L
2
L
2
Fig. 5.
Updating memory locations
Example 4.
Consider the following Java method, where the value computed for
the variable
low
does not actually depend on the value of the high confidentiality
variable
high
(which only affects the temporal variable
aux
). This program does
fulfill the non-interference policy at the final state, which can be proved by using
our non-interference verification methodology.
class Testclass { static int low=0, high; //@ setLabel(high, High);
public static void main(String[] args) {
high = Integer.parseInt(args[0]);
int aux=0; if (high > 2) aux = 1; else aux = 0; low = 0; } }
In order to avoid false positives during the evaluation of conditional statements,
we dynamically restore the previous context label after its execution. The ex-
tended semantics equations for the if-then-else are shown in Figure 6, where a
new continuation symbol
restoreLEnv
is used to restore the previous confiden-
tiality label. However, restoring the previous context label has to be carefully
considered in the presence of
break
or
continue
statements within a loop, since
they can abruptly change the information flow as shown in the following example.
Example 5.
Consider a variation of Example 3 where the while loop has a bogus
guard together with a
break
statement to exit the loop:
public class Testclass {static int low=0, high; //@ setLabel(high, High);
public static void main(String[] args) {high = Integer.parseInt(args[0]);
int aux=0; while (true) {high--; low++; if (high == 0) break;} } }
As in Example 3, when the while loop ends, the variable
low
has the initial value
of the variable
high
. Whenever
high
=0,the
break
statement is not executed.
In this case, the conditional guard uses
High
-labeled data, and the conditional
statement should not restore the previous context label. In other words, the
critical component here is not the
break
statement but rather the else branch
that does not contain the
break
.
In order to solve this problem, we check in Figure 6 whether either of the two
branches of a conditional statement contains a
break
or
continue
statement
and no other conditional statement or
while
loop in between. If there is such a
statement,
restoreLEnv
is not used. This case was not considered in [23] or in
[2], which only considered
break
statements within
High
guarded while loops.
Method invocation propagates the context label without changes as proposed
in [23] and, thus, is not shown here. Since while statements were expressed in
terms of if-then-else statements, they need a slight extension to introduce the
