Information Technology Reference
In-Depth Information
--- Evaluates boolean expression keeping the then and else statements
ceq k((if E S else S') -> K) lenv(CL)
= k(E -> (if(S, S') -> restoreLEnv(CL) -> K)) lenv(CL)
if not break-or-continue(S) and not break-or-continue(S') .
ceq k((if E S else S') -> K) lenv(CL) = k(E -> (if(S, S') -> K)) lenv(CL)
if break-or-continue(S) or break-or-continue(S') .
eq k(<bool(true),LVal> -> (if(S, S') -> K)) lenv(CL)
= k(S -> K) lenv(CL join LVal) .
eq k(<bool(false),LVal> -> (if(S, S') -> K)) lenv(CL)
= k(S' -> K) lenv(CL join LVal) .
--- New equation to restore previous context label
eq k(restoreLEnv(CL) -> K) lenv(CL') = k(K) lenv(CL) .
Fig. 6.
Extended equations for the if-then-else
--- Stack loop and transform while expression into while continuation
eq k((while E S) -> K) lstack(Lstack) lenv(CL)
= k(while(E,S) -> restoreLEnv(CL) -> popLStack -> K)
lstack(while(E,S) -> K, Lstack) lenv(CL) .
Fig. 7.
Extended equations for while statement
restorelEnv
continuation (shown in Figure 7). The semantic specification of
the
break
statement stays the same as shown in Figure 4: the context label
lenv
(
CL
) is not modified and the
restoreLEnv
expression introduced by the
while statement is removed.
4.1 Proving Non-interfence as a Safety Property
Now, we are ready to formulate a novel characterization of non-interference that
allows us to check it as a property that is verified for each possible execution
trace instead of being verified for each set of indistinguishable execution traces.
Definition 3 (Strong Non-Interference).
A Java program
P
Java
is
strongly
non-interferent
for a given labeling function if for every extended initial state
St
1
and for its corresponding final program state
St
2
given by
P
Java
,St
1
→
Java
E
St
2
Low
(
P
Java
)
,
St
2
[
var
]=
, we have that for all
var
∈
Val,
Low
for a value
Val
.
Since in our model, a public variable can only have the label
Low
or the label
Low
High
, this means that in the extended execution of a program that
is not strongly non-interferent, the label of at least one program variable is
Low
High
. Given an initial state
St
and a given labeling function, we denote
the corresponding extended state by
St
E
.
Lemma 1.
Consider a Java program
P
Java
and two initial states
St
1
and
St
2
such that
St
1
=
Low
St
2
. Consider the two corresponding final program states
St
1
and
St
2
given by
→
Java
St
1
→
Java
St
2
P
Java
,St
1
and
P
Java
,St
2
.If
Low
(
P
Java
)
such that
St
1
[
var
]
St
2
[
var
]
,then
there exists
var
∈
=
