Information Technology Reference
In-Depth Information
Abstract Certification of Global
Non-interference in Rewriting Logic
Mauricio Alba-Castro
1
,
2
,Mar ıa Alpuente
1
, and Santiago Escobar
1
1
ELP-DSIC, U. Politecnica de Valencia, Spain
{
alpuente,sescobar
}
@dsic.upv.es
2
U. Autonoma de Manizales, Colombia
malba@autonoma.edu.co
Abstract.
Non-interference
is a semantic program property that as-
signs confidentiality levels to data objects and prevents illicit information
flows from occurring from high to low security levels. In this paper, we
present a novel security model for global non-interference which approx-
imates non-interference as a safety property. We also propose a certifica-
tion technique for global non-interference of complete Java classes based
on rewriting logic, a very general
logical
and
semantic framework
that is
eciently implemented in the high-level programming language Maude.
Starting from an existing Java semantics specification written in Maude,
we develop an extended, information-flow Java semantics that allows us
to correctly observe global non-interference policies. In order to achieve
a finite state transition system, we develop an abstract Java semantics
that we use for secure and effective non-interference Java analysis. The
analysis produces certificates that are independently checkable and are
small enough to be used in practice.
1
Introduction
Confidentiality is a property by which information that is related to an entity or
party is not made available or disclosed to unauthorized individuals, entities, or
processes. A
non-interference policy
[11] is a confidentiality policy that allows
programs to manipulate and modify confidential data as long as the observable
data generated by those programs do not improperly reveal information about
the confidential data, i.e., confidential data does not interfere with publicly ob-
servable data. Thus, ensuring that a program adheres to a non-interference policy
means analyzing how information flows within the program. The mechanism for
transfering information through a computing system is called a
channel
.Variable
updating, parameter passing, value return, file reading and writing, and network
communication are channels. Channels that use a mechanism that is not designed
for information communication are called
covert channels
[20]. There are covert
channels such as the control structure of a program, termination, timing, ex-
ceptions, and resource exhaustion channels. The information flow that occurs
This work has been partially supported by the EU (FEDER) and the Spanish
MEC/MICINN under grant TIN 2007-68093-C02-02.
