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.

Titre de l'écran-titre (visionné le 1er novembre 2023) / Un dossier de santé électronique rassemble des informations médicales relatives à une personne, telles que les médicaments, les antécédents médicaux, les allergies, les tests médicaux, le statut vaccinal, les radiographies, les signes vitaux, l'âge et le poids, entre autres. Ces données sont stockées numériquement et partagées lorsque nécessaire. Cependant, maintenir la confidentialité et l'intégrité des données, ainsi que leur échange dans un environnement sécurisé et fiable, représente un défi majeur dans le domaine des dossiers médicaux. La blockchain, en tant que réseau distribué hautement sécurisé, offre une technologie révolutionnaire pour le secteur de la santé. Grâce à sa nature immuable, elle permet le partage sécurisé des données médicales. Dans ce mémoire, nous expliquerons comment les dossiers médicaux des patients sont cryptés et stockés dans une mémoire décentralisée. En utilisant la technologie de la blockchain, nous fournissons un accès sécurisé aux données, basé sur les attributs spécifiques des données, tout en maintenant la confidentialité sur une plate-forme évolutive. Nous sommes arrivés à la conclusion que l'utilisation de la blockchain avec une mémoire de stockage décentralisée peut augmenter considérablement le niveau de sécurité. En utilisant cette méthode, l'accès aux données médicales est assuré en cas d'urgence et les chercheurs peuvent accéder aux données des patients de manière anonyme pour mener leurs recherches. Le contrôle du partage des données est entre les mains du patient et, si celui-ci donne son autorisation, les prestataires de soins de santé peuvent accéder à ses données. Dans l'ensemble, nous avons proposé un environnement de partage de données sûr et très efficace. / An electronic health record collects medical information about a person, such as medications, medical history, allergies, medical tests, vaccination status, x-rays, vital signs, age and weight, among others . This data is stored digitally and shared when necessary. However, maintaining the confidentiality and integrity of data, as well as their exchange in a secure and reliable environment, represents a major challenge in the eld of medical records. Blockchain, as a highly secure distributed network, offers a revolutionary technology for the healthcare sector. Thanks to its immutable nature, it allows the secure sharing of medical data. In this research report, we will explain how patient medical records are encrypted and stored in a decentralized memory. Using blockchain technology, we provide secure access to data, based on specific data attributes, while maintaining privacy on a scalable platform. We have come to the conclusion that using blockchain with decentralized storage can significantly increase the level of security. Using this method, access to medical data is ensured in case of emergency and researchers can access patient data anonymously to conduct their research. Control over data sharing is in the hands of the patient and, if the patient gives permission, healthcare providers can access their data. Overall, we provided a secure and very efficient data sharing environment.

Les dossiers de santé électronique (DSE) sont critiques. Les données privées hautement sensibles dans les soins de santé doivent être fréquemment partagées entre les parties prenantes. La blockchain fournit un historique partagé, transparent et immuable de toutes les transactions pour établir des relations avec confiance, transparence et responsabilité. Il peut offrir une possibilité unique de développer un système de gestion et de partage des données de DSE fiables et sécurisé. La technologie de blockchain et les contrats intelligents pourraient aider dans des scénarios typiques liés à la gestion des données, à l'accès aux données et à l'interopérabilité des données. Une analyse complète et exploratoire du contrôle d'accès basé sur la blockchain a montré que la plupart des systèmes de contrôle actuels ne prennent pas en charge le contrôle d'accès à grain fin, ou se concentrent simplement sur d'autres facteurs, tels que la préservation de la vie privée et la sémantique des relations. Dans cet article, j'ai discuté de la nécessité d'un modèle de contrôle d'accès à granularité fine en ce qui concerne la confidentialité en utilisant des stratégies de contrôle d'accès basé sur les attributs, pour les dossiers de santé électroniques. La principale contribution est le cadrage des problèmes d'évolutivité, d'accessibilité et de confidentialité des données dans les soins de santé par une architecture intégrée basée sur la blockchain pour partager des données sécurisées entre les entités. / Health medical records (EHRs) are critical. Highly sensitive private data in healthcare require to be frequently shared among stakeholders. Blockchain provides a shared, transparent, and immutable history of all the transactions to build relationships with trust, transparency, and accountability. It can provide a unique possibility to develop a trustable and secure EHR data management and sharing system. Blockchain technology, and smart contracts, could help in typical scenarios correlated to data management, data access, and data interoperability. Comprehensive and exploratory analysis of blockchain-based access control has shown that most current control systems do not support fine-grained access control or just focus on other factors such as privacy preservation and relationship semantics. In this article, I discussed the need for a fine-grained access control model with respect to privacy by using Attribute-Based Access Control Policies for electronic health records. The main contribution is the framing of scalability, accessibility, and data privacy issues in healthcare by an integrated blockchain-based architecture to share secure data between entities.

Ces cinquante dernières annéees, les ordinateurs ont occupé une place toujours plus importante dans notre vie quotidienne. On les retrouve aujourd’hui présents dans de nombreuses applications, sous forme de systèmes enfouis. Ces applications sont parfois critiques, dans la mesure où toute défaillance du système informatique peut avoir des conséquences catastrophiques, tant sur le plan humain que sur le plan économique. <p>Nous pensons par exemple aux systèmes informatiques qui contrôlent les appareils médicaux ou certains systèmes vitaux (comme les freins) des véhicules automobiles. <p>Afin d’assurer la correction de ces systèmes informatiques, différentes techniques de vérification Assistée par Ordinateur ont été proposées, durant les trois dernières <p>décennies principalement. Ces techniques reposent sur un principe commun: donner une description formelle tant du système que de la propriété qu’il doit respecter, et appliquer une méthode automatique pour prouver que le système respecte la propriété. <p>Parmi les principaux modèles aptes à décrire formellement des systèmes informatiques, la classe des systèmes de transition bien structurés [ACJT96, FS01] occupe une place importante, et ce, pour deux raisons essentielles. Tout d’abord, cette classe généralise plusieurs autres classes bien étudiées et utiles de modèles à espace <p>d’états infini, comme les réseaux de Petri [Pet62](et leurs extensions monotones [Cia94, FGRVB06]) ou les systèmes communiquant par canaux FIFO avec pertes [AJ93]. Ensuite, des problèmes intéressants peuvent être résolus algorithmiquement sur cette classe. Parmi ces problèmes, on trouve le probléme de couverture, auquel certaines propriétés intéressantes de sûreté peuvent être réduites. <p>Dans la première partie de cette thèse, nous nous intéressons au problème de couverture. Jusqu’à présent, le seul algorithme général (c’est-à-dire applicable à n’importe quel système bien structuré) pour résoudre ce problème était un algorithme dit en arrière [ACJT96] car il calcule itérativement tous les états potentiellement non-sûrs et vérifie si l’état initial du système en fait partie. Nous proposons Expand, Enlarge and Check, le premier algorithme en avant pour résoudre le problème de couverture, qui calcule les états potentiellement accessibles du système et vérifie si certains d’entre eux sont non-sûrs. Cette approche est plus efficace en pratique, comme le montrent nos expériences. Nous présentons également des techniques permettant d’accroître l’efficacité de notre méthode dans le cas où nous analysons des réseaux de Petri (ou <p>une de leurs extensions monotones), ou bien des systèmes communiquant par canaux FIFO avec pertes. Enfin, nous nous intéressons au calcul de l’ensemble de couverture pour les réseaux de Petri, un objet mathématique permettant notamment de résoudre le problème de couverture. Nous étudions l’algorithme de Karp & Miller [KM69], une solution classique pour calculer cet ensemble. Nous montrons qu’une optimisation de cet algorithme présenté dans [Fin91] est fausse, et nous proposons une autre solution totalement neuve, et plus efficace que la solution de Karp & Miller. <p>Dans la seconde partie de la thèse, nous nous intéressons aux pouvoirs d’expression des systèmes bien structurés, tant en terme de mots infinis que de mots finis. Le pouvoir d’expression d’une classe de systèmes est, en quelque sorte, une mesure de la diversité des comportements que les modèles de cette classe peuvent représenter. En ce qui concerne les mots infinis, nous étudions les pouvoirs d’expression des réseaux de Petri et de deux de leurs extensions (les réseaux de Petri avec arcs non-bloquants et les réseaux de Petri avec arcs de transfert). Nous montrons qu’il existe une hiérarchie stricte entre ces différents pouvoirs d’expression. Nous obtenons également des résultats partiels concernant le pouvoir d’expression des réseaux de Petri avec arcs de réinitialisation. En ce qui concerne les mots finis, nous introduisons la classe des langages bien structurés, qui sont des langages acceptés par des systèmes de transition bien structurés étiquettés, où l’ensemble des états accepteurs est clos par le haut. Nous prouvons trois lemmes de pompage concernant ces langages. Ceux-ci nous permettent de réobtenir facilement des résultats classiques de la littérature, ainsi que plusieurs nouveaux résultats. En particulier, nous prouvons, comme dans le cas des mots infinis, qu’il existe une hiérarchie stricte entre les pouvoirs d’expression des extensions des réseaux de Petri considérées. / Doctorat en sciences, Spécialisation Informatique / info:eu-repo/semantics/nonPublished