Information Technology Reference
In-Depth Information
both
F
1
and
F
2
; the join operation
gives, for any two flow policies
F
1
,F
2
,
the most permissive policy that only allows what both
F
1
and
F
2
allow; the
most restrictive flow policy
does not allow any information flows; and the
most permissive flow policy
Ω
that allows all information flows. Finally, the
pseudo-subtraction operation
between two flow policies
F
1
and
F
2
(used only
in Subsection 5.3) represents the most permissive policy that allows everything
that is allowed by the first (
F
1
), while excluding all that is allowed by the second
(
F
2
); it is defined as the relative pseudo-complement of
F
2
with respect to
F
1
,
i.e. the greatest
F
such that
F
F
1
.
Considering a concrete example of a lattice of flow polices that meets the
abstract requirements defined above can provide helpful intuitions. Flow policies
that operate over the security lattice where security levels are sets of principals
p,q
F
2
provide such a case. In this setting, security levels are ordered by
means of the flow relation
∈
Pri
⊇
. Flow policies then consist of binary relations on
Pri
, which can be understood as representing additional directions in which
information is allowed to flow between principals: a pair (
p,q
)
∈
F
,mostoften
written
p
q
, is to be understood as “information may flow from
p
to
q
”. New
more permissive security lattices are obtained by collapsing security levels into
possibly lower ones, by closing them with respect to the valid flow policy. Writing
F
1
≺
F
2
means that
F
1
allows flows between at least as many pairs of principals
as
F
2
. The relation is here defined as
F
1
F
1
(where
F
∗
denotes
the reflexive and transitive closure of
F
): The meet operation is then defined as
F
2
iff
F
2
⊆
F
2
=
F
1
∩
F
2
, the top flow policy
=
∪
, the join operation is defined as
F
1
is given by
=
∅
, the bottom flow policy is given by
Ω
=
Pri
×
Pri
,andthe
pseudo-subtraction operation is given by
=
−
.
3 Language
The language extends an imperative higher order lambda calculus that includes
reference and concurrent thread creation, a declassification construct, and a
policy-context testing construct, with basic distribution and code mobility fea-
tures. Computation domains hold a local allowed flow policy, which imposes a
limit on the permissiveness of the declassifications that are performed within the
domain. A remote thread creation construct serves as a code migration primitive.
Variables
Reference Names
x
a
∈
∈
Var
Ref
Flow Policies
A,F ∈
Flo
Domain Names
d ∈
Dom
Values
V
∈
Val
::= ()
| x | a |
(
λx.M
)
| tt | ff
Pseudo-values
X ∈
Pse
::=
V |
(
x.X
)
Expressions
M,N ∈
Exp
::=
X |
(
MN
)
|
(
M
;
N
)
|
(if
M
then
N
t
else
N
f
)
|
(ref
θ
M
)
|
(!
N
)
|
(
M
:=
N
)
|
(flow
F
in
M
)
|
(allowed
F
then
N
t
else
N
f
)
|
(thread
M
at
d
)
Fig. 1.
Syntax of Expressions
