Information Technology Reference
In-Depth Information
for classes in [25], where the abstract value of a concrete object is its class. Two
objects (values) are indistinguishable at an abstraction level (class) if the objects
belong to the given class or if the given class is a superclass of object classes.
An algorithm for checking abstract non-interference of Java classes is proposed
that relies on class-based dependencies.
In previous work [2], we dealt with (local) non-interference of function meth-
ods regarding explicit inputs by parameter passing and explicit outputs by value
returning. The local non-interference policies considered there were required to
explicitly establish the confidentiality labels for all method parameters and vari-
ables. In this work, however, we consider global non-interference of complete
Java classes and we do not need to explicitly state the confidentiality level for
all program variables. In [2], we worked directly with an implementation level
definition of non-interference; in this work, we provide a general and language-
independent characterization as well as a formal and rigorous relation between
the approximate properties and the security model. As in [11,4,20,23,16], we take
into account implicit information flows by considering the context confidentiality
label in expression evaluation (the context label is joined with the confidential-
ity label of the expression) and also by modifying the context label during the
evaluation of guards of conditionals and while loops. Our global policies are very
flexible since the security levels of object variables, local variables, and method
parameters may change temporarily as in [16,23,4,14,5].
8Conluon
In this paper, we formalize a framework for automatically certifying global non-
interference of Java programs. Our methodology relies on an (abstract) extended
semantics for Java written in rewriting logic that can be model-checked in Maude
by using Maude's breadth-first search space exploration. In the extended seman-
tics, non-interference becomes a safety property, and we formally demonstrate
that the safety property in the extended semantics entails the semantic, non-
interference security property in the standard Java semantics. In this work, we
provide a general and abstract definition as well as a rigorous link between
the approximate properties and the security model that we consider, whereas
in our previous work [2], we worked directly with a program-level definition of
non-interference. The proposed framework fully accounts for explicit as well as
implicit flows, and allows not only the inference of rewriting logic safety proofs
but also the checking of existing ones, thus providing support for proof-carrying
code. Actually, the steps that the abstract semantics takes are recorded in order
to construct a certificate ensuring that the program satisfies the desired prop-
erty. By turning a potentially infinite labelled state space of a Java program
into a finite abstract space, the abstract semantics not only makes the approach
feasible, but also greatly reduces the size of the certificates that must be checked
on the consumer's end.
The Java operational semantics in rewriting logic that we have used is modular
and has 2635 lines of code in 4 files [12]. We have modified less than 20 of the
