Information Technology Reference
In-Depth Information
5.2 Runtime Type Checking
In this subsection we study a hybrid mechanism for enforcing confinement, that
makes use of a relaxation of the type system of Figure 3 during runtime. Migra-
tion is now controlled by means of a runtime check for typability of migrating
threads with respect to the allowed flow policy of the destination domain. The
condition represents the standard theoretical requirement of checking incoming
code before allowing it to execute in a given machine.
The relaxation is achieved by replacing rule Mig by the following one:
Γ
Ω
M
:
unit
(7)
[Mig]
Γ
A
(thread
M
at
d
):
unit
The new type system no longer imposes
future
migrating threads to conform to
the policy of their destination domain, but only to the most permissive allowed
flow policy
Ω
. The rationale is that it only worries about confinement of the
non-migrating parts of the program. This is sucient, as all threads that are to
be spawned by the program will be re-checked at migration time.
The following modification to the migration rule of the semantics of Figure 2
introduces the runtime check that controls migration (
n
fresh in
T
). The idea is
that a thread can only migrate to a domain if it respects its allowed flow policy:
W
(
d
)
N
:
unit
Γ
(8)
E[(thread
N
at
d
)]
m
n
−−→
E[()]
m
,N
n
W
Σ
{
}
,T,S
{
}
,
[
n
:=
d
]
T,S
E
The new remote thread creation rule (our migration primitive), now depends on
typability of the migrating thread. The typing environment
Γ
(which is constant)
is now an implicit parameter of the operational semantics. If only closed threads
are considered, then also migrating threads are closed. The allowed flow policy
of the destination site now determines whether or not a migration instruction
may be consummated, or otherwise block execution.
Notice that, thanks to postponing the migration control to runtime, the type
system no longer needs to be parameterized with information about the allowed
flow policies of all domains in the network, which in practice could be impossible.
The only relevant one are those of the destination domain of migrating threads.
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
modified using the new Mig rule represented in Rule (8), with respect to the
allowed flow policies of each thread's initial domain, using the semantics of Fig-
ure 2 modified according to Rule (7), as
Enforcement mechanism II
.
Soundness.
Enforcement mechanism II guarantees security of networks with
respect 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
Σ
∈
dom(
S
)tostoreavaluesatisfying
Γ
S
(
a
):
Σ
(
a
).
