Détail d'une fiche   Version PDF

EPICURE (SR0922AR)

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

CELTIQUE (SR0327HR) →  EPICURE


Statut: Décision signée

Responsable : Thomas Jensen

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2024" : 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 - 2024" : 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

Présentation

Les fréquentes annonces d’une énième faille de cybersécurité montrent que la sécurité des logiciels qui nous entourent est, plus que jamais, un défi scientifique de la plus haute importance sociétale. De plus en plus de logiciels sont produits pour fonctionner sur un nombre de plus en plus varié d'appareils et pour fournir des fonctionnalités de plus en plus complexes. L'objectif du projet EPICURE est de contribuer avec des méthodes basées sur la sémantique à la production de logiciels sûrs et sécurisés. Plus précisément, nous proposons de 
  •   définir de nouveaux cadres sémantiques qui fourniront des modèles plus précis de plates-formes d'exécution modernes et qui pourront faciliter la définition sémantique de la multitude de langages de programmation mentionnés ci-dessus,
  •   concevoir des schémas d'analyse et de compilation formellement vérifiés, dans le but spécifique de pouvoir analyser et vérifier les propriétés de programmes écrits dans des langages de haut niveau, et de compiler à la fois le programme et les propriétés vérifiées jusqu'à des représentations exécutables de bas niveau,
  •   démontrer l'impact des outils basés sur le langage sur la sécurité des logiciels en montrant comment ils peuvent améliorer l'exactitude, la sûreté et la sécurité des logiciels critiques trouvés dans les environnements d'exécution modernes, tels que la machine virtuelle Java, la blockchain Tezos écrite en OCaml et les petits systèmes d'exploitation pour l'IoT comme RIOT.
 

Axes de recherche

  • Modélisation sémantique des langages de programmation.
  • Analyse de programme basée sur la sémantique.
  • Compilation vérifiée.
  • Sécurité des environnements d'exécution

Relations industrielles et internationales

PEPR Cybersecurity "Secureval"

Salto: verification du block chain Tezos écrit en OCam (collaboration avec NomadicLabs)