Action de Recherche Coopérative S-Java

Combination of formal tools

for verifying security properties of Java programs



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: 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.



Research themes

Related projects and events

Further information

For further information, please contact Gilles Barthe.