Information Technology Reference
In-Depth Information
Theorem 2 (Soundness of Enforcement Mechanism II).
Consider a fixed
allowed-policy mapping
W
, a given reference labeling
Σ
and typing environment
Γ
,andathreadconfiguration
P,T
such that for all
M
m
∈
P
there exists
τ
such that
Γ
Σ
W
(
T
(
m
))
M
:
τ
.Then
P,T
is
(
W,Σ,Γ
)
-confined.
d,M
m
Σ
Proof.
By showing that the set
}
is a set of (
W,Σ,Γ
)-confined located threads, using induction on the inference
of
Γ
{
|
m
∈
Nam
and
∃
τ.Γ
W
(
d
)
M
:
τ
Σ
W
(
d
)
M
:
τ
.
Safety, precision and eciency.
The proposed mechanism does not offer a safety
result, guaranteeing that programs never “get stuck”. Indeed, the side condition
of the thread creation rule introduces the possibility for the execution of a thread
to block, since no alternative is given. This can happen in Example 3 (in page 28),
if the flow policy
F
is not permitted by the allowed policy of the domain of
the branch that is actually executed, then the migration will not occur, and
execution will not proceed. In order to have safety, we could design the thread
creation instruction as including an alternative branch for execution in case the
side condition fails. Nevertheless, Example 3 might have better been written
(thread (allowed
F
then (flow
F
in
M
1
) else
M
2
)at
d
)
(9)
in effect using the allowed condition for encoding such alternative behaviors.
Returning to Example 6 (in page 6), thanks to the relaxed Mig rule, this pro-
gram is now
always
accepted statically by the type system. Depending on the
result of the test, the migration might also be allowed to occur if a safe branch
is chosen. This means that enforcement mechanism II accepts more secure pro-
grams. Because of the possibility of blockage mentioned above, an information
flow analysis might reject some of the programs accepted here, in case for in-
stance the reference
a
is assigned a “high” security level, and a “low” write is
performed after the test. This issue is however orthogonal to our aims here.
A drawback with this enforcement mechanism lies in the computation weight
of the runtime type checks. This is particularly acute for an expressive language
such as the one we are considering. Indeed, recognizing typability of ML expres-
sions has exponential (worst case) complexity [11].
5.3 Static Informative Typing for Runtime Effect Checking
We have seen that bringing the type-based migration control of programs to run-
time allows to increase the precision of the confinement analysis. This is, how-
ever, at the cost of performance. It is possible to separate the program analysis
as to what are the declassification operations that are performed by migrating
threads, from the safety problem of determining whether those declassification
operations should be allowed at a given domain. To achieve this, we now present
an
informative
type system [8] that statically calculates a summary of all the
declassification operations that might be performed by a program, in the form of
a
declassification effect
. Furthermore, this type system produces a version of the
