Information flow analysis by abstract interpretation

Protéger la confidentialité de l’information numérique stockée ou en transfert sur des réseaux publics est un problème récurrent dans le domaine de la sécurité informatique. Le but de cette thèse est de fournir des résultats théoriques et expérimentaux sur une analyse de flue permettant la vérification automatique de l’absence de fuite possible d’information sensible. Notre approche est basée sur la théorie de l’Interprétation Abstraite et consiste à manipuler une approximation de la sémantique des programmes. Nous détectons les différentes dépendances entre les variables d’un programme en utilisant des formules propositionnelles avec notamment le domaine Pos. Nous étudions les principales façon d’améliorer la précision (en combinant des domaines abstraits) et l’efficacité (en associant des opérateurs d’élargissement et de rétrécissement) de l’analyse. Le produit réduit du domaine logique Pos et d’un domaine numérique choisi permet une analyse strictement plus précise que celles précédemment présentent dans la littérature. La construction modulaire de notre analyse permet de choisir un bon compromis entre efficacité et précision en faisant varier la granularité de l’abstraction et la complexité des opérateurs abstraits. Pour finir, nous introduisons Sails une nouvelle analyse de flue destinée à des langages de haut niveau sans annotation tel que Java. Sails combine une analyse de fuite possible d’information à différentes abstraction de la mémoire (du tas), ce qui lui permet d’inférer des résultats sur des programmes manipulant des structures complexes. De premiers résultats expérimentaux permettent de pointer l’efficacité de notre approche en appliquant Sails à l’analyse de SecuriBench-micro.