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.

Durant ces dernières décennies, nous avons assisté à une automatisation massive de la société selon toutes ses sphères. Malheureusement, cette révolution technologique n’a pas eu que des bienfaits. En effet, une nouvelle génération de criminels en a profité, afin d’occasionner davantage d’activités illégales. De ce fait, afin de protéger les systèmes informatiques, il est devenu plus que primordial de définir rigoureusement des politiques de sécurité ainsi que de mettre en oeuvre des mécanismes efficaces capables de les appliquer. L’objectif majeur d’un mécanisme de sécurité consiste souvent à contrôler des logiciels, afin de les contraindre à “bien” se comporter. Cependant, la plupart des mécanismes de sécurité procèdent par des méthodes ad hoc qui sont loin d’être efficaces. En outre, ils sont peu fiables, puisqu’il n’y a aucune preuve sur leur capacité à faire respecter les politiques de sécurité. De là apparaît la nécessité de concevoir des mécanismes de sécurité alternatifs qui résolvent le problème de l’application de la sécurité d’une manière formelle, correcte et précise. Dans ce contexte, notre thèse cible principalement la caractérisation formelle de l’application effective des politiques de sécurité via des mécanismes basés sur la réécriture de programmes. On entend par application effective, le fait d’éliminer tous les “mauvais” comportements d’un programme, tout en conservant tous les “bons” comportements qu’il engendre, et ce, sans compromettre la sémantique du programme à sécuriser. Nous avons opté pour la réécriture de programmes, vu sa grande puissance par rapport aux autres mécanismes de sécurité qui sont soit laxistes soit très restrictifs. Les principaux résultats qui ont été réalisés, afin d’atteindre les objectifs ciblés par cette thèse sont les suivants : – Caractérisation formelle de l’application des propriétés de sûreté par la réécriture de programmes. Il s’agit d’appliquer les propriétés de sûreté qui constituent la classe de propriétés de sécurité la plus communément appliquée par les mécanismes de sécurité. – Caractérisation formelle de l’application de n’importe quelle propriété de sécurité par la réécriture de programmes. Cette contribution montre comment la réécriture de programmes permet l’application de politiques de sécurité qu’aucune autre classe de mécanismes de sécurité ne peut appliquer. – Caractérisation alternative de l’application de la sécurité par une approche algébrique. Cette contribution propose un formalisme algébrique afin de réduire l’écart entre la spécification et l’implantation des mécanismes de sécurité basés-réécriture. / During the last decades, we have witnessed a massive automation of the society at all levels. Unfortunately, this technological revolution came with its burden of disadvantages. Indeed, a new generation of criminals emerged and is benefitting from continuous progress of information technologies to cause more illegal activities. Thus, to protect computer systems, it has become very crucial to rigorously define security policies and provide the effective mechanisms required to enforce them. Usually, the main objective of a security mechanism is to control the executions of a software and ensure that it will never violate the enforced security policy. However, the majority of security mechanisms are based on ad hoc methods and thus, are not effective. In addition, they are unreliable, since there is no evidence on their ability to enforce security policies. Therefore, there is a need to develop novel security mechanisms that allow enforcing security policies in a formal, correct, and accurate way. In this context, our thesis targets the formal characterization of effective security policies enforcement that is based on programs rewriting. We mean by “effective” enforcement preventing all the “bad” behaviors of a program while keeping all its "good" behaviors. In addition, effective enforcement should not compromise the semantics of controlled programs. We have chosen for rewriting programs, because it has a great power compared to other security mechanisms that are either permissive or too restrictive. Themain contributions of this thesis are the following : – Formal characterization of security enforcement of safety properties through program rewriting. Safety properties represent the main class of properties usually enforced by security mechanisms. – Formal characterization of any security property using program rewriting. This contribution shows how program rewriting allows the enforcement of security policies that no other class of security mechanisms can enforce. – Algebraic approach as an alternative formal characterization of program rewriting based security enforcement. In this contribution, we investigate an algebraic formal model in order to reduce the gap between the specification and the implementation of program rewriting based security mechansisms.

La nature des réseaux de capteurs sans fil comme ZigBee, permettant la communication entre différents types de nœuds du réseau, les rend très vulnérables à divers types de menaces. Dans différentes applications des technologies sans fil modernes comme SmartHome, les informations privées et sensibles produites par le réseau peuvent être transmises au monde extérieur par des moyens filaires ou sans fil. Outre les avantages offerts, cette intégration augmentera certainement les exigences en matière de protection des communications. Les nœuds capteurs du réseau étant souvent placés à proximité d'autres appareils, le réseau peut être plus vulnérable aux attaques potentielles. Cette recherche de doctorat a pour but d'utiliser les attributs natifs distincts de radiofréquence RF-DNA sécurisés produits par le processus d'empreinte numérique dans le but de fournir un support de communication sans fil sécurisé pour les communications de réseau ZigBee. Ici, nous visons à permettre une discrimination d'appareil en utilisant des préambules physiques (PHY) extraits des signaux émis pas de différents appareils. Grâce à cette procédure, nous pouvons établir une distinction entre différents appareils produits par différents fabricants ou par le même fabricant. Dans un tel cas, nous serons en mesure de fournir aux appareils des identifications physiques de niveau binaire non clonables qui empêchent l'accès non autorisé des appareils non autorisés au réseau par la falsification des identifications autorisées. / The nature of wireless networks like ZigBee sensors, being able to provide communication between different types of nodes in the network makes them very vulnerable to various types of threats. In different applications of modern wireless technologies like Smart Home, private and sensitive information produced by the network can be conveyed to the outside world through wired or wireless means. Besides the advantages, this integration will definitely increase the requirements in the security of communications. The sensor nodes of the network are often located in the accessible range of other devices, and in such cases, a network may face more vulnerability to potential attacks. This Ph.D. research aims to use the secure Radio Frequency Distinct Native Attributes (RF-DNA) produced by the fingerprinting process to provide a secure wireless communication media for ZigBee network device communications. Here, we aim to provide device discrimination using Physical (PHY) preambles extracted from the signal transmitted by different devices. Through this procedure, we are able to distinguish between different devices produced by different manufacturers, or by the same one. In such cases, we will be able to provide devices with unclonable physical bit-level identifications that prevent the unauthorized access of rogue devices to the network through the forgery of authorized devices' identifications.

Autant les applications Android ont réussi à positionner Android parmi les systèmes d'exploitation les plus utilisés, autant elles ont facilité aux créateurs de maliciels de s'introduire et de compromettre ses appareils. Une longue liste de menaces causées par les applications téléchargées vise l'intégrité du système et la vie privée de ses utilisateurs. Malgré l'évolution incessante du système Android pour améliorer son mécanisme de sécurité, le niveau de sophistication des logiciels malveillants a augmenté et s'adapte continuellement avec les nouvelles mesures. L'une des principales faiblesses menaçant la sécurité de ce système est le manque abyssal d'outils et d'environnements permettant la spécification et la vérification formelle des comportements des applications avant que les dommages ne soient causés. À cet égard, les méthodes formelles semblent être le moyen le plus naturel et le plus sûr pour une spécification et une vérification rigoureuses et non ambiguës de telles applications. Notre objectif principal est de développer un cadre formel pour le renforcement de politiques de sécurité dans les applications Android. L'idée est d'établir une synergie entre le paradigme orienté aspect et les méthodes formelles. L'approche consiste à réécrire le programme de l'application en ajoutant des tests de sécurité à certains points soigneusement sélectionnés pour garantir le respect de la politique de sécurité. La version réécrite du programme préserve tous les bons comportements de la version originale qui sont conformes à la politique de sécurité et agit contre les mauvais. / As much as they have positioned Android among the most widely used operating systems, Android applications have helped malware creators to break in and infect its devices. A long list of threats caused by downloaded applications targets the integrity of the system and the privacy of its users. While the Android system is constantly evolving to improve its security mechanism, the malware's sophistication level is skyrocketing and continuously adapting with the new measures. One of the main weaknesses threatening smartphone security is the abysmal lack of tools and environments that allow formal specification and verification of application behaviors before damage is done. In this regard, formal methods seem to be the most natural and secure way for rigorous and unambiguous specification and verification of such applications. Our ultimate goal is to formally enforce security policies on Android applications. The main idea is to establish a synergy between the aspect-oriented paradigm and formal methods such as the program rewriting technique. The approach consists of rewriting the application program by adding security tests at certain carefully selected points to ensure that the security policy is respected. The rewritten version of the program preserves all the good behaviors of the original one that comply with the security policy and acts against the bad ones.

Ce mémoire traite en premier lieu des avantages et des désavantages des différentes approches visant à assurer la sûreté et la sécurité des logiciels. En second lieu, il présente une nouvelle approche pour combiner l'analyse statique et l'analyse dynamique afin de produire une architecture de sécurité plus puissante. Les premiers chapitres du mémoire comportent une revue analytique des différentes approches statiques, dynamiques et hybrides qui peuvent être utilisées afin de sécuriser le code potentiellement malicieux. L'exposé identifie alors les avantages et les inconvénients de chaque approche ainsi que le champ des politiques de sécurité dans lesquels on peut l'appliquer. Le dernier chapitre traite de la possibilité de combiner l'analyse statique et l'analyse dynamique par une nouvelle approche hybride. Cette approche consiste à instrumenter le code seulement là où c'est nécessaire pour assurer satisfaire une politique de sécurité définie par l'usager et exprimée en un ensemble de propriétés exprimées μ-calcul modal. Cette instrumentation est guidée par une analyse statique effectuée à priori et basée sur un système de type à effets. Les effets représentent les accès aux ressources protégées du système. / The purpose of this thesis is twofold. In the first place it presents a comparative study of the advantages and drawbacks of several approaches to insure software safety and security. It then focuses more particularly on combining static analyses and dynamic monitoring in order to produce a more powerful security architecture. The first chapters of the thesis present an analytical review of the various static, dynamic and hybrid approaches that can be used to secure a potentially malicious code. The advantages and drawbacks of each approach are thereby analyzed and the field of security properties that can be enforced by using it are identified. The thesis then focuses on the possibility of combining static and dynamic analysis through a new hybrid approach. This approach consists in a code instrumentation, that only alters those parts of a program where it is necessary to do so to insure the respect of a user-defined security policy expressed in a set of modal μ-calculus properties. this instrumentation is guided by a static analysis based on a type and effect system. The effects represent the accesses made to pretested system ressources.

Ce mémoire présente une nouvelle approche pour sécuriser du code potentiellement malicieux à l'aide d'un moniteur incorporé au code. Les premiers chapitres du mémoire introduisent les notions préliminaires à la présentation de l'approche. Plus précisément, les concepts fondamentaux de la vérification de modèle et du contrôle des systèmes à événements discrets. Le dernier chapitre présente les fondements théoriques de l'approche en généralisant les résultats de Ligatti, Bauer et Walker, et montre une classe de moniteurs qui est plus puissante lorsqu'on précise son contexte d'application. Cette observation mène à l'élaboration d'une approche consistant à instrumenter un programme, dans le but de le rendre sécuritaire, à partir d'un modèle du programme et d'une propriété de sécurité représentée par un automate de Rabin.

Les problèmes logiciels sont frustrants et diminuent l’expérience utilisateur. Par exemple, la fuite de données bancaires, la publication de vidéos ou de photos compromettantes peuvent affecter gravement une vie. Comment éviter de telles situations ? Utiliser des tests est une bonne stratégie, mais certains bogues persistent. Une autre solution est d’utiliser des méthodes plus mathématiques, aussi appelées méthodes formelles. Parmi celles-ci se trouve la sémantique dénotationnelle. Elle met la sémantique extraite de vos logiciels préférés en correspondance avec des objets mathématiques. Sur ceux-ci, des propriétés peuvent être vérifiées. Par exemple, il est possible de déterminer, sous certaines conditions, si votre logiciel donnera une réponse. Pour répondre à ce besoin, il est nécessaire de s’intéresser à des théories mathématiques suffisamment riches. Parmi les candidates se trouvent le sujet de ce mémoire : la théorie des domaines. Elle offre des objets permettant de modéliser formellement les données et les instructions à l’aide de relations d’ordre. Cet écrit présente les concepts fondamentaux tout en se voulant simple à lire et didactique. Il offre aussi une base solide pour des lectures plus poussées et contient tout le matériel nécessaire à sa lecture, notamment les preuves des énoncés présentés. / Bugs in programs are definitively annoying and have a negative impact on the user experience. For example, leaks of bank data or leaks of compromising videos or photos have a serious effect on someone’s life. How can we prevent these situations from happening? We can do tests, but many bugs may persist. Another way is to use mathematics, namely formal methods. Among them, there is denotational semantics. It links the semantics of your favorite program to mathematical objects. On the latter, we can verify properties, e.g., absence of bugs. Hence, we need a rich theory in which we can express the denotational semantics of programs. Domain Theory is a good candidate and is the main subject of this master thesis. It provides mathematical objects for data and instructions based on order relations. This thesis presents fundamental concepts in a simple and pedagogical way. It is a solid basis for advanced readings as well as containing all the needed knowledge for its reading, notably proofs for all presented statements.

Titre de l'écran-titre (visionné le 13 novembre 2023) / Du fait de leur danger, les deepfakes (ou hypertrucage en français) sont devenus un sujet de société. Cependant, aucune étude conséquente n'a été réalisée sur les deepfakes appliqués au domaine géospatial : l'hypertrucage géospatial. Ce travail commence par faire un état de l'art des technologies génératives permettant la modification partielle d'images, aussi appelées techniques d'« inpainting » en anglais. Grâce à celles-ci, il nous a été possible de concevoir des deepfakes d'imagerie aérienne d'une grande qualité. Afin de tester leur robustesse, des techniques de détection de falsification classiques ont été testées. Ces méthodes se sont révélées utiles mais pas suffisantes. Une méthode originale de détection spécialement adaptée aux particularités des images géospatiales a donc finalement été proposée. Les résultats très satisfaisants obtenus avec cette méthode, permettent de montrer que le contrôle de l'information n'est pas la seule solution au problème de la désinformation. Ce travail pourrait ainsi être utilisé par un public large allant des agences de renseignement, journalistes ou citoyens concernés soucieux de détecter les falsifications provenant de différentes entités.

Autant les applications Android ont réussi à positionner Android parmi les systèmes d'exploitation les plus utilisés, autant elles ont facilité aux créateurs de maliciels de s'introduire et de compromettre ses appareils. Une longue liste de menaces causées par les applications téléchargées vise l'intégrité du système et la vie privée de ses utilisateurs. Malgré l'évolution incessante du système Android pour améliorer son mécanisme de sécurité, le niveau de sophistication des logiciels malveillants a augmenté et s'adapte continuellement avec les nouvelles mesures. L'une des principales faiblesses menaçant la sécurité de ce système est le manque abyssal d'outils et d'environnements permettant la spécification et la vérification formelle des comportements des applications avant que les dommages ne soient causés. À cet égard, les méthodes formelles semblent être le moyen le plus naturel et le plus sûr pour une spécification et une vérification rigoureuses et non ambiguës de telles applications. Notre objectif principal est de développer un cadre formel pour le renforcement de politiques de sécurité dans les applications Android. L'idée est d'établir une synergie entre le paradigme orienté aspect et les méthodes formelles. L'approche consiste à réécrire le programme de l'application en ajoutant des tests de sécurité à certains points soigneusement sélectionnés pour garantir le respect de la politique de sécurité. La version réécrite du programme préserve tous les bons comportements de la version originale qui sont conformes à la politique de sécurité et agit contre les mauvais. / As much as they have positioned Android among the most widely used operating systems, Android applications have helped malware creators to break in and infect its devices. A long list of threats caused by downloaded applications targets the integrity of the system and the privacy of its users. While the Android system is constantly evolving to improve its security mechanism, the malware's sophistication level is skyrocketing and continuously adapting with the new measures. One of the main weaknesses threatening smartphone security is the abysmal lack of tools and environments that allow formal specification and verification of application behaviors before damage is done. In this regard, formal methods seem to be the most natural and secure way for rigorous and unambiguous specification and verification of such applications. Our ultimate goal is to formally enforce security policies on Android applications. The main idea is to establish a synergy between the aspect-oriented paradigm and formal methods such as the program rewriting technique. The approach consists of rewriting the application program by adding security tests at certain carefully selected points to ensure that the security policy is respected. The rewritten version of the program preserves all the good behaviors of the original one that comply with the security policy and acts against the bad ones.

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.