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.

Les techniques traditionnelles de détection d'intrusions s'appuient sur différentes approches permettant d'identifier une utilisation non prévue et non autorisée de différentes ressources d'un système informatique. Afinn de détecter ces comportements, nous décrivons dans ce mémoire une approche logique de détection d'intrusions basée sur l'identification, dans des traces d'exécutions, de violations de politiques de sécurité données. Le modèle développé spécifie l'état des ressources d'un système ainsi que les effets des différents appels système sur cet état. Le système obtenu, qui s'apparente à un système expert, s'appuie sur un ensemble de règles logiques décrivant les connaissances d'un expert en sécurité informatique. Tout comportement illégal, c'est-à-dire non conforme aux politiques de sécurité considérées, est signalé et est considéré comme une tentative d'intrusion. Le système implémenté est capable de détecter une large classe d'attaques puisque l'approche développée ne se base pas sur certaines séquences particulières d'actions déjà recensées, mais plutôt sur les effets des différentes actions effectuées. De plus, il est capable de détecter de nouveaux comportements malveillants non préalablement identifiés. / Traditional techniques for intrusion detection based on different approaches for identifying unintended and unauthorized use of dfferent resources of a computer system. To detect these behaviors, we describe in this paper a logical approach to intrusion detection based on the identification, in execution traces, of violations of given security policies. The developed model specifies the state of system resources as well as the effects of different system calls on this state. The resulting system, which is similar to an expert system, relies on a set of logical rules describing the knowledge of an expert in computer security. Any illegal behavior, that means not conform to the considered security policies, is reported and is considered as an intrusion attempt. The implemented system is able to detect a wide class of attacks since the approach is not based on some particular sequences of actions already identified, but rather on the effects of different actions performed. In addition, it is able to detect new malicious behavior not previously identified.

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.

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.

L'évolution des systèmes informatiques ayant des programmes parallèles, des processeurs multi-cores et des réseaux fortement interconnectés rend la détection des activités malicieuses plus difficile. Dans un tel contexte, le traçage du noyau s:est révélé être une solution appropriée. Ce travail présente un framework complet pour les analyses des traces du noyau. On a proposé un langage scripte déclaratif et simple à utiliser pour la spécification des patrons. Les patrons compilés sont insérés dans le moteur de détection qui par la suite analyse les traces et progressivement communique avec le module d'affichage. Le module d1 affichage est responsable d'avertir l'administrateur sur les problèmes qui exécutent en arrière plan sur le système. On considère que notre approche est suffisamment générale pour être utiliser avec n'importe quel types de trace (réseaux ou systèmes) ou même des traces combinés. Le langage proposé peut efficacement décrire des patrons reliés aux différents types de domaines : sécurité, performance, débogage et abstraction.

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.

Thèse ou mémoire avec insertion d'articles / La détection d'anomalies vidéo (DAV) est une tâche cruciale de vision par ordinateur pour diverses applications du monde réel telles que la vidéosurveillance, le contrôle qualité, etc. Avec la rareté des données d'anomalies étiquetées et la nature ouverte des définitions d'anomalies, il y a eu une croissance d'intérêt des chercheurs pour l'exploration de méthodes semi-supervisées de détection d'anomalies vidéo. Ces méthodes utilisent une tâche proxy pour ajuster un modèle sur des échantillons normaux, en tenant compte de leurs caractéristiques d'apparence et de mouvement. Les anomalies sont par conséquent détectées en mesurant l'écart des échantillons de test par rapport au modèle normal formé. Cette thèse est dédiée à l'avancement de ce domaine, englobant quatre composantes distinctes. Dans la partie initiale, nous menons une étude approfondie sur les méthodes DAV semi-supervisées de pointe existantes afin d'examiner leurs points forts et leurs défis. Pour compléter notre examen, nous effectuons également des expériences pour mieux comprendre les capacités et les limites des approches existantes. Les résultats de cette étude servent de source de motivation et mettent en lumière l'orientation de notre recherche. Cette étude est publiée sous la forme d'un article de synthèse (MTAP2023). Lors de l'analyse des méthodes existantes, il devient évident qu'elles ne tiennent pas suffisamment compte de la classe des objets lorsqu'il s'agit de détecter des anomalies d'apparence. Inspirés par ce besoin, nous proposons, dans la deuxième partie, une méthode DAV basée sur l'apprentissage en profondeur et sensible aux classes d'objets. C'est une méthode à deux flux qui modélise et détecte les anomalies de mouvement et d'apparence dans différentes branches. Dans la branche apparence, nous introduisons une approche basée sur la distillation des connaissances qui utilise une méthode de segmentation sémantique pré-entraînée (Mask-RCNN) pour former un réseau étudiant dédié à la segmentation sémantique avec des objets normaux. Par conséquent, en mesurant l'écart entre les sorties des réseaux enseignant et étudiant, nous dérivons un score d'anomalie pour la branche d'apparence. La branche de mouvement, d'autre part, traduit une image brute en sa carte de magnitude de flux optique correspondante, pour modéliser les mouvements normaux et détecter les anomalies associées. L'approche de modélisation de mouvement proposée atténue le risque de généralisation aux anomalies, améliorant ainsi la fiabilité et la précision du processus de détection. Les résultats de cette étude ont été publiés sous forme d'article de conférence (CRV 2022). Dans la troisième partie, nous proposons une méthode de détection d'anomalies vidéo basée sur l'apprentissage multi-tâches visant à tirer parti des avantages de la combinaison de plusieurs tâches proxy complémentaires pour améliorer les performances de détection d'anomalies. Différentes tâches complémentaires sont proposées en tenant compte de leurs capacités et insuffisances à détecter différents cas d'anomalies. De plus, nous proposons une nouvelle tâche proxy de prédiction de carte de segmentation sémantique future pour la détection d'anomalies vidéo qui bénéficie des capacités de prédiction de trames futures et de tâches de segmentation sémantique pour la détection d'anomalies de mouvement et d'apparence. De plus, pour améliorer encore la détection des anomalies de mouvement, nous intégrons la tâche de prédiction de l'amplitude du flux optique à partir d'une trame brute dans une autre branche. Finalement, pour relever les défis rencontrés dans notre méthode précédente, nous proposons plusieurs mécanismes d'attention pour engager des informations contextuelles dans la modélisation de mouvement, conduisant à une amélioration des performances. Les résultats de cette étude ont été publiés sous forme d'article de conférence (CVPRW 2023). Dans la dernière partie, nous relevons un autre défi dans la modélisation du mouvement. Tant dans nos méthodes proposées que dans d'autres méthodes existantes, les modèles de mouvement à long terme n'ont pas été efficacement pris en compte pour la détection d'anomalies vidéo. Pour remédier à cette limitation, nous proposons une nouvelle tâche proxy pour la détection d'anomalies vidéo : la prédiction vidéo future à partir d'une seule image. Cette méthode prend en compte les modèles de mouvement à long terme en plus des modèles à court terme pour la détection d'anomalies vidéo et relève le défi de la généralisation aux mouvements anormaux. Cette étude donne des résultats significatifs. Les résultats démontrent que la formulation de DAV comme une prédiction d'images plus éloignées dans le futur (au lieu de l'image suivante immédiate) entraîne une plus grande disparité entre les normales et les anomalies et donc une amélioration des performances. Les résultats de cette étude sont acceptés sous forme d'article de conférence (ISVC 2023). Nos résultats qualitatifs et quantitatifs ainsi que des études d'ablation sur des ensembles de données de référence tels que les ensembles de données ShanghaiTech, UCSD-Ped1 et UCSD-Ped2 démontrent le succès de chaque contribution de notre thèse dans la réalisation de leurs objectifs respectifs. / Video anomaly detection (VAD) is a crucial computer vision task for various real-world applications such as video surveillance, quality control, etc. With the scarcity of labeled anomaly data and the open-ended nature of anomaly definitions, there has been a growing interest among researchers in exploring semi-supervised methods for video anomaly detection. These methods employ a proxy-task to fit a model on normal samples, taking into account their appearance and motion features. Anomalies are consequently detected by measuring the deviation of test samples from the trained normal model. This thesis is dedicated to advancing this field, encompassing four distinct components. In the initial part, we conduct an in-depth study on existing state-of-the-art semi-supervised VAD methods to examine their strong points and challenges. To supplement our review, we also conduct experiments to gain deeper insights into the capabilities and limitations of existing approaches. The outcomes of this study serve as a source of motivation and highlights the direction of our research. This study is published as a review paper (MTAP2023). Upon analyzing the existing methods, it becomes apparent that they do not adequately consider the object class when it comes to detecting appearance anomalies. Inspired by this need, we propose, in the second part, a two-stream object class-aware deep learning based VAD method that models and detects motion and appearance anomalies in different network branches. In the appearance branch, we introduce a knowledge-distillation-based approach that utilizes a pre-trained semantic segmentation method (Mask-RCNN) to train a student network dedicated to semantic segmentation with normal objects. Consequently, by measuring the disparity between the outputs of the teacher and student networks, we derive an anomaly score for the appearance branch. Motion branch, on the other hand, translates a raw frame to its corresponding optical flow magnitude map, to model normal motions and detect related anomalies. The proposed motion modeling approach, mitigates the risk of generalization to anomalies, thus enhancing the reliability and precision of the detection process. Results of this study is published as a conference paper (CRV 2022). In the third part, we put forth a multi-task learning based video anomaly detection method aimed at leveraging the benefits of combining multiple complementary proxy-tasks to enhance anomaly detection performance. Different complementary tasks are suggested taking into ac count their abilities and shortcomings in detecting different anomaly cases. Moreover, we propose a novel proxy-task of future semantic segmentation map prediction for video anomaly detection which benefits from the abilities of future frame prediction and semantic segmentation tasks for motion and appearance anomaly detection. Additionally, to further enhance the detection of motion anomalies, we incorporate the task of optical flow magnitude prediction from a raw frame in another branch. Finally, to address the challenges encountered in our previous method, we propose multiple attention mechanisms to engage context information in motion modeling, leading to performance improvement. Results of this study is published as a conference paper (CVPRW 2023). As the final part, we tackle another challenge in motion modeling. Both in our proposed methods and other existing methods, long-term motion patterns have not been effectively considered for video anomaly detection. To address this limitation, we put forward a novel proxy-task for video anomaly detection: future video prediction from a single frame. This method considers long-term motion patterns in addition to short-term ones for video anomaly detection and addresses the challenge of generalization to abnormal motion. This study yields significant findings. The results demonstrate that formulating VAD as a prediction of farther frames in the future (instead of the immediate next frame) results in a larger disparity between normals and anomalies and hence in improved performance. Results of this study is accepted as a conference paper (ISVC 2023). Our qualitative and quantitative results along with ablation studies on benchmark datasets such as ShanghaiTech, UCSD-Ped1 and UCSD-Ped2 datasets demonstrate the success of each contribution of our thesis in achieving their respective goals.