Exécution symbolique pour tous ou Compilation d’OCaml vers WebAssembly
Lundi 16 décembre 2024 à 14h
Amphithéâtre du bâtiment 660, Avenue des Sciences, 91190 Gif-sur-Yvette
Résumé. Les limitations de JavaScript en tant que langage par défaut du Web ont conduit au développement de WebAssembly (Wasm), un langage sûr, efficace et modulaire. Toutefois, compiler des langages à glaneur de cellules vers Wasm ne se fait pas sans peine, notamment du fait de la nécessité de réécrire le moteur d’exécution ou de la gestion des interactions avec le glaneur de cellules de l’hôte (le navigateur). Des extensions, dont WasmGC, ont été développées par les groupes de travail Wasm pour faciliter cette tâche. Nous présentons Wasocaml, le premier compilateur d’OCaml vers WasmGC. Ce projet confirme l’adéquation de la proposition WasmGC pour des langages fonctionnels et a influencé son développement. Les stratégies de compilation mises en œuvre dans Wasocaml peuvent également être appliquées à d’autres compilateurs et langages ; deux compilateurs les ont d’ailleurs déjà adoptées.
Cependant, Wasm, bien qu’initialement conçu pour les applications web, est devenu une alternative sérieuse pour les environnements serveurs et les systèmes embarqués, en raison de ses avantages en termes de performances et de sécurité. Cependant, des vulnérabilités comme les débordements de tampon et les fuites de mémoire subsistent, ce qui peut conduire à des vulnérabilités. Pour répondre à cette problématique, nous introduisons Owi, un interpréteur symbolique pour Wasm, écrit en OCaml. Owi est basé sur un interpréteur modulaire et monadique capable d’exécutions concrètes et symboliques de programmes Wasm. Grâce à cette architecture, nous avons développé un outil de détection de bogues performant qui, selon notre évaluation, est le meilleur actuellement disponible pour Wasm
En outre, puisque Wasm est une cible de compilation pour de nombreux langages, Owi peut être utilisé pour détecter des bogues dans dans des programmes issus d’autres langages tels que C et Rust, ou dans des projets mêlant les deux. Nos expériences, basées sur les benchmarks Test-Comp 2024, montrent qu’Owi offre des performances comparables à celles des outils représentant l’état de l’art comme KLEE, avec certains avantages dans des scénarios spécifiques où les approximations de KLEE peuvent entraîner des faux négatifs. Contrairement aux autres outils d’exécution symboliques qui ont une approche ad-hoc, le notre présente l’avantage d’être facilement utilisable pour tout langage possédant un compilateur vers Wasm.
Enfin, nous montrons également comment Owi peut être utilisé à d’autres fins que la recherche de bogues, par exemple la programmation par contraintes. En particulier, Owi permet, tout comme son moteur d’exécution symbolique, d’ajouter des capacités de programmation par contraintes à n’importe quel langage possédant un compilateur vers Wasm, et ce d’une manière directe et modulaire.
Plus d'informations ici : https://www.zapashcanon.fr/phd
Directeur de thèse : Jean-Christophe Filliâtre, Directeur de recherche, CNRS, LMF