Certification de compilation Sure pour l'IoT – CISC

Depuis il y a une dizaine d'années, les chercheurs ont travaillé sur
la conception de langages multiniveaux pour le web. Un langage
multiniveau de programmation unifie dans un seul formalisme et un seul
environnement d'exécution la programmation des differents niveaux de
applications distribuées. Sur le web, ce paradigme unifie le client ,
le serveur, et la base de données. Dans ce projet, nous proposons la
conception et la mise en oeuvre d'une langage multiniveau pour
l'Internet des Objets (IoT), avec des abstractions de programmation de
microcontroleurs vers le cloud. La proposition comprend la conception
de renforts de sécurité par la compilation ainsi que le traitement des
questions de confidentialité par construction. En se fondant sur la
syntaxe JavaScript et les formalisations de Coq actuelles de la
sémantique JavaScript, nous prévoyons certifier le compilateur ainsi
que l'étude de compilation certifiant dans le contexte de l'IoT.