Information Technology Reference
In-Depth Information
through channels is called
explicit flow
[11] because it does not depend on the
specific information that flows. The information flow that occurs through the
control structure of a program (conditionals, loops, breaks, and exceptions) is
called an
implicit flow
[11] because it depends on the value of the condition that
guards the control structure. In this paper, we are interested in both explicit and
implicit flows for non-interference analysis of deterministic Java programs. How-
ever, we do not consider covert channels such as termination, timing, exceptions,
and resource exhaustion channels.
In [1,2], we proposed an abstract methodology for certifying safety properties
of Java source code. It is based on
Rewriting logic
(RWL) and is implemented
in Maude [8], which is a high-performance language that implements RWL. In
[1], we considered integer arithmetic properties that we analyzed as a safety
property, whereas in [2] we dealt with (local) non-interference of Java methods.
Non-interference is usually defined as a hyperproperty [7], i.e., a property de-
fined on a set of sets of traces, and cannot be established by simply checking
a (safety) property on a set of runs (essentially, no single run of a system can
violate non-interference). However, we are able to analyze non-interference by
observing a stronger property which can be checked as a safety
1
property using
an instrumented flow-sensitive semantics.
The methodology of [1,2] is as follows. Consider a Java program together with
a specification of the Java semantics. The Java program is a concrete expression
(i.e., term) that represents the initial state of the Java interpreter running the
considered Java program. The Java semantics is a specification in Maude. Given
a safety property (i.e., a system property that is defined in terms of certain
events that do not happen), the unreachability of the system states that denote
the events that should never occur allows us to infer the desired safety property.
Unreachability analysis is performed by using the standard Maude (breadth-
first) search command, which explores the entire state space of the program
from an initial system state. In the case where the unreachability test succeeds,
the corresponding rewriting proofs that demonstrate that those states cannot
be reached are delivered as the expected outcome certificate. We achieve a finite
search space by using abstraction [9]. This methodology is an instance of Proof-
carrying code (PCC), a mechanism originated by Necula [19] for ensuring the
secure behavior of programs.
This article provides a comprehensive and full-fledged formulation of the ab-
stract non-interference certification methodology of [2]. In that work, we focused
on the methodology as well as the PCC and rewriting-based particulars of our
approach with a specific emphasis on practicality and good performance. This
paper, however, formalizes more foundational semantic security aspects, namely:
(i) the characterization of non-interference as a safety property on extended
Java computations; (ii) the conditions required by Java programs in order to
ensure the correctness of our methodology; (iii) the observational capabilities
of an attacker; and (iv) the soundness of our abstract non-interference analysis
1
There are other approaches for proving non-interference as a safety property, which
use self-composition [10,5] or flow-sensitive security types [16].
