Préservation des propriétés dans un flot de compilation optimisant
Son Tuan Vu · HAL (Le Centre pour la Communication Scientifique Directe) · 2021
Afin d’assurer des garanties sécuritaires des applications binaires, des analyses et vérifications doivent avoir lieu au niveau binaire. Ces analyses et vérifications nécessitent des propriétés de sécurité ou fonctionnelles des applications. Il est donc nécessaire de transporter et transposer ces propriétés portant sur le code source au niveau du code compilé. La préservation de propriétés tout au long du flot de compilation est un problème difficile à cause des optimisations qui réorganisent les calculs ou éliminent les variables inutiles. Cette thèse présente des approches permettant de propager et préserver des propriétés tout au long d’un flot de compilation optimisant sans modifier les passes d’optimisation du compilateur. Dans l’implémentation dans LLVM, les propriétés sont émises dans le code binaire sous forme d’information de débug DWARF permettant leur utilisation par des outils d’analyse binaire. Les mécanismes proposés peuvent être utilisés pour préserver des protections insérées dans le code source tout en activant les optimisations du compilateur.