Accueil > Projets > FXMessages X1, X4 ... > Réécriture et compilation de confiance par Antoine Reilles
Réécriture et compilation de confiance par Antoine Reilles
mardi 25 juin 2019, par
« Introduction
Le sujet de cette thèse est la compilation de langages de haut niveau vers des langages de niveau moins élevé. Plus précisément, la question est de savoir quel niveau de confiance peut être accordé à ces compilateurs, et ce que l’on peut faire pour élever ce niveau de confiance.
Cette question est motivée par le développement de Tom, qui est un compilateur pour des constructions de filtrage intégrées à un langage comme Java, C ou ML. Le langage Tom fournit des outils et fonctionnalités dont le but est de permettre l’écriture de compilateurs sûrs. Ceci se fait par l’introduction de constructions de haut niveau et de signatures aidant la description formelle d’algorithmes complexes et de manipulations d’arbres de syntaxe abstraits.
Une première question est de savoir quel niveau de confiance attribuer au
compilateur Tom lui-même : si ce compilateur produit du code faux, comment pourrait-il nous permettre d’écrire de meilleurs compilateurs ? Nous développons pour résoudre ce problème une méthode de certification qui nous permet de prouver formellement à chaque exécution du compilateur que le code qu’il vient de générer implémente effectivement les constructions de filtrage qu’il avait à compiler.
Cela nous conduit à fournir un générateur d’implémentations de structures de données avec partage maximal, efficaces et sûres, intégrant des invariants ainsi que leur préservation. Ces invariants, comme par exemple imposer aux listes d’être ordonnées ou aux éléments neutres d’être supprimés sont alors assurés par l’implémentation. Ce générateur de structures de données sûres est aussi une pierre angulaire pour le développement d’applications sûres avec Tom.
On s’intéresse alors à fournir un langage de haut niveau pour décrire des traversées et des transformations d’arbres, conduisant à une implémentation plus simple et plus sûre de transformations de documents complexes.
Une fois tous ces éléments rassemblés, on obtient un environnement pour décrire et implémenter des compilateurs de manière sûre. Cet environnement n’a pas pour but de fournir des compilateurs et transformations de documents entièrement vérifiés formellement, mais plutôt de fournir un ensemble de méthodes et outils facilitant le développement de telles transformations et augmentant le niveau de confiance dans le résultat de ce développement. »