EPICURE

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.

Centre(s) inria

Centre Inria de l’Université de Rennes

En partenariat avec

Université de Rennes