Address
Project Everest
INRIA Sophia-Antipolis
2004, Route des Lucioles
BP 93
06902 Sophia-Antipolis
 Verification and Security of Software |
The project's privileged application domain ranges from trusted personal devices, such as mobile phones and smart cards, to ubiquitous computing.
The project focuses on the following research themes:
- Program verification and Proof Carrying Code
- Machine-checked semantics and algorithms
- Foundations of proof assistants
Program verification and Proof
Carrying Code
To ensure safety and security of software we study different verification techniques, notably program logics and type systems. We focus on particular paradigms for mobile code security, in particular Proof Carrying Code.
Current topics of interest include:
- Information flow type systems: we develop information flow
type systems for the Java Virtual Machine, and establish
type-preserving compilation results between our type system and
information flow type systems for Java source code programs.
- Security by logic: we devise methods that
use program logics to enforce security policies
such as non-interference, resource control, or high-level security
rules found in industrial security policies. Further, we also study
compositional verification techniques.
- Certificate translation: we provide means to bring the benefits of source code verification to code consumers, via certificate translators that transform certificates (as in Proof Carrying Code) of source code programs into certificates of byte code programs. Our certificate translators apply to non-optimizing compilers as well as to compilers that perform standard program optimizations.
- Verification of multi-threaded programs: specification languages and program logics are extended to multi-threading. We pay particular attention to techniques that allow to simplify reasoning, preferably by reducing it to sequential verification problems. As a first point of interest we study immutable objects, thread-local objects and atomicity properties.
- JACK (Java Applet Correctness Kit), an environment for the verification of annotated Java programs. The programs are written in either source code or byte code, their annotations are written using JML or its byte code equivalent, as developed within the Everest project.
- Verification of system components.
Machine-checked semantics and algorithms
We use proof assistants to model and verify programming language
semantics and cryptographic
algorithms.Current topics of interest include:
- Machine checked type systems and static analyses. We develop certified static analyses for the Java Card platform; in order to facilitate our work, we also develop the Jakarta toolset, that provides automatic tool support for large parts of the verification task.
- Verification of cryptographic algorithms. We develop machine checked formalisations of provable security to show the security of cryptographic schemes. In particular, we use the Generic Model and Random Oracle Model to prove security bounds for cryptosystems based on the discrete logarithm.
Earlier work includes the formalization of the JavaCard platform, and
of the GlobalPlatform specifications. We also participated in a
collaborative effort to verify a moderately optimizing compiler for C--.
Foundations of proof assistants
We study means to improve the usability and robustness of proof assistants, both from a theoretical perspective and from an implementation point of view.Current topics of interest include:
- type-based termination, an approach that advocates the use of size types to guarantee termination of recursive definitions;
- reflective tactics;
- efficient convertibility checking.