Information Technology Reference
In-Depth Information
In the remaining rules of the operational semantics the annotations are ignored.
We refer to the mechanism that consists of statically annotating all threads in
a network according to the type and effect system of Figure 4, assuming that each
thread's declassification effect is allowed by its initial domain, using the seman-
tics of Figure 2 modified according to Rule (12), as
Enforcement mechanism III
.
Soundness.
We will now see that the declassification effect can be used for
enforcing confinement. The (
W,Σ,Γ
)-compatibility predicate that is used to
define confinement here requires all references
a
dom(
S
) to store a value that
results from annotating some other value
V
according to
Γ
∈
Σ
V
→
S
(
a
):
Σ
(
a
).
Theorem 3 (Soundness of Enforcement Mechanism III).
Consider a
fixed allowed-policy mapping
W
, a given reference labeling
Σ
and typing en-
vironment
Γ
, and a thread configuration
such that for all
M
m
P,T
∈
P
there
M
,
s
and
τ
such that
Γ
M
:
s,τ
and
W
(
T
(
m
))
P,T
Σ
M
exist
→
s
.Then
,
formed by annotating the threads in
P,T
,is
(
W,Σ,Γ
)
-confined.
Proof.
By showing that the following is a set of (
Σ,Γ
)-confined located threads
{d, M
m
M
:
s,τ
and
W
(
d
)
s}
(13)
Σ
M→
|m ∈
Nam
and
∃M,s,τ . Γ
M
:
s,τ
.
Σ
M
using induction on the inference of
Γ
→
Precision and eciency.
The relaxed type system of Subsection 5.2 for checking
confinement, and its informative counterpart of Figure 4, are strongly related.
The following result states that typability according to latter type system is
at least as precise as the former. It is proven by induction on the inference of
Γ
A
M
:
τ
.
Proposition 1.
Consider a given a typing environment
Γ
and reference labeling
Σ
.Ifthereexist
A
,
τ
such that
Γ
A
M
:
τ
, then there exist
M
,
τ
and
s
such
Σ
M
:
s,τ
and
A
Σ
M
τ
.
that
Γ
→
s
with
τ
The converse direction is not true, i.e. enforcement mechanism III accepts
strictly more programs than enforcement mechanism II. This can be seen by
considering the secure program where,
θ
1
=
τ
F
1
σ
and
θ
2
=
τ
F
2
−→
−→
σ
:
(if (!
a
)then(!(ref
θ
1
M
1
)) else (! (ref
θ
2
M
2
)))
(14)
This program is not accepted by the type system of Section 5.2 because it cannot
give the same type to both branches of the conditional (the type of the derefer-
ence of a reference of type
θ
is precisely
θ
). However, since the two types satisfy
θ
1
≈
θ
2
.
A more fundamental difference between the two enforcement mechanisms lays
in the timing of the computation overhead that is required by each mechanism.
While mechanism II requires heavy runtime type checks to occur each time a
thread migrates, in III the typability analysis is anticipated to static time, leaving
θ
2
, the informative type system can accept it and give it the type
θ
1
