Analyse mémoire précise et efficace pour les languages de bas niveau

La sécurité mémoire est essentielle pour les codes critiques tels que les logiciels embarqués et les systèmes d'exploitation. Les erreurs mémoire telles que les débordements de tampon (buffer overflows), la déréférencement de pointeurs nuls et les erreurs d'utilisation de mémoire après libération (use-after-free) sont parmis les principales causes de vulnérabilités en cybersécurité. Les analyses statiques de code bas niveau visent à détecter de telles erreurs sans exécuter les programmes. Cette thèse définit une méthode d'analyse statique solide, automatique, pratique et efficace pour prouver la sécurité spatiale de la mémoire des codes binaires ou des programmes C de bas niveau. Cette analyse repose sur un nouveau système de types dépendants appelé TypedC, qui étend le système de types du langage C et est capable de capturer des propriétés complexes concernant la disposition et le contenu de la mémoire. Ces propriétés incluent celles de idiomes de programmation de bas niveau tels que le bit-stealing, les pointeurs intérieurs ou les tableaux flexibles (flexible array members). L'analyse utilise l'interprétation abstraite pour effectuer automatiquement la vérification de types, prouvant ainsi la sécurité spatiale des accès à la mémoire comme conséquence du typage correct. L'analyse est inter-procédurale, c'est-à-dire qu'elle exploite des résumés de fonctions au lieu d'analyser chaque fonction individuellement. L'analyse ne nécessite pas la modification du code source - ce qui serait impossible pour le code binaire - mais exploite à la place une spécification des types fournie par l'utilisateur et décrivant les prototypes de fonctions.Un autre apport de cette thèse est un cadre général appelé abstract abstract data types (AADT) permettant de construire des analyses précises et polyvalentes pour traiter des structures de données complexes obtenues en combinant des types de pointeurs, d'unions, de structures et de tableaux. Dans ce cadre, un domaine abstrait pour un type de données fixé est construit de manière compositionnelle par dessus un domaine abstrait relationnel de valeurs, et à partir des domaines abstraits correspondant à chacun des composants du type de données. Pour cela, un AADT raffine une interface générique, que nous formalisons dans cette thèse, et il fournit un équivalent abstrait des opérations du type de données. Nous définissons formellement plusieurs domaines abstraits comme AADT, par exemple des AADT de tableaux, des AADT de tuples, des AADT de types de données variants, et des AADT de blocs mémoire.Nous avons implémenté l'analyse basée sur le système de types dépendants proposé et sur le cadre des AADT dans Codex, une plateforme d'analyse de code binaire et C basée sur l'interprétation abstraite. L'analyse a été appliquée à une base de tests complexes comprenant des extraits de systèmes d'exploitation, du code binaire d'Emacs et de bibliothèques de structure de données. Les résultats expérimentaux obtenus démontrent que l'approche proposée dans cette thèse est efficace pour prouver la sécurité spatiale de la mémoire dans du code de bas niveau.