Information Technology Reference
In-Depth Information
as being allowed at the computation domain where the expression
M
is running.
Finally,
W
represents the mapping of domain names to allowed flow policies.
Types have the standard syntax (
t
is a type variable)
τ
A
τ,σ,θ
∈
Typ
::=
t
|
unit
|
bool
|
θ
ref
|
−→
σ
(5)
wherethereferencetyperecordsthetype
θ
of values that the reference contains,
and the functional type records the latent allowed policy
A
that is used to type
the application of the function to an argument.
Our type system applies restrictions to programs in order to ensure that
flow declarations can only declare flow policies that are allowed by the con-
text (rule Flow). These restrictions are relaxed when typing the first branch of
allowed conditions, by extending the flow policy allowed by the context with the
policy that guards the condition (rule Allow). In rule Mig, the flow policy al-
lowed by the context is adjusted to that of the destination computation domain
W
(
d
) that is specified by the (thread
M
at
d
)construct.
Note that if an expression is typable with respect to an allowed flow policy
A
,
then it is also so for any more permissive allowed policy
A
. In particular, due
to the Abs rule, the process of typing an expression is not deterministic. For
instance, the expression (
λx.
()) can be given any type of the form
τ
F
unit
.
We refer to the enforcement mechanism that consists of statically type check-
ing all threads in a network according to the type and effect system of Figure 3,
with respect to the allowed flow policies of each thread's initial domain, using
the semantics represented in Figure 2, as
Enforcement mechanism I
.
−→
Soundness.
Enforcement mechanism I guarantees security of networks with re-
spect to confinement, as is formalized by the following result. The (
W,Σ,Γ
)-
compatibility predicate that is used to define confinement here requires all ref-
erences
a
Σ
S
(
a
):
Σ
(
a
).
Theorem 1 (Soundness of Enforcement Mechanism I).
Consider a fixed
allowed-policy mapping
W
, a given reference labeling
Σ
and typing environment
Γ
,andathreadconfiguration
∈
dom(
S
)tostoreavaluesatisfying
W
;
Γ
such that for all
M
m
P,T
∈
P
there exists
τ
Σ
such that
W
;
Γ
W
(
T
(
m
))
M
:
τ
.Then
P,T
is
(
W,Σ,Γ
)
-confined.
Proof.
By showing that the set
{d,M
m
W
(
d
)
M
:
τ}
is a set of (
W,Σ,Γ
)-confined located threads, using induction on the inference
of
W
;
Γ
|m ∈
Nam
and
∃τ.W
;
Γ
Σ
W
(
d
)
M
:
τ
.
Precision.
Given the purely static nature of this migration control analysis, some
secure programs are bound to be rejected. There are different ways to increase
the precision of a type system, which are all intrinsically limited to what can
conservatively be predicted before runtime. For example, for the program
(if (!
a
) then (thread (flow
F
in
M
)at
d
1
) else (thread (flow
F
in
M
)at
d
2
)) (6)
it is in general not possible to predict which branch will be executed (or, in
practice, to which domain the thread will migrate), for it depends on the contents
of the memory. It will then be rejected if
W
(
d
2
)
F
or
W
(
d
1
)
F
.
