Contrôle du flot d'information par des techniques basées sur le langage de programmation

Un programme est dit non interférent si les valeurs de ses sorties publiques ne dépendent pas des valeurs de ses entrées secrètes. Des études ont montré que par l'analyse du flot d'information, on peut établir et contrôler cette propriété ou des propriétés qui lui sont étroitement liées. Dans ce travail, nous examinons en détail les modèles d'analyse de flot d'information existants, et esquissons une nouvelle approche dans un paradigme concurrent. La première partie de ce mémoire présente les différentes formulations de la non-interférence et un survol des grandes familles de mécanismes d'analyse de flot d'information. En second lieu, nous présentons en détail quelques mécanismes récents d'analyse sensibles aux flots, applicables à la programmation séquentielle. Mécanismes statiques pour certains, dynamiques ou hybrides pour d'autres. Dans la troisième partie, nous explorons deux modèles récents de sécurisation des flots d'information dans un programme concurrent. Les deux modèles ont en commun la particularité de proposer des traitements pour sécuriser l'interaction entre les programmes et l'ordonnanceur. Nous terminons par une esquisse de notre nouvelle approche, basée sur l'analyse des dépendances entre les variables d'un programme concurrent.A program is said to be noninterfering if the values of its public (or low) outputs do not depend on the values of its secret (or high) inputs. Various researchers have demonstrated how this property (or closely related properties) can be achieved through information flow analysis. In this work, we present in detail some existing models of information flow analysis, and sketch a new approach of analysis for concurrent programming. The first part of this thesis presents the different formulations of non-interference, and an overview of the main types of information flow analysis. In the second part, we examine in detail some recent static and dynamic (hybrid) flow-sensitive analysis models, for a simple imperative language. In the third part, we explore two recent models of secure information flow in concurrent programs, which develop a novel treatment of the interaction between threads and the scheduler to prevent undesired interleaving. We end with a sketch of the foundations for another approach, based on the analysis of dependencies between variables of concurrent programs