Information Technology Reference
In-Depth Information
Σ
A
() :
unit
Σ
A
tt
:
bool
Σ
A
ff
:
bool
[Nil]
W
;
Γ
[Bt]
W
;
Γ
[Bf]
W
;
Γ
Σ
A
a
:
Σ
(
a
)ref
Σ
A
x
:
τ
[Loc]
W
;
Γ
[Var]
Γ,x
:
τ
A
M
:
σ
A
X
:
τ
W
;
Γ,x
:
τ
[Rec]
W
;
Γ,x
:
τ
[Abs]
A
−→ σ
Σ
A
(
x.X
):
τ
Σ
A
(
λx.M
):
τ
W
;
Γ
W
;
Γ
Σ
A
M
:
θ
Σ
A
M
:
θ
ref
W
;
Γ
W
;
Γ
[Der]
W
;
Γ
[Ref]
Σ
A
(ref
θ
M
):
θ
ref
Σ
A
(!
M
):
θ
W
;
Γ
Σ
A
M
:
θ
ref
W
;
Γ
Σ
A
N
:
θ
Σ
A
M
:
τW
;
Γ
Σ
A
N
:
σ
[Ass]
W
;
Γ
[Seq]
W
;
Γ
A
(
M
:=
N
):
unit
A
(
M
;
N
):
σ
W
;
Γ
W
;
Γ
Σ
A
N
t
:
τ
W
;
Γ
A
M
:
bool
W
;
Γ
Σ
A
N
f
:
τ
W
;
Γ
[Cond]
Σ
A
(if
M
then
N
t
else
N
f
):
τ
W
;
Γ
A
−→ σW
;
Γ
Σ
A
M
:
τ
Σ
A
N
:
τ
W
;
Γ
Σ
A
N
:
τA
W
;
Γ
F
[App]
[Flow]
Σ
A
(
MN
):
σ
Σ
A
(flow
F
in
N
):
τ
W
;
Γ
W
;
Γ
Σ
A
F
N
t
:
τ
W
;
Γ
W
;
Γ
Σ
A
N
f
:
τ
[Allow]
Σ
A
(allowed
F
then
N
t
else
N
f
):
τ
W
;
Γ
Σ
W
(
d
)
M
:
unit
W
;
Γ
[Mig]
Σ
A
(thread
M
at
d
):
unit
W
;
Γ
Fig. 3.
Type and effect system for checking Confinement
In this program, the flow declaration of the policy
F
is executed only if
F
has
been tested as being allowed by the domain where the program was started.
It might then seem that the flow declaration is “protected” by an appropriate
allowed construct. However, by the time the flow declaration is performed, the
thread is already located at another domain, where that flow policy might not be
allowed. It is clear that a static enforcement of a confinement property requires
tracking the possible locations where threads might be executing at each point.
Figure 3 presents a new type and effect system [10] for statically enforcing
confinement over a migrating program. The type system guarantees that when
operations are executed by a thread within the scope of a flow declaration, the
declared flow complies to the allowed flow policy of the current domain. The
typing judgments have the form
Σ
A
M
:
τ
W
;
Γ
(4)
meaning that expression
M
is typable with type
τ
in typing context
Γ
:
Var
→
Typ
, which assigns types to variables. In addition to the reference mapping
Σ
,
the turnstile has as parameter the flow policy
A
that is
allowed by the context
,
which includes all flow policies that have been positively tested by the program
