Alive prouve formellement que les optimisations des compilateurs sont correctes

Des dizaines de défauts corrigés dans LLVM et Visual C++

Lorsque l’on développe une application et que l’on rencontre un problème, la source la plus courante est le code que l’on écrit soi-même. Plus rarement, il s’agit d’un défaut dans les bibliothèques utilisées, exceptionnellement dans le compilateur, jamais dans le processeur. Du moins, c’est ce que bon nombre de programmeurs ont fini par intégrer. Il n’empêche que cette hiérarchie est assez optimiste. Par exemple, les processeurs n’exécutent pas toujours correctement les instructions qui leur sont passées : depuis la mauvaise implémentation de FDIV sur les premiers Pentium jusqu’à la technologie HyperThreading de la dernière génération de processeurs Intel Core ou un problème pas encore identifié sur les AMD Ryzen qui causent un bon nombre d’erreurs de segmentation avec GCC.

Les compilateurs ne font pas exception. Comme les fabricants de processeurs, les développeurs de compilateurs sont sous pression. Ils veulent augmenter la performance des applications compilées/exécutées, augmenter l’efficacité énergétique, etc. De plus, la complexité de ces projets ne fait qu’augmenter : il est impossible de dessiner l’entièreté des processeurs à la main pour leur conception depuis belle lurette, les compilateurs modernes font plusieurs millions de lignes de code qui évoluent rapidement. Ainsi, des défauts sont présents, tant au niveau des compilateurs que des processeurs — des défauts qui peuvent mener à des failles de sécurité béantes.



[h=2]Un exemple : Heartbleed[/h] Par exemple, pour accéder à une cellule d’un tableau en mémoire, il faut s’assurer que l’adresse est bien dans le tableau : sinon, on peut lire des données normalement inaccessibles pour ce morceau de code (c’est notamment le principe de Heartbleed, qui avait fait beaucoup de bruit en 2014). Pour un bon nombre de langages, ces vérifications sont effectuées à chaque accès au tableau, sauf s’il est possible de prouver que l’accès ne pose aucun problème. Si une optimisation du compilateur fait une erreur à ce moment, la sécurité du programme compilé est mise à mal.

Cette preuve peut se faire en déterminant la plage de valeurs possibles pour l’index et en la comparant à la taille du tableau, par exemple. Toutes les optimisations du compilateur doivent ainsi être écrites précisément : si l’une d’entre elles fait une petite erreur dans le calcul de la plage de valeurs possibles, tout le reste du château s’effondre.

[h=2]Alive[/h] C’est pourquoi une série de chercheurs s’est associée à Microsoft pour développer Alive, un outil de vérification formel des optimisations effectuées par un compilateur. Il faut tout d’abord décrire l’optimisation dans un langage précis ; ensuite, Alive utilise les technologies actuelles de preuve automatique de théorème (plus précisément, le solveur SMT Z3) pour déterminer si l’optimisation est correcte ou non. Les résultats ne se sont pas fait attendre : très rapidement, une dizaine de défauts ont été trouvés dans LLVM ; Alive a aussi empêché l’introduction d’optimisations fausses dans LLVM et le compilateur C++ de Microsoft.

La suite des travaux de ce groupe envisage une intégration dynamique au compilateur : au lieu de vérifier en amont qu’une optimisation est valide (peu importe le programme à compiler), il s’agit de vérifier si l’optimisation d’un programme s’est déroulée sans anicroche. Ce principe s’appelle validation de la traduction et permet de détecter d’autres types de problèmes, dans les cas où l’optimisation effectuée est hors de portée des programmes de vérification. Notamment, Microsoft déclare avoir déjà pu corriger quelques défauts dans son compilateur C++ grâce à cette méthode, malgré les autres analyses effectuées.

Il n’empêche que ces travaux n’ont pas beaucoup d’intérêt si la sémantique de la représentation intermédiaire (utilisée par les compilateurs pour effectuer les optimisations sans dépendre du langage compilé) n’est pas parfaitement définie : c’est là le prochain axe de recherche, déjà entamé en ce qui concerne les comportements indéfinis (notamment en C et C++).

Source : Getting compilers right: a reliable foundation for secure software.