Information Technology Reference
In-Depth Information
Focusing on declassification control, the idea of using a notion of declassifica-
tion effect for building a runtime migration control mechanism was put forward
in [6] for a similar language with local thread creator and a basic goto migration
instruction. In spite of the restrictions that are pointed out in Subsection 5.1
for a static analysis, the type system presented as part of Enforcement Mech-
anism I is more refined than the proof-of-concept presented earlier. Indeed, in
the previous work, migration was not taken into account when analyzing the de-
classifications occurring within the migrating code. So while there the following
program would be rejected if
F
was not allowed by
W
(
d
1
)
(thread (thread (flow
F
in
M
)at
d
2
)at
d
1
)
(15)
the type system of Figure 3 only rejects it if
F
is not allowed by
W
(
d
2
). En-
forcement Mechanism II adopts part of the idea in [6] of performing a runtime
type analysis to migrating programs, but uses a more permissive “checking” type
system. Enforcement Mechanism III explores a mechanism that allows to take
advantage of the eciency of flow policy comparisons. It uses a type and effect
system for calculating declassification effects that is substantially more precise
than previous ones, thanks to the matching relations and operations that it uses.
The concept of informative type and effect system was introduced in [8], where
a different notion of declassification effect was defined and applied to the problem
of dealing with dynamic updates to a local allowed flow policy.
7Con lu on
We have considered an instance of the problem of enforcing compliance of declas-
sifications to a dynamically changing allowed flow policy. In our setting, changes
in the allowed flow policy result from the migration of programs during execu-
tion. We approach the problem from a migration control perspective. To this
end, we chose a network model that abstracts away the details of the migration
control architecture. This allows us to prove soundness of a concrete network
level security property, guaranteeing that programs can roam over the network,
never performing declassifications that violate the network confinement property.
While our results are formulated for a particular security property - flow pol-
icy confinement - we expect that similar ideas can be used for other properties.
One could add expressiveness to the property by taking into account the history
of domains that a thread has visited when defining secure code migrations. For
instance, one might want to forbid threads from moving to domains with more
favorable allowed flow policies. This would be easily achieved by introducing a
condition on the allowed flow policies of origin and destination domains.
By performing comparisons between three related enforcement mechanisms,
we have argued that the concept of declassification effect offers a good balance
between precision and eciency. We believe that similar mechanisms can be
applied in other contexts. For future work, we plan to study others instances of
enabling dynamic changing allowed flow policies.
