Information Technology Reference
In-Depth Information
flow policy
F
as parameter, written (thread
F
M
at
d
). The syntax of types is
the same as the ones used in Subsections 5.1 and 5.2.
It is possible to relax the type system by matching types that have the same
structure, even if they differ in flow policies pertaining to them. We achieve this
by overloading
to relate types where certain latent effects in the first are at
least as permissive as the corresponding ones in the second. The more general
relation
≈
matches types where certain latent effects differ: Finally, we define an
between two types
τ
and
τ
such that
τ
τ
:
operation
≈
σ
and
τ
=
θ
F
τ
iff
τ
=
τ
,
or
τ
=
θ
F
σ
with
F
F
and
σ
σ
τ
−→
−→
σ
and
τ
=
θ
F
τ
iff
τ
=
τ
,
or
τ
=
θ
F
σ
with
σ
σ
τ
≈
−→
−→
≈
(11)
!
τ
=
τ,
if
τ
=
τ
,
or
θ
F
F
σ
and
τ
=
θ
F
σ
,
if
τ
=
θ
F
σ
τ
−−−→
σ
−→
−→
The
relation is used in rules Ref
I
, Ass
I
andApp
I
, in practice enabling to
associate to references and variables (by reference creation, assignment and ap-
plication) expressions with types that contain stricter policies than required by
the declared types. The relation
≈
is used in rules Cond
I
andAllow
I
in order
to accept that two branches of the same test construct can differ regarding some
of their policies. Then, the type of the test construct is constructed from both
using
, thus reflecting the flow policies in both branches.
The declassification effect is constructed by aggregating (using the meet oper-
ation) all relevant flow policies that are declared within the program. The effect
is updated in rule Flow
I
, each time a flow declaration is performed, and “grows”
as the declassification effects of sub-expressions are met in order to form that of
the parent command. However, when a part of the program is “protected” by an
allowed condition, some of the information in the declassification effect can be
discarded. This happens in rule Allow
I
, where the declassification effect of the
first branch is not used entirely: the part that will be tested during execution
by the allowed-condition is omitted. In rule Mig
I
, the declassification effect of
migrating threads is also not recorded in the effect of the parent program, as
they will be executed (and tested) elsewhere. That information is however used
to annotate the migration instruction.
One can show that the type system is deterministic, in the sense that it
assigns to a non-annotated expression a single annotated version of it, a single
declassification effect, and a single type.
Modified operational semantics, revisited.
By executing annotated programs, the
type check that conditions the migration instruction can be replaced by a simple
declassification effect inspection. The new migration rule is similar to the one in
Subsection 5.2, but now makes use of the declassification effect (
n
fresh in
T
):
W
(
d
)
s
(12)
n
−−→
E[(thread
s
N
at
d
)]
m
E[()]
m
,N
n
Σ
W
{
}
,T,S
E
{
}
,
[
n
:=
d
]
T,S
