Information Technology Reference
In-Depth Information
and eciency. In this paper we look closely at the problem of the overhead that
is implied by using types and effects for checking programs during runtime.
We study three type and effect-based mechanisms for enforcing confinement
that place different weight over static and run time: First, we present a purely
static type and effect system. Second, we increase its precision by letting most
of the control be done dynamically, at the level of the operational semantics.
To this end, the migration instruction is conditioned by a type check by means
of a standard type and effect checking system. Third, we provide a mechanism
for removing the runtime weight of typing migrating programs. It consists in
statically annotating programs with information about the declassifying behavior
of migrating threads, in the form of a
declassification effect
, and using it to
support ecient runtime checks.
This work is formulated over an expressive distributed higher-order imperative
lambda-calculus with remote thread creation. This language feature implies that
programs might need to comply to more than one dynamically changing allowed
flow policy simultaneously. The main contributions are:
1. A purely static type and effect system for enforcing flow policy confinement.
2. A type and effect system for checking migrating threads at runtime, that is
more precise than the one in point 1.
3. A static-time informative pre-processing type and effect system for annotat-
ing programs with a declassification effect, for a more ecient and precise
mechanism than the one in point 2.
We start by presenting the security setting (Section 2) and language (Sec-
tion 3). The formal security property of Flow Policy Confinement (Section4)
follows. Then, we study three type and effect-based enforcement mechanisms
(Section 5) and draw conclusions regarding their eciency and precision. Fi-
nally we discuss related work (Section 6) and conclude (Section 7). An extended
version of this article (available from the authors) presents the detailed proofs.
2 Security Setting
The study of confidentiality traditionally relies on a lattice of security levels [7],
corresponding to security clearances, that is associated to information contain-
ers in the programming language. The idea is that information pertaining to
references labeled with
l
2
can be legally transferred to references labeled with
l
1
only if
l
1
is at least as confidential as
l
2
. In this paper we do not deal explicitly
with security levels, but instead with
flow policies
that define how information
should be allowed to flow between security levels. Formally, flow policies can be
seen as downward closure operators over a basic lattice of security levels [8].
Flow policies
A,F
can be ordered according to their permissiveness by
means of a
permissiveness relation
∈
Flo
F
2
means that
F
1
is at least
as permissive as
F
2
. We assume that flow policies form a lattice that supports a
pseudo-subtraction operation
,where
F
1
Flo
,
,
,
,
,Ω,
, where: the meet operation
gives, for any two flow policies
F
1
,F
2
, the strictest policy that allows for
