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
.