Information Technology Reference
In-Depth Information
Σ
()
→
() :
,
unit
[Bt
I
]
Γ
Σ
tt →tt
:
,
bool
[Bf
I
]
Γ
Σ
ff →ff
:
,
bool
[Nil
I
]
Γ
Σ
a→ a
:
,Σ
(
a
)ref
Σ
x→ x
:
,τ
[Loc
I
]
Γ
[Var
I
]
Γ,x
:
τ
M
:
s,σ
X
:
s,τ
Σ
M→
Σ
X→
Γ,x
:
τ
Γ,x
:
τ
[Abs
I
]
[Rec
I
]
Σ
(
λx.M
)
→
(
λx. M
):
,τ
s
Σ
(
x.X
)
→
(
x. X
):
s,τ
Γ
Γ
→ σ
M
:
s,θ
θ
θ
M
:
s,θ
ref
Σ
M→
Σ
M→
Γ
Γ
[Ref
I
]
[Der
I
]
M
):
s,θ
ref
Σ
(!
M
)
→
(!
M
):
s,θ
Σ
(ref
θ
M
)
→
(ref
θ
Γ
Γ
M
:
s,θ
ref
Γ
N
:
s
,θ
θ
θ
Σ
M→
Σ
N→
[Ass
I
]
Γ
Σ
(
M
:=
N
)
→
(
M
:=
N
):
s
s
,
unit
Γ
M
:
s,τ Γ
N
:
s
,σ
Σ
M→
Σ
N→
[Seq
I
]
Γ
Σ
(
M
;
N
)
→
:
s
s
,σ
Γ
N
t
:
s
t
,τ
t
Σ
N
t
→
Γ
M
:
s,
bool
Σ
M→
Γ
τ
t
≈ τ
f
N
f
:
s
f
,τ
f
Σ
N
f
→
Γ
[Cond
I
]
M
then
N
t
else
N
f
):
s
s
t
s
f
,τ
t
τ
f
Σ
(if
M
then
N
t
else
N
f
)
→
(if
Γ
s
−→ σΓ
M
:
s,τ
N
:
s
,τ
τ
τ
Γ
Σ
M→
Σ
N→
[App
I
]
Σ
(
MN
)
→
(
M N
):
s
s
s
,σ
Γ
N
:
s,τ
Σ
N→
Γ
[Flow
I
]
(flow
F
in
N
):
s
Σ
(flow
F
in
N
)
Γ
→
F,τ
N
t
:
s
t
,τ
t
Σ
N
t
→
Γ
τ
t
≈ τ
f
[Allow
I
]
N
f
:
s
f
,τ
f
Σ
N
f
→
Γ
Σ
(allowed
F
then
N
t
else
N
f
)
→
(allowed
F
then
N
t
else
N
f
):
s
t
F
s
f
,τ
t
τ
f
Γ
M
:
s,
unit
Σ
M→
Γ
[Mig
I
]
Σ
(thread
M
at
d
)
→
(thread
s
M
at
d
):
,
unit
Γ
Fig. 4.
Informative Type and Effect System for obtaining the Declassification Effect
program that is annotated with the relevant information for deciding, at run-
time, whether its migrating threads can be considered safe by the destination
domain. The aim is to bring the overhead of the runtime check to static time.
The typing judgments of the type system in Figure 4 have the form:
M
:
s,τ
Σ
M
Γ
→
(10)
Comparing with the typing judgments of Subsection 5.2, while the flow policy
allowed by the context parameter is omitted from the turnstile '
', the security
effect
s
represents a flow policy which corresponds to the
declassification effect
:
a lower bound to the flow policies that are declared in the typed expression. The
second expression
M
is the result of annotating
M
. The syntax of annotated
expressions differs only in the thread creation construct, that has an additional
