Information Technology Reference
In-Depth Information
only a comparison between two flow policies to be performed at migration time.
The complexity of this comparison depends on the concrete representation of
flow policies. In the worst case, that of flow policies as general downward closure
operators (see Section 2), it is linear on the number of security levels that are
considered. When flow policies are flow relations, then it consists on a subset
relation check, which is polynomial on the size of the flow policies.
6 Related Work
Controlling declassification.
Most previous mechanisms for controlling declassi-
fication [12] target flexible versions of an information flow property. Departing
from this approach, the work by Boudol and Kolundzija [13] on combining access
control and declassification is the first to treat declassification control separately
from the underlying information flow problem. In [13], standard access control
primitives are used to control the access level of programs that perform declas-
sifications in the setting of a local language, ensuring that a program can only
declassify information that it has the right to read.
Controlling code mobility.
A wide variety of distributed network models have
been designed with the purpose of studying mechanisms for controlling code
mobility. These range from type systems for statically controlling migration as
an access control mechanism [5,14], to runtime mechanisms that are based on
the concept of programmable domain. In the latter, computing power is explic-
itly associated to the
membranes
of computation domains, and can be used for
controlling boundary transposition. This control can be performed by processes
that interact with external and internal programs [15,16,4], or by more specific
automatic verification mechanisms [17]. In the present work we abstract away
from the particular machinery that implements the migration control checks,
and express declaratively, via the language semantics, the condition that must
be satisfied for the boundary transposition to be allowed.
Checking the validity of the declassification effect as a certificate is not simpler
than checking the program against a concrete allowed policy (as presented in
Subsection 5.2), meaning that it does not consist of a case of Proof Carrying
Code. The concept of trust can be used to lift the checking requirements of
code whose history of visited domains provides enough reassurance [17,5]. These
ideas could be applied to the present work, assisting the decision of trusting the
declassification effect, otherwise leading to a full type check of the code.
Hybrid mechanisms.
The use of hybrid mechanisms for enforcing information
flow policies is currently an active research area (see [18] for a review of related
work). The closest to ours is perhaps the study of securing information release
for a simple language with dynamic code evaluation in the form of a string eval
command, which includes an on-the-fly information flow static analysis [19].
