Information Technology Reference
In-Depth Information
of located threads is a set of
(
W,Σ,Γ
)-
confined located threads
if the following
holds for all
d,M
m
∈C
, for all
T
such that
T
(
m
)=
d
,andforall
(
W,Σ,Γ
)
-
compatible memories
S
:
Σ
M
m
M
m
,T
,S
-
W
{
}
,T,S
F
{
}
implies
W
(
T
(
m
))
F
and also
T
(
m
)
,M
m
.Furthermore,
S
is still
(
W,Σ,Γ
)
-compatible.
∈C
Σ
M
m
M
m
,N
n
,T
,S
-
W
{
}
,T,S
F
{
}
implies
W
(
T
(
m
))
F
and also
T
(
m
)
,M
m
T
(
n
)
,N
n
.Furthermore,
S
is still
(
W,Σ,Γ
)
-compatible.
,
∈C
Note that for any
W
,
Σ
,and
Γ
there exists a set of (
W,Σ,Γ
)-confined located
threads, like for instance
). Furthermore, the union of a
family of sets of (
W,Σ,Γ
)-confined located threads is a set of (
W,Σ,Γ
)-confined
located threads. The largest set of (
W,Σ,Γ
)-confined threads is denoted by
C
Dom
×
(
Val
×
Nam
Σ,Γ
W
.
We say that a thread
M
m
is (
W,Σ,Γ
)-confined when located at
d
,if
d,M
m
∈
Σ,Γ
W
.Awellformed
thread configuration
C
P,T
, satisfying the applicable rules
of a well formed configuration, is said to be (
W,Σ,Γ
)-confined if all located
threads in
{T
(
m
)
,M
m
|M
m
∈ P}
are (
W,Σ,Γ
)-confined.
Notice that this property speaks strictly about what
flow declarations
athread
can do
while
it is at a specific domain. In particular, it does not restrict threads
from migrating to more permissive domains in order to perform a declassification.
More importantly, the property does not deal with information flows. So for
instance it offers no assurance that information leaks that are encoded at each
point of the program do obey the declared flow policies for that point. Such an
analysis can be done independently, cf.
non-disclosure
in [9].
5 Enforcement Mechanisms
In this section we start by studying a type system for statically ensuring that
global computations always comply to the locally valid allowed flow policy. This
type system is inherently restrictive, as the domains where each part of the code
will actually compute cannot in general be known statically (Subsection 5.1). We
then present a more precise type system to be used at runtime by the semantics
of the language for checking migrating threads against the allowed flow policy of
the destination domain (Subsection 5.2). Finally, we propose a yet more precise
type and effect system that computes information about the declassification
behaviors of programs. This information will be used more e
ciently at runtime
by the semantics of the language in order to control migration of programs.
5.1 Purely Static Type Checking
We have seen that in a setting where code can migrate between domains with
different allowed security policies, the computation domain might change
during
computation, along with the allowed flow policy that the program must comply
to. This can happen in particular within the branch of an allowed condition:
(allowed
F
then (thread (flow
F
in
M
1
)at
d
) else
M
2
)
(3)
