Information Technology Reference
In-Depth Information
M
the capture-avoiding substitution of
W
for the free
occurrences of
x
in
M
. The operation of adding or updating the image of an
object
z
to
z
in a mapping
Z
is denoted [
z
:=
z
]
Z
.
The transition rules of our semantics are decorated with the flow policy de-
clared by the evaluation context where the step is performed. The lifespan of the
flow declaration terminates when the expression
M
that is being evaluated termi-
nates (that is,
M
becomes a value). In particular, the evaluation of (flow
F
in
M
)
simply consists in the evaluation of
M
, annotated with a flow policy that is at
least as permissive as
F
. The flow policy that decorates the transition steps
is used only by the rules for (allowed
F
then
N
t
else
N
f
), where the choice of
the branch depends on whether
F
is allowed to be declared or not. The thread
creation construct functions as a migration construct when the new domain of
the created thread is different from that of the parent thread. The last rule
establishes that the execution of a pool of threads is compositional (up to the
expected restriction on the choice of new names). Notice that
W
, representing
the allowed flow policies associated to each domain, is never changed.
For simplicity, we assume memory to be shared by all programs and every
computation domain, in a transparent form. This does not remove the distributed
nature of the model, as programs' behavior depends on where they are [6].
{
x
→
W
}
We denote by
4 Security Property
In a distributed setting with concurrent mobile code, programs might need to
comply simultaneously to different allowed flow policies that change dynamically.
The property of flow policy confinement deals with this diculty by placing
individual restrictions on each step that might be performed by a part of the
program, taking into account the possible location where it might take place.
Compatibility.
Since we are considering a higher-order language, values stored
in memory can be used by programs to build expressions that are then executed.
In order to avoid deeming all such programs insecure, memories are assumed to
be compatible to the given security setting and typing environment, requiring
typability of their contents with respect to the relevant type system and param-
eters. Informally, a memory
S
is said to be (
W,Σ,Γ
)-compatible if for every
reference
a
dom(
S
) its value
S
(
a
) is typable. This predicate will be defined for
each security analysis, and can be shown to be preserved by the semantics.
∈
Flow Policy Confinement.
The property is defined co-inductively for
located
threads
, consisting of pairs
d,M
m
that carry information about the location
d
of a thread
M
m
. The location of each thread determines which allowed flow
policy it should obey at that point, and is used to place a restriction on the flow
policies that decorate the transitions: at any step, they should comply to the
allowed flow policy of the domain where the thread who performed it is located.
Definition 1 (
(
W,Σ,Γ
)
-Confined Located Threads).
Consider an allowed-
policy mapping
W
, a reference labeling
Σ
, and a typing environment
Γ
.Aset
C
