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.
 
Search WWH ::




Custom Search