Project-team

EPICURE

Semantic analysis and compilation for secure execution environments
Semantic analysis and compilation for secure execution environments

The frequent announcements of yet another cybersecurity breach show that the security of the software that surrounds us is, more than ever, a scientific challenge of utmost societal importance. More and more software is produced to operate on an increasingly varied number of devices and to provide increasingly complex functionality. The goal of the EPICURE project is to contribute with semantics-based methods for producing safe and secure software by

  • defining new semantic frameworks that will provide more accurate models of modern execution platforms, and which can facilitate the semantic definition of the above-mentioned multitude of programming languages,
  • designing formally verified analysis and compilation schemes, with the specific aim of being able to analyse and verify properties of programs written in high-level languages, and to compile both program and the verified properties down to low-level executable representations,
  • demonstrate the impact of language-based tools on software security by showing how they can improve the correctness, safety and security of critical software found in modern execution environments, such as the Java virtual machine, the Tezos blockchain written in OCaml, and small operating systems for the IoT such as RIOT.
Centre(s) inria
Inria Centre at Rennes University
In partnership with
Université de Rennes

Contacts

Team leader

Lydie Mabil

Team assistant