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.

La Sécurité des Systèmes d'Information est l'un des défis les plus urgents des différents organismes de la société actuelle. Le problème de sécurité a émergé du progrès technologique rapide qui pousse à l'utilisation des \emph{Systèmes d'Information}. L'un de ces progrès est l'utilisation de code mobile. En effet, pour protéger ses informations critiques d'une éventuelle menace d'un code mobile, un organisme doit chercher des solutions de plus en plus élaborées. Une des approches émergeantes pour aborder ce problème est la compilation certifiée. Il s'agit d'une approche statique, basée sur le langage et génère en plus du code objet, un certificat constitué des informations relatives aux aspects de sécurité d'un programme. En plus des avantages de l'analyse statique, cette approche fait coopérer le producteur du code et son consommateur. De plus, ce dernier n'a plus à faire confiance au producteur. Dans cette thèse nous avons appliqué cette approche au langage Java afin de vérifier statiquement la sécurité. En effet, Java couvre une gamme de périphériques, d'ordinateurs et de réseaux grâce à son évolutivité, son efficacité, sa portabilité et sa sécurité. Toutefois, les propriétés de sécurité de haut niveau sont vérifiées dynamiquement dans Java par le vérificateur du \emph{bytecode} et le gestionnaire de sécurité. Nous proposons alors de concevoir et d'implanter un compilateur certificateur pour Java (JACC) afin d'accroître la flexibilité, l'efficacité et la robustesse de l'architecture de sécurité de Java. Le certificat que génère JACC est vérifié statiquement par le vérificateur de l'architecture JACC. Il est constitué d'annotations qui essaient de reporter et abstraire au mieux le comportement du programme. Les principaux résultats qui nous ont permis d'atteindre ces objectifs sont: \begin{enumerate} \item la définition de la syntaxe et sémantique des annotations du certificat; \item la conception et l'implantation de JACC en partant de Jikes, un compilateur pour le langage Java développé par IBM. Nous avons également pu mener une étude expérimentale pour mesurer la performance de JACC ainsi que la taille des fichiers \emph{.class} générés et nous les avons comparés à Jikes; \item l'élaboration d'un cadre formel pour spécifier le module d'inférence. Cette spécifi\-cation décrit la sémantique opérationnelle de chaque étape d'inférence et ce pour l'ensemble des \emph{opcodes} ainsi qu'un système de types pour les annotations du certificat. \end{enumerate} / Information Systems Security is one of the most pressing challenges facing all kind of organizations today. The security problem has raised from rapid technological advances that are stimulating a greater use of \emph{Information Systems} in world-wide organizations. One of these advances is the use of mobile code. Keeping critical information safe from malicious mobile code is challenging. One way to address the security issue for mobile code is using certifying compilation. The certifying compilation is a language-based, static technique used to collect information (certificate) regarding the safety and security of a software. In addition to the advantages of the static analysis, this approach alleviates the burden on the consumer. The other advantage of this approach is to restrict the trust of the consumer to the verifier only. In this thesis we have applied this approach to Java to check safety and security statically. As we know, Java is present in a wide range of devices, computers, and networks due to it's versatility, efficiency, platform portability and security . Nevertheless, high-level security properties are verified by bytecode verifier and security manager at run time. The main objectives of this thesis are the design and the implementation of a Java certifying compiler (JACC) that helps to increase the flexibility, efficiency and robustness of the Java security architecture. Indeed, JACC certificate is verified statically by the JACC verifier to ensure high-level security properties. The certificate is made up of annotations that try to capture the behavior of a software and represent it in an abstract form. This behavior could be critical and aims to threaten the software user. The main research contributions that led to reach these objectives are: \begin{enumerate} \item the definition of the certificate syntax and semantic; \item the design and the implementation of JACC based on Jikes. We have also measured the generated \emph{.class} files sizes and JACC performance and compared them to Jikes; \item the elaboration of a formal framework in which we formally specify the certificate inference. This specification describes the operational semantic of each inference step as long as a type system for the certificate annotations. \end{enumerate}

L'objectif de cette thèse est d'explorer l'impact des politiques commerciales et de soutien à l'agriculture sur la sécurité alimentaire. Elle s'intéresse plus particulièrement aux pays en développement et émergents en tenant compte de l'importance du secteur agricole dans ces pays. Les politiques commerciales et de soutien à l'agriculture y sont généralement très variées et cette variété pourrait se traduire en des résultats en termes de sécurité alimentaire. Nous voulons savoir si et dans quelle mesure la variabilité temporelle des politiques sus-indiquées affecterait les disponibilités alimentaires ou la dépendance aux importations alimentaires. Pour cela, nous utilisons la littérature théorique et empirique et, testons les modèles d'analyse empirique. Dans le chapitre 1, nous passons en revue le concept de sécurité alimentaire et ses instruments de mesure. Si plusieurs définitions sont proposées pour la sécurité alimentaire, l'idée dans ce chapitre est d'identifier les instruments simples sur lesquels l'action politique nationale et internationale pourrait se concentrer pour la fixation d'objectifs en termes de sécurité alimentaire dans les pays en développement. Notre analyse suggère une pluralité d'instruments, évoluant selon les angles ou dimensions d'analyse de la sécurité alimentaire. Parmi eux, nous distinguons les mesures des disponibilités alimentaires ou encore, celles de dépendance aux importations de produits alimentaires que nous empruntons comme mesures ou indicateurs de sécurité alimentaire dans le cadre de ce travail. Dans le chapitre 2, nous avons fait une revue de la littérature sur, d'une part, la relation entre les politiques commerciales et les dimensions de la sécurité alimentaire, d'autre part, entre les mesures de soutien à l'agriculture et les dimensions et/ou indicateurs de la sécurité alimentaire. Si dans le premier cas, nous avons conclu à l'importance de la production agricole dans l'analyse d'une telle relation, nous avons constaté, dans le second cas, qu'étant donné la variété des mesures de soutien à l'agriculture, la complexité dans le calcul d'un indicateur unique de soutien à l'agriculture et, le classement qui est fait des mesures en ce qui concerne des distorsions qu'elles pourraient créer, leur effet sur la sécurité alimentaire serait variable. Ces différents développements ont permis de proposer différents canaux par lesquels ces deux types de politiques affecteraient la sécurité alimentaire. Dans le chapitre 3, nous avons testé empiriquement, sur la base d'une approche de modélisation en plusieurs étapes, l'impact du dégré d'ouverture commerciale sur les disponibilités alimentaires. Nos résultats révèlent que l'ouverture commerciale et la production ont un effet positif sur ces dernières. Cependant, l'effet de l'interaction entre ces deux variables est non significatif. Si nos résultats confirment également l'importance des facteurs de production agricole, des niveaux de production des autres secteurs de l'économie et, de la volatilité des prix aux producteurs dans les résultats de production agricole, ils révèlent également, outre les facteurs traditionnels, le rôle des libertés économiques dans les décisions d'ouverture commerciale. Enfin, dans le chapitre 4, nous avons testé empiriquement, en utilisant un modèle de traitement continu et l'estimation d'une fonction dose-réponse avec endogénéïté, l'impact des mesures de soutien à l'agriculture sur la dépendance aux importations alimentaires des pays en développement et émergents. Nos résultats suggèrent des effets variables qui dépendraient de l'intensité de soutien à l'agriculture. Nos résultats confirment aussi le rôle des dépenses de consommation, de la taille de la population et des niveaux de production agricole dans les importations de produits alimentaires au profit de ces pays. / The objective of this thesis is to explore the impact of trade and agricultural support policies on food security. It focuses on developing and emerging countries, taking into account the importance of the agricultural sector in these countries. Trade and agricultural support policies in these countries tend to be quite varied and this variety could translate into food security outcomes. We are interested in whether and to what extent the temporal variability of the above policies would affect food availability or food import dependence. To do so, we use theoretical and empirical literature and test models of empirical analysis. In Chapter 1, we review the concept of food security and its measurement tools. While several definitions of food security are proposed, the idea in this chapter is to identify simple instruments on which national and international policy action could focus for setting food security objectives in developing countries. Our analysis suggests a plurality of instruments, evolving according to the angles or dimensions of analysis of food security. Among them, we distinguish between measures of food availability and measures of dependence on food imports, which we use as measures or indicators of food security in this work. In Chapter 2, we reviewed the literature on the relationship between trade policies and the dimensions of food security on the one hand, and between agricultural support measures and the dimensions and/or indicators of food security on the other. While in the first case we concluded that agricultural production is important in the analysis of such a relationship, in the second case we found that, given the variety of agricultural support measures, the complexity of calculating a single agricultural support indicator and the classification of measures with regard to the distortions they could create, their effect on food security would vary. These different developments have made it possible to propose different channels through which these two types of policies would affect food security. In Chapter 3, we empirically tested the impact of trade openness on food availability using a multi-stage modeling approach. Our results show that trade openness and production have a positive effect on food availability. However, the effect of the interaction between these two variables is not significant. While our results also confirm the importance of agricultural inputs, output levels in other sectors of the economy, and producer price volatility in agricultural production outcomes, they also reveal, in addition to traditional factors, the role of economic freedoms in trade openness decisions. Finally, in Chapter 4, we empirically tested the impact of agricultural support measures on food import dependence in developing and emerging countries using a continuous treatment model and the estimation of a dose-response function with endogeneity. Our results suggest variable effects depending on the intensity of agricultural support. Our results also confirm the role of consumer spending, population size and agricultural production levels in food imports to these countries.

Ce mémoire examine le rôle de l'action communautaire au Québec dans la réalisation de la justice alimentaire. Au moyen des outils ethnographiques propres à l'anthropologie, un cas y est examiné en détails : le projet MAÏS réalisé dans la MRC de Portneuf, qui cherche à favoriser la sécurité alimentaire des habitantes et habitants de la région. L'action de cette initiative y est analysée à travers trois des principales dimensions du concept de justice alimentaire, soit la portée de l'action (de palliative à transformatrice), la reconnaissance des inégalités structurelles et les processus démocratiques. Y sont mises en évidence les forces et les limites de l'action communautaire pour favoriser la justice sociale dans le système alimentaire. L'utilisation du concept de justice alimentaire ayant peu pénétré les milieux de la recherche francophone, en particulier ceux du Québec, ce mémoire cherche à ouvrir ce champ en proposant une adaptation de ses outils au contexte québécois. / This master's thesis examines the role of community action in Quebec in achieving food justice. Using ethnographic tools, a case is examined in detail: the MAÏS project carried out in the MRC of Portneuf, which seeks to promote food security for the inhabitants of the region. This initiative is analyzed through three of the main dimensions of the food justice concept, namely the scope of the action (from palliative to transformative), the recognition of structural inequalities and democratic processes. It highlights the strengths and limitations of community action to promote social justice in the food system. The use of the concept of food justice having little penetrated the French-speaking research circles, in particular those of Québec; this thesis seeks to open this field by proposing an adaptation of its tools to the context of the province of Québec.

Au Québec, la Loi visant à lutter contre la pauvreté et l'exclusion sociale mandate aux gouvernements d'apporter des stratégies prévenant ces deux phénomènes. Toutefois, des études remarquent une tendance vers le workfare, soit l'activation des bénéficiaires vers l'autonomie et l'emploi (Binet, Lambert, & Molgat, 2024; Charron, 2019). Plusieurs bénéficiaires se retrouvent en situation d'aller-retour entre les mesures d'assistances et les emplois précaires. Ainsi, malgré l'objectif d'autonomie, les solutions proposées se soldent parfois par le maintien dans la pauvreté. Cette situation soulève des questions concernant les logiques de protection sociale, notamment l'espace laissé aux aspirations des individus dans leurs parcours. La notion d'aspiration apparaît comme un appui intéressant en sciences de l'orientation puisqu'elle génère l'espoir et la motivation dans la sortie de la pauvreté. Cette étude explore le soutien accordé par l'État québécois dans l'atteinte des aspirations des personnes en situation de pauvreté. Pour ce faire, elle adopte une méthode de recherche qualitative en deux phases. La première phase consiste en une revue narrative de la littérature scientifique pour retracer les propos de participants vivant en situation de pauvreté. Ensuite, deux analyses documentaires examinent premièrement la documentation (communications officielles, rapports, auditions publiques, publicités, etc.) émise par des acteurs gouvernementaux (ministères, agences gouvernementales, ministres, etc.) puis la documentation (rapports, lettres ouvertes, courts-métrages, etc.) émise par les acteurs militants (regroupements communautaires, associations de défense des droits, etc.). Les résultats rendent compte de trois dimensions. Premièrement, il est question des aspirations des personnes en situation de pauvreté au Québec. Ensuite, une analyse de la façon dont les stratégies gouvernementales tiennent comptent de ces aspirations est présentée. Finalement, la perception des acteurs concernés par ces stratégies en regard des aspirations est exposée. La discussion suggère une meilleure collaboration entre les intervenants dans une visée d'intégration des aspirations aux trajectoires de sorties de la pauvreté. / In Quebec, the Act to Combat Poverty and Social Exclusion states that governments must develop strategies to prevent poverty and social exclusion. However, recent studies highlight trends towards workfare models, emphasizing activation of welfare recipients towards autonomy and employment (Binet, Lambert, & Molgat, 2024; Charron, 2019). Thus, many people find themselves cycling between welfare and precarious employment. Despite the aim of autonomy, these solutions often fail to address persistent poverty. This raises questions over the efficiency of welfare policies, especially in regard to integrating people's aspirations along their pathways. Aspirations may become a key component in vocational counseling, as they foster hope and motivation to overcome poverty. This study investigates role of Quebec's public support in achieving aspirations of individuals living in poverty. A two-phase qualitative research approach is employed. First, a narrative analysis of the scientific literature was carried out to describe people's experiences of poverty. Then, two analyses were performed: one based on official documents (such as communications, reports and public announcements) from governmental actors (ministries, government agencies, etc.), and another on documents (including reports, open letters and brief documentaries) from activist organizations (community coalitions, social rights groups, etc.). Results first describe aspirations of individuals living in poverty in Québec, then investigate government strategies to address these aspirations. The study then discusses stakeholders' perceptions, suggesting a more collaborative approach to integrating aspirations in strategies for overcoming poverty.

La virtualisation est une technologie dont la popularité ne cesse d’augmenter dans le monde de l’entreprise, et ce pour l’efficacité et la facilité de gestion qu’elle apporte. Cependant, le problème majeur de cette technologie est la sécurité. Dans cette thèse, nous proposons de renforcer la sécurité des systèmes virtualisés et nous introduisons de nouvelles approches pour répondre aux différents besoins en sécurité de cette technologie et aussi aux aspects liés à à son fonctionnement et son déploiement. Nous proposons une nouvelle architecture de supervision qui permet de contrôler la totalité de la plateforme virtualisée en temps réel. L’idée est de simuler une supervision décentralisée (plusieurs postes) sur un seul poste physique. Nous étudions les avantages et les limites de cette approche et nous montrons que cette solution est incapable de réagir é à un certain nombre d’attaques nouvelles. Comme remède, nous introduisons une nouvelle procédure qui permet de sécuriser les ressources critiques d’un système virtualisé pour s’assurer que des familles d’attaques ne peuvent être exécutées en ayant accès à ces ressources. Nous introduisons une variante de LTL avec de nouveaux opérateurs de passé et nous démontrons comment des politiques de sécurité formulées à l’aide de ce langage peuvent être facilement traduites en signatures d’attaques qui sont indispensables à la détection des intrusions dans le système. Nous analysons aussi l’impact d’une communication réseau non sécurisée entre machines virtuelles sur la sécurité globale du système virtualisé. Nous proposons un modèle d’une politique de sécurité multi-niveaux qui couvre la majorité des opérations liées au réseau et qui peuvent être exécutées par une machine virtuelle. Notre modèle couvre aussi des opérations de gestion de l’infrastructure virtualisée et étudie les contraintes de sécurité qui doivent être satisfaites. / Virtual machine technology is rapidly gaining acceptance as a fundamental building block in enterprise data centers. It is most known for improving efficiency and ease of management. However, the central issue of this technology is security. We propose in this thesis to enforce the security of virtualized systems and introduce new approaches that deal with different security aspects related not only to the technology itself but also to its deployment and maintenance. We first propose a new architecture that offers real-time supervision of a complete virtualized architecture. The idea is to implement decentralized supervision on one single physical host. We study the advantages and the limits of this architecture and show that it is unable to react according to some new stealthy attacks. As a remedy, we introduce a new procedure that permits to secure the sensitive resources of a virtualized system and make sure that families of attacks can not be run at all. We introduce a variant of the LTL language with new past operators and show how policies written in this language can be easily translated to attack signatures that we use to detect attacks on the system. We also analyse the impact that an insecure network communication between virtual machines can have on the global security of the virtualized system. We propose a multilevel security policy model that covers almost all the network operations that can be performed by a virtual machine. We also deal with some management operations and introduce the related constraints that must be satisfied when an operation is performed.

L’intégration de la Turquie à l’Union européenne pose la question de l’essence de cette construction, de ses origines, de son devenir et de sa sécurité. Cette thèse a pour objet de proposer une analyse de l’évolution des coopérations politiques et militaires entre l’Europe et la Turquie, d’en envisager les perspectives et les opportunités futures, à travers l’étude des paramètres passés et actuels de la Politique de défense et de sécurité commune, mais également de l’implication et du rôle de la Turquie dans la construction de l’Europe de la défense depuis 1945. Il s’agit de cerner les enjeux de ce débat, à la lumière des approches convergentes et divergentes de la sécurité européenne et internationale des deux partenaires. Il s’agit également de circonscrire les lacunes, définir les besoins et déterminer le cadre adéquat de l’existence de ce partenariat, au regard des mutations récentes de la scène internationale. Du début de la République kémaliste à nos jours, la Turquie, dans l’étau des continents européen et asiatique, a préféré s’associer et imaginer son futur avec les Européens. La position inédite de la Turquie dans l’architecture de la défense européenne repose sur l’attachement de la Turquie au cercle occidental, à ses valeurs et à ses desseins. Elle a toujours cherché à participer et à peser dans l’équation de la sécurité en Europe. La Turquie est membre de l’OTAN, de l’OSCE et coopère avec les Européens en matière de sécurité, grâce aux multiples forums institutionnalisés à cet effet et auxquels elle contribue. La Turquie est européenne dans sa démarche de sécurité. Elle est de culture plurielle mais toujours liée aux intérêts occidentaux, dont elle partage les valeurs et les comportements de sécurité. Malgré une Histoire contemporaine commune, échaudée par des différends encore d’actualité, comme la situation sur l’île de Chypre, elle n’est pas perçue par la communauté internationale comme faisant définitivement partie du bloc occidental. La Turquie est considérée comme un pont, un rempart ou une médiatrice entre deux mondes, que certains analystes comme Samuel Huntington, aime opposer. La Politique de sécurité et de défense commune de l’Union européenne souffre de nombreux maux. Les Etats membres n’accordent pas suffisamment de crédits à cette politique non intégrée et ne lui offre pas les moyens capacitaires de mettre en oeuvre la Stratégie européenne de sécurité. Elle est mise en échec par le manque de détermination politique des Etats membres et par leur trop faible engagement diplomatique et militaire. Les différentes politiques mises en place depuis la signature des accords Berlin plus ont certes permis la conduite de nombreuses opérations militaires et civiles, mais elles ont maintenu certaines problématiques, accentuées par l’élargissement de l’Union européenne. Néanmoins la clarification des relations transatlantiques, dont la Turquie est à l’initiative, peut être considérée comme l’alpha de la légitimation du développement d’une Europe de la défense parallèle à l’OTAN. La démarche constructiviste privilégiée dans cette thèse, invite le lecteur à lire le chantier de la sécurité européenne comme construit par les apports et les perceptions, intérieurs et extérieurs au projet européen. [...] / The Turkish candidacy to European Union points out the question of the origins, the future and the security construction of EU. Through the studies of past and actual parameters of the defense and security common policy and also regarding the involvement of Turkey in the construction of EU defense policy, this thesis proposes an analysis of the politic and military cooperation's between Turkey and EU members from 1945 until today. The Turkish and the European visions of European and international security might converge or diverge somehow, but our aim is to determinate the challenges, the needs, and the lacks of their partnership in order to draw a compatible frame according to the recent changes of the international scene. The Constructivist approach highlighted in this thesis, invites the reader to understand the European project of security as designed by the internai and external feedings and perceptions to the European project. Taking into account the past common initiatives, and keeping in mind the feedbacks related to the needs of both Common Security and Defense Policy and Turkish security system; it seems obvious to question ourselves on the benefits of the enlargement to Turkey for the EU security policy (1). It appears possible to understand the future dimension of European and Turkish policies, but also to appreciate their potential impact on the global order, by the analysis of the several European apprehensions and the political evolution of Turkey (II).

Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA. / Software-based architectures pose challenges for security experts. Many studieshave aimed to develop theoretical solutions, methodological guides and recommendations to enhance security and protect these systems.One solution proposed is to integrate security patterns as methodological solutions to adapt to the specificities of the considered architectures. Such a solution is considered reliable if it solves a security problem without affecting systemrequirements. Once an architecture model implements the security patterns, it is necessary to formally validate this new model against the expected requirements. Model checking techniques allow this validation by verifying, on one hand, that theproperties of the security patterns are respected and, on the other hand, that the properties of the initial model are preserved.In this thesis work, we study the methods and concepts to generate architectural models that meet specific security requirements. Starting with a software architecture model, a security policy and a library of security patterns, we want to generate a secure architecture. Each security pattern is described by aformal description of its structure and behavior, as well as a formal description of the security properties associated with that pattern.This thesis reports work on the technical exploitation of formal verification of properties, using model-checking.The idea is to be able to generate an architecture model that implements security patterns, and to verify that the security properties, as well as the model requirements, are respected in the resulting architecture.In perspective, the results of our work could be applied to define a methodology for a better validation of the security of industrial systems like SCADA.

Cette thèse porte sur la sécurité des patients, plus particulièrement dans le domaine de la radiothérapie, spécialité médicale qui utilise des rayonnements ionisants pour le traitement des cancers. Si cette technique contribue à l'amélioration de la prise en charge des patients, elle présente des risques qui peuvent conduire à des conséquences graves sur leur santé, comme en témoignent les derniers accidents ayant eu lieu en France. Le caractère collectif de la construction des traitements notamment, engageant quatre métiers différents, peut être à la fois une source de défaillance et une ressource pour la sécurité. L'objectif de cette thèse est d'apporter des éléments de compréhension sur la gestion de la sécurité en radiothérapie et de fournir des pistes d'amélioration de la sécurité des patients, au travers du développement de la culture collective de sécurité. Plus spécifiquement, il s'agit de comprendre comment les professionnels gèrent, individuellement et collectivement, les contraintes et les ressources disponibles afin de répondre aux objectifs de production de la santé et de la sécurité des patients. Pour ce faire, trois études empiriques ont été conduites : dans un premier temps, 14 sujets (médecins, physiciens médicaux, dosimétristes et manipulatrices) ont analysé des situations d'écart à la norme ; dans un second temps, l'activité des manipulatrices a été analysée au moyen d'observations in situ ; dans un dernier temps, 14 physiciens médicaux ont pu, via des allo-confrontations individuelles, commenter des dosimétries réalisées par leurs confrères. Cinq résultats principaux ont été mis en évidence : - le manque de procédures formelles relatives à la sécurité des patients ; - l'existence de sous-cultures de sécurité propres aux professions et aux établissements ; - une gestion de la sécurité qui repose sur la sécurité gérée, c'est-à-dire fondée sur les connaissances que possèdent les opérateurs sur les situations, l'organisation et l'activité de leurs collègues, et qui, dans la majorité des cas, s'éloigne des règles formelles ; - une gestion de la qualité qui repose davantage sur les règles formelles (qualité réglée), issues des référentiels thérapeutiques et des démarches d'assurance-qualité ; - un besoin de développement durable de la culture collective de sécurité, c'est-à-dire fondée sur la conscience partagée à propos des risques, d'une part, et sur la présence de l'activité de tous dans l'activité de chacun, d'autre part. L'analyse de la sécurité (ou de l'insécurité) dans ce secteur médical peut fournir des idées nouvelles quant aux modèles de fiabilité humaine et organisationnelle. Cette thèse débouche sur une vision de la sécurité totale qui articule qualité et sécurité – réglées ou gérées – où la qualité est tributaire de la sécurité. Les résultats ont montré que la sécurité totale repose en partie sur la connaissance du travail des collègues. De manière générale et de façon à pouvoir assurer la sécurité totale, c'est-à-dire la production de la qualité (santé) en sécurité, il faut accorder aux organisations des ressources matérielles et humaines ainsi qu'une place au développement du collectif et de l'organisation prescrite.