Information Technology Reference
In-Depth Information
3.1 Syntax
The syntax of expressions defined in Figure 1 is based on a
λ
-calculus extended
with the imperative constructs of ML, conditional branching and boolean values,
where the (
x.X
) construct provides for recursive values. Names of references
(
a
), domains (
d
), and threads (
m,n
), are drawn from disjoint countable sets
Ref
, respectively. References are information containers
to which values of the language pertaining to a given type in
,
Dom
=
∅
and
Nam
can be assigned.
Declassification is introduced in the language by means of
flow policy decla-
rations
[9]. They have the form (flow
F
in
M
), and are used to locally weaken
the information flow policy that is valid for the particular execution context, by
enabling information flows that comply to the flow policy
F
to take place within
the scope of the delimited block of code
M
. Expression
M
is executed in the
context of the current flow policy extended with
F
; after termination the current
flow policy is restored, that is, the scope of
F
is
M
. For context-policy awareness,
programs can inspect the allowed flow policy of the current domain by means of
the
allowed-condition
, which is written (allowed
F
then
N
t
else
N
f
). The con-
struct tests whether the flow policy
F
is allowed by the current domain and
executes branches
N
t
or
N
f
accordingly, in practice offering alternative behav-
iors to be taken in case the domains they end up are too restrictive. For migration
and concurrency, the thread creator (thread
M
at
d
) spawns the thread
M
in
domain
d
, to be executed concurrently with other threads at that domain.
Networks
are flat juxtapositions of domains, each containing a store and a
pool of threads, which are subjected to the allowed flow policy of the domain.
Threads run concurrently in
pools
P
:
Typ
, which are mappings from
thread names to expressions (denoted as sets of threads).
Stores
S
:
Nam
→
Exp
Ref
→
Val
map reference names to values.
Position-trackers
T
:
, map thread
names to domain names, and are used to keep track of the locations of threads in
the network. The pool
P
containing all the threads in the network, the mapping
T
that keeps track of their positions, and the store
S
containing all the references
in the network, form
configurations
P,T,S
. The flow policies that are allowed
by each domain are kept by the
allowed-policy mapping
W
:
Dom
→
Flo
from
domain names to flow policies, which is considered fixed in this model.
Nam
→
Dom
3.2 Operational Semantics
The small step operational semantics of the language is defined in Figure 2. The
'
W
Σ
' turnstile makes explicit the allowed flow policy of each domain in the
network, and the
reference labeling
Σ
that determines the type of values that
is assigned to each reference name. Other security-related information, such as
security levels, could be added for the purpose of an information flow analysis.
The call-by-value evaluation order is specified by representing expressions
using
evaluation contexts
.
Evaluation Contexts
E ::= []
|
(E
N
)
|
(
V
E)
|
(E;
N
)
|
(ref
θ
E)
|
(! E)
(1)
(E :=
N
)
|
(
V
:= E)
|
(if E then
N
t
else
N
f
)
|
(flow
F
in E)
