Profile
INRIA is a French public-sector scientific and technological institute operating under the dual authority
of the Ministry of Research and the Ministry of Industry.
INRIA’s missions are “to undertake basic and applied research, to design experimental systems, to ensure technology and knowledge transfer, to organize international scientific exchanges, to carry out scientific assessments, and to contribute to standardization”.
The research carried out at INRIA brings together experts from the fields of computer science and applied
mathematics. INRIA gathers in its premises around 3,200 persons including 2,400 scientists, many of
which belong to partner organizations (CNRS, industrial labs, universities). A large number of INRIA
senior researchers are involved in teaching and their PhD students (about 800) prepare their thesis within
the different INRIA research projects (over 100).
Industrial relations are strategic for INRIA: numerous industrial partners, French or foreign, contract
with the Institute for collaborative research.
INRIA is a member of ERCIM EEIG, the European Research Consortium for Computer Science and
Mathematics. Outside Europe, INRIA also has a significant activity: it has created joint research laboratories
(in Russia and China), signed cooperation agreements (with NSF, India, Brazil, etc.) and promotes
intensive scientific exchanges.
Fields of expertise
The research team involved in the MOBIUS project spans over three INRIA research teams (EVEREST
at INRIA Sophia Antipolis, LANDE at IRISA, and PARSIFAL at INRIA Futurs) resulting in a unique
blend of competences in the areas of security, Proof Carrying Code, type-based and logic-based analysis
of programs, and formal methods.
The
Everest research team aims at ensuring system security for mobile applications. Its work
concentrates on the development and validation of secure software, both at platform and application
level. Its privileged application domains are small, trusted and portable devices, their operating systems
and the applications running on these devices. The team most recent work includes the development
of the verification environment JACK, the design of type systems (information flow type systems) and
logical verification methods (weakest precondition calculi) for low-level languages, and the study of proofpreserving
and type-preserving compilers.
The
Lande research team has a long-standing expertise in static program analysis and verification.
The main application domain of these techniques is software security, in particular security of Java and Java
Card applications, for which the team has developed an approach to verifying security properties based
on control flow and model checking. Recent work include the certification and the extraction of a static
analyser using the proof assistant Coq, a control flow analysis for fragments of object-oriented programs
and a modular analysis techniques for verifying behavioural properties of code fragments intended for
download.
The
Parsifal research team has developed significant strengths in the areas of formal methods,
particularly applied to specifying and reasoning with operational semantics and with the structure and
search of proofs. Recent research work of the team has allowed the development of a number of effective
tools for mixing deduction and computation closely, as is often done in systems such as symbolic model
checking, symbolic bisimulation, type checkers, and Proof Carrying Code. Several aspects of the MOBIUS
proposal can make effective use of this line of research and of the prototype systems that the team has
either built or plans to build.
Projects Links: