Information Technology Reference
In-Depth Information
search in PGM-SEMANTICS :
java((preprocess(EX2-MAUDE) noType . 'main < new string [i(0)] > noVal))
=>! JO:Output .
Solution 1 JO:Output --> pl(bool(true))
No more solutions.
If the attacker observes these two final states, she will appreciate the two different
values for the variable
extraService
.
4 Proving Non-interference by Using an Extended
Instrumented Semantics
Non-interference is usually understood to be a security property and is therefore
defined as a
hyperproperty
[7] (i.e., a property defined on a set of sets of traces).
For instance, in Example 2, the verification process for non-interference should
check the (possibly infinite) set of (possibly infinite) sets of final states issued
from the (possibly infinite) sets of indistinguishable initial configurations. Note
that checking the final states issued from
EX1-MAUDE
and
EX2-MAUDE
is just one
of the combinations to be analyzed. In contrast, the verification process for a
safety property should simply check the traces issuing from the (possibly infinite)
set of initial configurations, which is simpler.
In this paper, we prove non-interference as a safety property by instrumenting
the Java semantics in order to dynamically keep track of the change of the confi-
dentiality labels of program variables. Intuitively, the semantic instrumentation
is defined as follows:
1. Attach a confidentiality label to each memory location; this allows us to
observe their confidentiality level at the final execution state.
2. Attach a confidentiality label to the evaluation of program expressions; this
allows us to know whether the evaluation of an expression involves high
confidentiality data.
3. Associate a confidentiality label to the evaluation of program statements,
particularly those involving conditional expressions or guards; this allows us
to determine whether the control flow at a given execution point depends
on the actual value of high confidential variables. However, this label is not
attached to each program statement. Rather it is kept as an extra attribute
of a state in the extended Java semantics. This corresponds to the notion of
a
context label
being updated after each evaluation step in [11,23,16], which
is introduced in the following example.
Example 3.
Consider the following Java
3
program
TestClass
that is borrowed
from [23]. We endow it with the attached non-interference policy:
public class Testclass {static int low=0, high; //@ setLabel(high, High);
public static void main(String[] args) {
high = Integer.parseInt(args[0]); while (high > 0) {high--;low++;} }}
3
We omit the semantics of some Java operators such as
++
,
++
,and
+=
,sincethey
can be defined in terms of addition (
+
) and assignment (
=
), as usual [18].
