Une chaîne de compilation vérifiée pour WebAssembly

WebAssembly (Wasm) est un langage de bas niveau portable qui est devenu un standard industriel pour exécuter efficacement des applications dans les navigateurs Web, ainsi que dans les environnements côté serveur et edge computing. Wasm représente des instructions proches de l’assembleur, mais abstraites de l’architecture matérielle. Chaque instruction est typée et vérifiable, ce qui garantit la sécurité et la portabilité. Il fournit en particulier des garanties fortes d'isolation mémoire, ce qui est crucial pour la sécurité des applications web et cloud. WebAssembly permet d’écrire des programmes dans des langages comme C, C++, Rust ou Go, puis de les compiler vers Wasm pour être exécutés presque aussi vite que du code natif, tout en restant sûr et isolé.

Nous nous intéresserons dans cette thèse à la conception d’une chaîne de compilation vérifiée partant du langage C et ciblant Wasm. Cette chaîne de compilation s’appuiera sur le compilateur vérifié CompCert et un des objectifs de la thèse sera de développer un back-end vérifié depuis un des langages intermédiaires de CompCert vers Wasm. Les langages envisagés sont RTL (code bas niveau 3-adresses impliquant des registres et la mémoire) ou Cminor (qui est plus proche du C et dispose de boucles comme Wasm). Le back-end comprendra une série de passes de compilation (de traduction et d’optimisation) dont certaines pourront opérer sur de nouveaux langages intermédiaires à définir. Enfin, la chaîne de compilation finale et le backend seront évalués expérimentalement sur des bancs de tests de l’état de l’art et les résultats seront comparés à ceux obtenus avec d’autres backends Wasm non vérifiés. Cette thèse comprend donc à la fois une partie théorique (raisonnement sémantique nécessaire pour démontrer la correction du compilateur) et une partie pratique (validation expérimentale à mener sur des programmes réalistes et comparaison par rapport à des backends de l’état de l’art).

Le thèse se déroulera en deux étapes successives.

1. Définition d'un back-end vérifié, démontrant formellement l'équivalence du code Wasm généré avec le langage intermédiaire d'origine, sans chercher à optimiser fortement le code généré. Cette première étape sera séparée en deux volets :

  - conception de règles de génération de code, afin de mettre en correspondance les concepts du RTL/C-minor en concepts équivalents de Wasm,

  - preuve formelle (en Rocq) de correction du backend, en s'appuyant sur les sémantiques pré-existantes des deux langages.

2. Augmentation du back-end en assurant des propriétés non fonctionnelles additionnelles. Nous nous intéresserons par exemple à la performance ou à certaines propriétés de sécurité du code généré. La portée exacte de cette seconde étape et la définition des propriétés non fonctionnelles ajoutées seront définies au cours de la première étape selon l'avancement de cette dernière.