Information Technology Reference
In-Depth Information
of a JML annotation can either be in one line after the //@ marker, or in many
lines enclosed between the markers /*@ and @*/ . They are ignored by traditional
compilers. The initial confidentiality level of a variable in a Java program is writ-
tenwiththeword setLabel as a JML annotation (e.g. setLabel ( var , High )).
The confidentiality label of program variables is Low if nothing is specified (i.e.,
program variables are public by default). These JML annotations, together with
the default assumption, define the labeling function of the non-interference
policy.
Example 1. Consider the following Java program borrowed from [10] that models
a bank account and the initial state given by the execution of the function main :
public class Account { int balance; //@ setLabel(balance, High);
public boolean extraService;
public Account() { balance = 0; extraService = false; }
public void writeBalance(int amount) { balance = amount;
if (balance>=10000) extraService=true; else extraService=false; }
private int readBalance() {return balance;}
public boolean readExtra() {return extraService;}
}
class System { static Account a = new Account();
public static void main(String[] args) {
int initbalance; //@ setLabel(initbalance, High);
initbalance = Integer.parseInt(args[0]);
a.writeBalance(initbalance); System.out.println(readExtra()); }}
This non-interference policy specifies that the object field balance of the global
object a and the initialization parameter initbalance (i.e., args [ 0 ]) hold secret
data. This program is insecure w.r.t. this policy since an observer with low
access rights can obtain partial information about the variable balance via an
observation of the non-secret variable extraService .
We assume a fixed Java program P Java . Vars ( P Java ) denotes the set of static
source variables that may be initialized by the main function call. We denote
the set of Low program variables as Low ( P Java )=
{
var
Vars ( P Java )
|
Labeling ( var )= Low
. A program state St is a set of value assignments to
program variables. Given var ∈ Vars ( P Java ) and a state St , St [ var ] denotes the
value of variable var in St .Wemodela Java program P Java as a state transi-
tion system between pairs P, St ,where P is the current, still-to-be-executed
part of the Java program P Java and St represents the current program state.
}
P Java ,St 0
denotes the initial configuration of standard program execution and
stands for the empty program.
Note that we assume that every Java program properly terminates for each set
of input data (i.e., we do not consider non-terminating programs, deadlocks, or
runtime errors). We also assume deterministic Java programs, without threads
or exceptions.
,St
denotes a final configuration ,where
Java is the transition relation that describes any possible one-
step transition between any two Java program states. An execution (or trace) of
P Java is a sequence
P Java ,St 0 Java
···
P i ,St i Java
··· → Java
,St n
,
P Java ,St 0 Java
which is simply denoted by
,S n
if the intermediate states
are irrelevant. We can also abbreviate
,S n
by
S n
.
 
Search WWH ::




Custom Search