Skip to topic | Skip to bottom
... Mobius IST-15905

Start of topic | Skip to actions



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: