Détail d'une fiche   Version PDF


Analyse sémantique et compilation pour la sécurité des environnements d'exécution


Statut: Décision signée

Responsable : Thomas Jensen

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2023" : A2.1. Langages de programmation , A2.2. Compilation , A2.2.1. Analyse statique , A2.2.5. Environnements d'exécution , A2.2.9. Sécurité par la compilation , A2.4. Méthodes formelles pour vérification, sureté, certification , A2.4.1. Analyse , A2.4.3. Preuves , A4.4. Sécurité des équipements et des logiciels , A4.5. Méthodes formelles pour la sécurité

Mots-clés de "B - Autres sciences et domaines d'application - 2023" : B6.1.1. Génie logiciel , B6.4. Internet des objets , B6.6. Systèmes embarqués

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/06/2022 -> 31/05/2026
Dates d'évaluation :

Etablissement(s) de rattachement : U. RENNES
Laboratoire(s) partenaire(s) : IRISA (UMR6074)

CRI : Centre Inria de l'Université de Rennes
Localisation : Centre Inria de l'Université de Rennes
Code structure Inria : 031135-0

Numéro RNSR : 202224278Y
N° de structure Inria: SR0922AR


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.

Axes de recherche

Semantic modeling of programing languages.

Semantics-based program analysis.

Verified compilation.

Security of execution environments

Relations industrielles et internationales

H2020 Cybersecurity network SPARTA

Salto: verification of a block chain written in OCam (collaboration with NomadicLabs)

ANR Scrypt : Secure cryptographic primitives