Les noyaux de systèmes d'exploitation manipulent des données fournies par les programmes utilisateur via les appels système. Si elles sont manipulées sans prendre une attention particulière, une faille de sécurité connue sous le nom de Confused Deputy Problem peut amener à des fuites de données confidentielles ou l'élévation de privilèges d'un attaquant. Le but de cette thèse est d'utiliser des techniques de typage statique afin de détecter les manipulations dangereuses de pointeurs contrôlés par l'espace utilisateur. La plupart des systèmes d'exploitation sont écrits dans le langage C. On commence par en isoler un sous-langage sûr nommé Safespeak. Sa sémantique opérationnelle et un premier système de types sont décrits, et les propriétés classiques de sûreté du typage sont établies. La manipulation des états mémoire est formalisée sous la forme de lentilles bidirectionnelles, qui permettent d'encoder les mises à jour partielles des états et variables. Un première analyse sur ce langage est décrite, permettant de distinguer les entiers utilisés comme bitmasks, qui sont une source de bugs dans les programmes C. / Operating system kernels need to manipulate data that comes from user programs through system calls. If it is done in an incautious manner, a security vulnerability known as the Confused Deputy Problem can lead to information disclosure or privilege escalation. The goal of this thesis is to use static typing to detect the dangerous uses of pointers that are controlled by userspace. Most operating systems are written in the C language. We start by isolating Safespeak, a safe subset of it. Its operational semantics as well as a type system are described, and the classic properties of type safety are established. Memory states are manipulated using bidirectional lenses, which can encode partial updates to states and variables. A first analysis is described, that identifies integers used as bitmasks, which are a common source of bugs in C programs. Then, we add to Safespeak the notion of pointers coming from userspace. This breaks type safety, but it is possible to get it back by assigning a different type to the pointers that are controlled by userspace. This distinction forces their dereferencing to be done in a controlled fashion. This technique makes it possible to detect two bugs in the Linux kernel: the first one is in a video driver for an AMD video card, and the second one in the ptrace system call for the Blackfin architecture.

À mesure que le nombre d’objets capables de communiquer croît, le besoin de sécuriser leurs interactions également. La conception des protocoles cryptographiques nécessaires pour cela est une tâche notoirement complexe et fréquemment sujette aux erreurs humaines. La vérification formelle de protocoles entend offrir des méthodes automatiques et exactes pour s’assurer de leur sécurité. Nous nous intéressons en particulier aux méthodes de vérification automatique des propriétés d’équivalence pour de tels protocoles dans le modèle symbolique et pour un nombre non borné de sessions. Les propriétés d’équivalences ont naturellement employées pour s’assurer, par exemple, de l’anonymat du vote électronique ou de la non-traçabilité des passeports électroniques. Parce que la vérification de propriétés d’équivalence est un problème complexe, nous proposons dans un premier temps deux méthodes pour en simplifier la vérification : tout d’abord une méthode pour supprimer l’utilisation des nonces dans un protocole tout en préservant la correction de la vérification automatique; puis nous démontrons un résultat de typage qui permet de restreindre l’espace de recherche d’attaques sans pour autant affecter le pouvoir de l’attaquant. Dans un second temps nous exposons trois classes de protocoles pour lesquelles la vérification de l’équivalence dans le modèle symbolique est décidable. Ces classes bénéficient des méthodes de simplification présentées plus tôt et permettent d’étudier automatiquement des protocoles taggués, avec ou sans nonces, ou encore des protocoles ping-pong. / As the number of devices able to communicate grows, so does the need to secure their interactions. The design of cryptographic protocols is a difficult task and prone to human errors. Formal verification of such protocols offers a way to automatically and exactly prove their security. In particular, we focus on automated verification methods to prove the equivalence of cryptographic protocols for a un-bounded number of sessions. This kind of property naturally arises when dealing with the anonymity of electronic votingor the untracability of electronic passports. Because the verification of equivalence properties is a complex issue, we first propose two methods to simplify it: first we design a transformation on protocols to delete any nonce while maintaining the soundness of equivalence checking; then we prove a typing result which decreases the search space for attacks without affecting the power of the attacker. Finally, we describe three classes of protocols for which equivalence is decidable in the symbolic model. These classes benefit from the simplification results stated earlier and enable us to automatically analyze tagged protocols with or without nonces, as well as ping-pong protocols.

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.

L'avènement d'Internet révolutionne l'accès à l'information, mais contribue également à l'essor de nouveaux services, notamment le commerce électronique, à l'allègement de la bureaucratie et à l'arrivée d'une multitude de e-services. Or, le développement de cette technologie de l'information s'est accompagné d'une panoplie de problématiques. Parmi celles-ci, les plus inquiétantes ont trait à la sécurité puisqu'elles mettent en péril le bon fonctionnement de ces services. Le présent mémoire approfondit ces problématiques de sécurité selon une approche formelle : les algèbres de processus. Dans un premier temps, le fruit de la recherche sur les failles de sécurité réseau de niveau deux et trois de la couche TCP/IP et d'une étude comparative de l'expressivité des principales algèbres de processus est présenté. Dans un second temps, les caractéristiques souhaitées d'une algèbre de modélisation de réseau sont mises en exergue et sont intégrées dans la syntaxe et la sémantique d'une nouvelle algèbre. Finalement, une nouvelle algèbre de processus pour la modélisation de réseau, Netcal, ainsi que les principes d'un système de détection de failles d'architecture et de configuration de réseau sont explicités.

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.

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.

Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2022 / Alors que les appareils de tous les jours deviennent de plus en plus intelligents et interconnectés, il existe un besoin d'appareils intégrés dotés de capacités de traitement étendues qui favorisent des cycles de développement courts. Dans les applications IoT (Internet of Things), il est également nécessaire que ces dispositifs intégrés soient à faible consommation d'énergie et à faible latence pour traiter efficacement les données de plusieurs capteurs en parallèles. Ce besoin peut être largement satisfait par les dispositifs SoC FPGA ou System-on-Chip Field Programmable Gate Array (en français, systèmes sur puce intégrant des circuits logiques programmables). Les dispositifs SoC FPGA intègrent un HPS (Hard Processing System) étroitement lié à une structure FPGA. Tout en permettant un délai de conception rapide par rapport aux dispositifs ASIC (Application-Specific Integrated Circuit) traditionnels, le SoC FPGA permet d'apporter des mises à niveau matérielles aux dispositifs déployés via ses diverses interfaces. De plus, la combinaison du HPS avec le FPGA apporte de nombreux avantages aux applications comme l'intelligence artificielle en permettant la mise en œuvre avec facilité de circuits massivement parallèles. Cependant, le problème avec les dispositifs SoC FPGA réside dans la manière dont les données de configuration sont stockées. Par exemple, dans les dispositifs ASIC, le circuit est implémenté directement dans le silicium. Alors qu'un acteur malveillant pourrait effectuer la rétro-ingénierie du silicium pour récupérer la fonction du circuit, un tel exploit nécessite des équipements coûteux, des connaissances approfondies et un processus fastidieux. Cependant, étant donné que les FPGA sont composés d'une structure reconfigurable, les données de configuration doivent être stockées dans une structure de mémoire à l'intérieur de l'appareil. L'extraction de ces données pourrait fournir à un acteur malveillant des informations précieuses sur le fonctionnement du circuit sans nécessairement impliquer le processus de rétro-ingénierie matérielle long et coûteux. Ce mémoire se concentre sur l'aspect cybersécurité des dispositifs SoC FPGA qui pourraient mettre en péril les données de configuration du FPGA. Par exemple, alors que les périphériques FPGA traditionnels peuvent être correctement sécurisés en limitant l'accès aux interfaces directement connectées à la mémoire des données de configuration, les interconnexions complexes du HPS avec le FPGA ajoutent un niveau de complexité qui transfère nécessairement la tâche de sécuriser le périphérique aux développeurs. Cette complexité accrue est la principale préoccupation étudiée dans ce mémoire. Nous visons à produire un modèle générique de menace de cybersécurité pour les dispositifs SoC FPGA afin de fournir une base de référence sur laquelle les concepteurs peuvent s'appuyer tout en effectuant l'analyse de cybersécurité de leurs conceptions. Nous effectuons un examen approfondi des attaques existantes sur les appareils SoC FPGA et identifions les vulnérabilités potentielles. L'une des vulnérabilités identifiées, qui concerne les effets des injections de fautes électromagnétiques, fait l'objet d'une étude approfondie de sa faisabilité. Une deuxième vulnérabilité identifiée, liée à la mémoire synchrone dynamique à accès aléatoire (SDRAM) est confirmée via une démonstration pratique qui exploite le processus de démarrage du dispositif SoC FPGA. / As everyday devices become increasingly intelligent and further interconnected, there is a need for integrated devices with extensive processing capabilities that favour short development cycles. In applications of the Internet of Things (IoT), there is a further need for these integrated devices to be low-power and low-latency to efficiently process data from multiple sensors in a parallel fashion. This need can largely be met by Systems on a Chip (SoC) Field Programmable Gate Array (FPGA) devices. SoC FPGA devices incorporate a hard processing system (HPS) intricately connected with an FPGA fabric. While allowing for a quick design turnaround time compared to traditional Application-Specific Integrated Circuit (ASIC) devices, SoC FPGA conveniently allows for hardware upgrades to be brought to deployed devices through its various interfaces. Furthermore, the combination of the HPS with the FPGA brings many advantages to applications such as artificial intelligence by allowing massively parallel circuits to be implemented with relative ease. However, how the configuration data is stored is a concern with SoC FPGA devices. For instance, in ASIC devices, the circuit is implemented directly within the silicon. While a malicious actor could reverse engineer the silicon to retrieve the circuit's function, such a feat requires expensive equipment, extensive expert knowledge, and a tedious process. However, since FPGA devices are composed of a reconfigurable fabric, one must store the configuration data within a memory structure inside the device. Extracting this data could provide a malicious actor with valuable insight into the circuit's function without necessarily implicating the expensive and time-consuming hardware reverse engineering process. This thesis focuses on the cybersecurity aspect of SoC FPGA devices that could jeopardize the FPGA's configuration data. For instance, while one can adequately secure traditional FPGA devices by limiting access to interfaces directly connected to configuration data's memory, the HPS's intricate interconnections with the FPGA add a level of complexity that necessarily handovers the task of securing the device to the developers. This increased complexity is the primary concern being investigated in this thesis. We aim to derive a generic cybersecurity threat model for SoC FPGA devices to provide a baseline for designers to build upon while performing the cybersecurity analysis of their designs. We provide a thorough review of existing attacks on SoC FPGA devices and identify potential vulnerabilities. One of the identified vulnerabilities, which deals with the effects of electromagnetic fault injections, is the subject of an in-depth investigation into its feasibility. A second identified vulnerability related to the Synchronous Dynamic Random Access Memory (SDRAM) is confirmed via a practical demonstration that exploits the boot process of the SoC FPGA device.