Analyses de sécurité par interprétation abstraite.

Depuis récemment, les outils de vérification par interprétation abstraite de code bas-niveau sont devenus suffisamment mûrs pour réaliser des analyses de sécurité. Ils savent notamment faire des analyses précises des propriétés mémoires des programmes, des analyses modulaires sur des morceaux de programmes, et des analyses capables de gérer les aspects bas-niveau du langage. L'outil Codex, développé au CEA LIST, est une exemple d'outil capable de faire ce type d'analyses. Le but de cette thèse est d'explorer les possibilités permises par un outil d'interprétation abstraite pour réaliser des analyses de sécurité, couvrant les différents aspects: aide à la compréhension de code, vérification d'absence d'erreurs dans des sous parties du code, utilisation des invariants pour produire un langage intermédiaire optimisé. École doctorale : Sciences et Technologies de l'Information et de la Communication Direction : Matthieu LEMERRE Financement : Autre type de financement - Autre type de financement,