Information Technology Reference
In-Depth Information
Here there is an an illicit and implicit information flow from the
High
-labeled
source variable
high
to the
Low
-labeled source variable
low
. For instance, when
the variable
high
contains the value
0
or
1
,thevariable
low
is assigned the value
0
and
1
, respectively. This implicit flow would be detected using the context
label, which is set to
High
after evaluating the expression
high>0
,andwhich
forces variable
low
to be set to
High
independently of the confidentiality level
of the expression
low++
.
In contrast to [2] where local non-interference was studied, here we consider
global non-interference (i.e., we are able to ensure a non-interference policy at
the final state of the whole Java program execution, which contains several meth-
ods, classes, and function calls). This important improvement in the verification
power (which has been hardly explored in the related literature) requires the fol-
lowing two modifications to the non-interference analysis of [2]. These changes
avoid the dicult (or costly) process of tracing the current confidentiality label
of a memory location back to the point where this location was created.
1. We introduce an additional confidentiality label (
Low
High
), which al-
low us to represent not only the current confidentiality label of a memory
location but also to keep track, at a global level, of hazardous transitions
from an initial confidentiality label
Low
to
High
. Similarly, we introduce the
confidentiality label (
High
Low
), in order to avoid false positives where a
High
-labeled variable is updated with the value of a
Low
-labeled expression
and then updated again with the value of a
High
-labeled expression.
2. In [2], we used the context label only when updating the value of a variable
in memory, as in [23,16,14], and when returning values as in [14]. In this
paper, we use the context label during expression evaluation, as in [4].
We describe the information-flow extended version of the rewriting logic seman-
tics of Java by the rewrite theory
R
Java
E
=(
Σ
Java
E
,E
Java
E
,R
Java
E
),
E
Java
E
=
Δ
Java
E
→
Java
E
rewriting relation. In the new
semantics, program data not only consist of standard concrete values but each
value is decorated with its corresponding confidentiality label. Formally, we con-
sider the label change
LabelChange
=
B
Java
E
and its corresponding
{
High
,
High
}
so that the
domain of program variables in the extended semantics is
Value×
Low
Low
(
Labels ∪
LabelChange
). We write
<Value,LValue>
for a pair consisting of a concrete
value and its corresponding confidentiality label in
Labels
LabelChange
.
Thanks to the modularity of the rewriting logic approach to formalizing pro-
gram semantics [12], our changes to the semantics of Section 3 are incremental
and minimal. The assignment computes the new confidentiality label in terms
of the previous label at the memory location, namely
NewVal = LVal' >>> LVal
.
The new operator
∪
is defined in Figure 5.
The context label can only change due to a conditional control flow state-
ments. According to [11,4,23,16], the evaluation of its boolean guards returns
a confidentiality level that is associated to the resulting
true
or
false
value
and, possibly, a modified context label. The extended semantic equations for
the if-then-else of Figure 2 need some slight revision, which is motivated by the
following example.
≫