Action de Recherche Coopérative S-Java
Combination of formal tools
for verifying security properties of Java programs
01.01.2000-31.12.2001
Objectives
While Java designers put a lot of emphasis security-related issues for mobile
code on Internet, recent research has unveiled several flaws in
its security model. Yet Java has quickly become a standard for
Internet and (through Java Card) smartcard programming, putting
security issues at stake. It is therefore fundamental to develop
environments to verify the security of the Java platform and of
Java programs.
Thus far Java security has been instrumented with two main layers:
- proving safety properties of the language, in particular type
safety and properties related
to memory management. This first layer may be instrumented with
proof development systems, which are well-suited to
formalization and logical reasoning, but are ill-suited for
combinatorial reasoning based on exhaustive case-analysis;
- proving that a specific program obeys a
specific security policy, such as the sandbox security policy or
information-flow based security policies. This second layer
might be instrumented with a variety of tools such as
model-checkers. These latter allow to verify automatically
if a given program adheres to a given security policy.
The main goal of the S-Java action is to provide an environment that
integrates both layers and allows to prove security properties
for Java programs. One of the main challenges is to device
abstraction techniques which allow to construct finite,
preferably compact, abstract representations of Java programs
and to prove that the abstraction preserves the semantics of the
program for the property to be verified.
Participants
Meetings
- March 20th, INRIA Sophia-Antipolis. You may find here the
programme and list of participants.
- September 27th, INRIA Rocquencourt. You may find here the programme and list of participants.
- October 24th, INRIA Sophia-Antipolis. You may find here
the programme and list of participants.
Research themes
-
Formalisation of the JVM: we have been formalizing
substantial parts of the JVM in Coq. We plan to complete the
formalization, notably by including dynamic class loading
and multi-threading.
-
Specification of security policies: the Lande team has proposed a
general setting in which to specify
control-flow based security policies. We shall extend this
setting to data-flow so as to capture non-interference
properties. Second, we hope to develop compositional
techniques so as to handle dynamic class loading.
- Development and certification of abstractions: the ``Equipe
Sémantique'' of ENS has a long-standing experience in
abstract interpretation and been developing certified
abstract interpretations for a small imperative
language. On the other hand, the Lande and Oasis team have
been developing static analyses for imperative
object-oriented languages. We plan to integrate both trends
in the context of the JVM.
-
Combination of Coq with model-checkers: several architectures are
being envisaged. The first, simplest, alternative is to use
the model-checker as an oracle. A second alternative is to
translate the trace of the
model-checker into Coq proofs. However, this alternative is
unlikely to scale-up to real-size programs. A third, better
alternative consists of using reflexiom mechanisms; indeed,
the Coq team has been developing certified algorithms for
Binary Decision Diagrams. Yet another alternative is to
develop interactive abstractions in which abstractions are
built simulatenously with their proof of correction and the
model-checking process.
Related projects and events
Further information
For further information, please contact Gilles Barthe.