EPICURE

Les annonces fréquentes d'une énième brèche dans la 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. Ces logiciels sont produits pour fonctionner sur un nombre de plus en plus varié d'appareils et de fournir des fonctionnalités de plus en plus complexes. 

L'objectif du projet EPICURE est de concevoir des méthodes sémantiques pour produire des logiciels sûrs et sécurisés en définissant de nouveaux cadres sémantiques qui fourniront des modèles plus précis de plates-formes d'exécution.  Cela nous servira à modéliser des propriétés de sûreté et de sécurité liées au contrôle de flux d'information et aux canaux auxiliaires, ainsi que de concevoir des analyses statiques et des schémas de compilation formellement
vérifiés. 

Notre but est d'être en mesure d'analyser et de 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'à l'exécutable de bas niveau.  Nous démontrerons l'impact de ces outils sur la correction, la sûreté et la sécurité des logiciels critiques trouvés dans les environnements d'exécution, tels que la machine virtuelle Java, la blockchain Tezos écrite en OCaml et les systèmes d'exploitation pour l'IoT comme RIOT.