Ce mémoire présente un mécanisme d’application de politiques de sécurité grâce à une analyse de types trivaluée sur un langage impératif. Notre analyse a pour but de réduire les faux positifs générés par l’analyse statique, tout en préparant les programmes analysés à être instrumentés. Les faux positifs se produisent dans l’analyse de systèmes informatiques à temps réel quand il manque de l’information au moment de la compilation, par exemple un nom de fichier, et par conséquent, son niveau de sécurité. Notre approche visant à répondre à la question « Y a-t’il violation de la propriété de non-interférence dans le programme ? », l’idée clé est de distinguer les réponses négatives des réponses incertaines. Au lieu de rejeter le programme systématiquement en cas d’incertitude, nous typons les instructions avec un type additionnel, unknown, indiquant l’incertitude. Notre travail est fait en préparation à un mécanisme d’application hybride, combinant l’analyse statique par l’analyse de types et l’analyse dynamique par l’instrumentation de code. Durant l’étape d’analyse statique, les réponses positives et négatives sont traitées de manière standard, tandis que les réponses incertaines sont clairement annotées du type incertain, préparant ainsi pour un éventuel passage à la deuxième étape : l’instrumentation. Une preuve que notre système de types est cohérent est donnée, ceci en montrant qu’il satisfait la non-interférence. Les programmes interagissent à travers les canaux de communication. Notre contribution réside dans la manipulation de trois types de sécurité, mais aussi dans le traitement des variables et canaux de communication de manière particulière. Les niveaux de sécurité sont associés aux canaux plutôt qu’aux variables dont les niveaux de sécurité varient selon l’information qu’elles contiennent.

Ce mémoire présente une approche d'application de politiques de sécurité qui utilise une analyse de types basée sur un système de types multi-valeurs. Cette analyse est suivie d'une instrumentation lorsque nécessaire. Le langage cible est un langage impératif. Notre approche vise à réduire les faux-positifs générés par une analyse statique, et à réduire la surcharge d'exécution en n'instrumentant que lorsque nécessaire. Les faux-positifs surviennent dans l'analyse de systèmes informatiques lorsqu'une information est manquante durant la compilation, par exemple le nom d'un fichier, et par conséquent, son niveau de sécurité. L'idée principale de notre approche est de distinguer les réponses négatives des réponses incertaines. Au lieu de rejeter les commandes potentiellement non sécuritaires, elles sont identifiées et étiquetées pour la seconde phase de l'analyse. Les réponses négatives et positives sont traitées comme cela se fait d'habitude. Ce travail est une approche hybride d'application de politique de sécurité : les points potentiellement sécuritaires du programme détectés par notre analyse par typage sont instrumentés par la suite avec des tests dynamiques. Le système de typage sur lequel se base le nôtre a été présenté par Desharnais et al. [12]. Notre approche a été acceptée pour publication [7]. Dans ce travail nous présentons les modifications apportées au précédent travail et la phase d'instrumentation qui la complète. La nouveauté de notre approche est de rajouter un niveau de sécurité aux trois du travail précédent. Nous traitons les canaux et les variables de façon spéciale. Les programmes interagissent par le biais de canaux de communication. Des niveaux de confidentialité sont associés aux canaux plutôt qu'aux variables dont le niveau de sécurité est fonction de l'information qu'elles stockent. Notre analyse est sensible au flot. / In this Master thesis, we present an approach to enforce information flow policies using a multi-valued type-based analysis followed by an instrumentation when needed. The target is a core imperative language. Our approach aims at reducing false positives generated by static analysis, and at reducing execution overhead by instrumenting only when needed. False positives arise in the analysis of real computing systems when some information is missing at compile time, for example the name of a file, and consequently, its security level. The key idea of our approach is to distinguish between negative and may responses. Instead of rejecting the possibly faulty commands, they are identified and annotated for the second step of the analysis; the positive and negative responses are treated as is usually done. This work is a hybrid security enforcement mechanism: the maybe-secure points of the program detected by our type based analysis are instrumented with dynamic tests. The basic type based analysis has been reported by Desharnais et al. [12], this work deals with the modification of the type system and the instrumentation step. It has been accepted for publication [7]. The novelty of our approach is the handling of four security types, but we also treat variables and channels in a special way. Programs interact via communication channels. Secrecy levels are associated to channels rather than to variables whose security levels change according to the information they store. Thus the analysis is flow-sensitive.

« Thèse présentée à l'École des gradués de l'Université Laval pour l'obtention du grade de philosophiæ doctor (Ph. D.) » / « Ayant mis en évidence les faiblesses analytiques de la dynamique des systèmes, notre recherche se préoccupera d'abord de modifier le modèle de dynamique des système pour pouvoir exploiter les outils puissants du Contrôle Automatique. Comme nous le verrons, cette modification consistera à procéder à une approximation linéaire du modèle initial de dynamique des systèmes qui est non linéaire. Dans cet effort, nous éviterons la méthode de transformation utilisée par les tenants du Contrôle Automatique (Appiah et Coyle 1983, Mohpatra et Sharma 1983) ; elle nous éloigne de ce qui est le langage par excellence de la dynamique des systèmes: DYNAMO; et surtout, elle est impuissante devant les modèles de grande taille. Nous partirons des principes de linéarisation, pour y procéder directement avec DYNAMO (on y arriverait avec n'importe quelle version de DYNAMO) sans recourir comme N. B. Forrester à un logiciel supplémentaire, DYNASTAT ou autre. Après avoir mis au point un instrument de linéarisation, la thèse montrera comment les gestionnaires peuvent recourir à l'analyse modale pour comprendre la nature et l'ampleur des forces dynamiques présentes au sein de leur entreprise. Pour cela, elle s'appuyera sur la correspondance existant entre la stabilité intrinsèque d'un système et les valeurs propres de son modèle linéaire. En troisième lieu, la thèse fournira une procédure de modification des forces dynamiques pour stabiliser et ajuster les divers secteurs de l'entreprise. La stabilisation consiste à identifier et changer les politiques qui causent l'instabilité. L'ajustement n'intervient qu'après la stabilisation; il consiste à identifier et à renforcer les politiques qui augmentent la stabilité. Basée sur les valeurs propres et l'analyse de leur sensibilité, cette procédure se révélera être un excellent moyen de mettre en évidence les effets réels des politiques suivies dans l'entreprise et d'évaluer l'opportunité de renforcer, atténuer ou éliminer ces politiques par des mesures appropriées. Enfin, elle donne une méthode d'implantation, dans le réel, des suggestions issues de l'analyse modale. L'application sera faite sur le modèle bien connu de Lyneis. Cela permettra d'identifier les sous-systèmes constitutifs du modèle global: leur nature, leur taille et leur mode d'interaction. Le degré d'intégration des différents secteurs de l'entreprise telle que modélisée par Lyneis apparaîtra avec plus de netteté. Nous nous servirons de la procédure développée dans cette thèse pour dégager les mesures et transformations nécessaires à la stabilisation accrue de chaque secteur. Il en résultera une meilleure performance. »--Pages 10-12