Résumé
Compiler un programme source en code machine peut être l’occasion de le rendre plus résistant à certaines attaques. Par exemple, des tests systématiques de bornes lors des accès aux tableaux peuvent être introduits pendant la compilation, puis optimisés pour en réduire le surcoût en temps d’exécution, augmentant ainsi grandement la sécurité à coût raisonnable. Cependant, de nombreuses optimisations de compilation, pourtant sémantiquement correctes, peuvent affaiblir la sécurité du programme. C’est notamment le cas des optimisations qui supposent l’absence de comportements indéfinis dans le programme source. Nous avons montré comment caractériser ces différences de sécurité entre un fragment de programme source et son code compilé à l’aide d’outils sémantiques classiques : l’équivalence observationnelle et le problème de la full abstraction. Nous avons présenté quelques approches récemment proposées pour compiler « en toute sécurité », c’est-à-dire en préservant les équivalences observationnelles dans les deux directions.
