L’externalisation des données dans le Cloud a engendré de nouvelles problématiques de sécurité. L’enjeu est de protéger les données des utilisateurs et leur vie privée. En ce sens, deux principes ont été suivis durant cette thèse : le premier est d’avoir une confiance limitée envers l’hébergeur de données (entre autres), le deuxième est d’établir une architecture basée sur un modulede confiance placé en rupture entre le poste client et le Cloud, d’où l’approche "Trust The Module,Not The Cloud" (TTM).Déléguer donc les opérations de sécurité à un module matériel dédié permet alors plusieurs bénéfices : d’abord s’affranchir d’un poste client davantage vulnérable face à des attaques internes ou externes ; ensuite limiter les composants logiciels au strict minimum afin d’avoir un meilleur contrôle du fonctionnement et enfin dédier les opérations cryptographiques à des co-processeurs spécialisés afin d’obtenir des performances élevées. Ainsi, les travaux menés durant cette présente thèse suivent trois axes. Dans un premieraxe nous avons étudié les défis d’un Cloud personnel destiné à protéger les données d’un particulier, et basé sur une carte nano-ordinateur du marché peu coûteuse. L’architecture que nous avons définie repose sur deux piliers : une gestion transparente du chiffrement grâce à l’usage d’un chiffrement par conteneur appelé Full Disk Encryption (FDE), initialement utilisédans un contexte de protection locale (chiffrement du disque d’un ordinateur ou d’un disque dur externe) ; et une gestion transparente de la distribution grâce à l’usage du protocole iSCSI qui permet de déporter le conteneur sur le Cloud. Nous avons montré que ces deux piliers permettent de construire un service sécurisé et fonctionnellement riche grâce à l’ajout progressif de modules"sur étagère" supplémentaires.Dans un deuxième axe, nous nous sommes intéressés au problème de performance lié à l’usage du FDE. Une étude approfondie du mode de chiffrement XTS-AES recommandé pour le FDE, du module noyau Linux dm-crypt et des co-processeurs cryptographiques (ne supportant pas tous le mode XTS-AES), nous ont conduit à proposer différentes optimisations dont l’approche extReq, qui étend les requêtes cryptographiques envoyées aux co-processeurs. Ces travaux nousont ainsi permis de doubler les débits de chiffrement et déchiffrement.Dans un troisième axe, afin de passer à l’échelle, nous avons utilisé un module de sécurité matériel (Hardware Secure Module ou HSM) certifié et plus puissant, dédié à la protection des données et à la gestion des clés. Tout en capitalisant sur l’architecture initiale, l’ajout du module HSM permet alors de fournir un service de protection adapté aux besoins d’une entreprise par exemple. / Data outsourcing to the Cloud has led to new security threats. The main concerns of this thesis are to protect the user data and privacy. In particular, it follows two principles : to decrease the necessary amount of trust towards the Cloud, and to design an architecture based on a trusted module between the Cloud and the clients. Both principles are derived from a new design approach : "Trust The Module, Not The Cloud ".Gathering all the cryptographic operations in a dedicated module allows several advantages : a liberation from internal and external attacks on client side ; the limitation of software to the essential needs offers a better control of the system ; using co-processors for cryptographic operations leads to higher performance.The thesis work is structured into three main sections. In the first section , we confront challenges of a personal Cloud, designed to protect the users’ data and based on a common and cheap single-board computer. The architecture relies on two main foundations : a transparent encryption scheme based on Full Disk Encryption (FDE), initially used for local encryption (e.g., hard disks), and a transparent distribution method that works through iSCSI network protocol in order to outsource containers in Cloud.In the second section we deal with the performance issue related to FDE. By analysing the XTS-AES mode of encryption, the Linux kernel module dm-crypt and the cryptographic co-processors, we introduce a new approach called extReq which extends the cryptographic requests sent to the co-processors. This optimisation has doubled the encryption and decryption throughput.In the final third section we establish a Cloud for enterprises based on a more powerful and certified Hardware Security Module (HSM) which is dedicated to data encryption and keys protection. Based on the TTM architecture, we added "on-the-shelf" features to provide a solution for enterprise.

La virtualisation matérielle telle que mise en oeuvre dans le cloud computing, permet le partage de ressources matérielles entre plusieurs machines virtuelles pouvant appartenir à différents utilisateurs. Ce partage des ressources constitue l’atout majeur de ces infrastructures,qui permet aux fournisseurs d’exploiter plus efficacement les ressources des centres de données, notamment à travers l’allocation dynamique des ressources. Cependant, le partage des ressources introduit de nouvelles contraintes de sécurité. Plusieurs travaux de l’état de l’art ont démontré l’apparition de nouvelles stratégies d’attaques propres aux infrastructures cloud computing, exploitant le partage des ressources. Néanmoins, il a aussi été démontré qu’il est possible de tirer avantage de la position privilégiée de la couche de virtualisation pour offrir une meilleure sécurité que celle assurée dans les plate-formes traditionnelles d’hébergement en silo. Cette thèse poursuit deux axes de recherche complémentaires. Le premier axe traite des nouvelles vulnérabilités liées aux infrastructures cloud computing. Nous avons démontré une attaque que nous appelons attaque par "migrations intempestives de machines virtuelles", dans laquelle un attaquant parvient à amener le système de gestion dynamique de ressources à migrer de façon abusive des machines virtuelles, par simple manipulation des quantités de ressources consommées par des machines virtuelles qui sont sous son contrôle. Nous avons démontré cette attaque sur une plate-forme constituée de cinq serveurs et analysé les conditions nécessaires à son succès ainsi que l’exposition des clusters vis-à-vis de la vulnérabilité qu’elle exploite. Le second axe propose de tirer avantage de la position privilégiée de l’opérateur qui dispose à la fois d’une vue multi-couches plus riche de l’utilisation des ressources et d’une vue plus globale des contextes d’exécution des machines virtuelles, comparativement à la vue limitée de l’utilisateur, pour offrir une meilleure sécurité. Nous avons proposé AMAD (Abusive VM Migration Attack Detection), un système de supervision, chargé de détecter l’occurrence des attaques par migrations intempestives de machines virtuelles et d’identifier de façon automatique celles à l’origine de l’attaque. AMAD est implémenté sur notre plate-forme d’expérimentation et évalué à l’aide de traces de consommation de machines virtuelles collectées sur des clouds réels. Les résultats d’évaluation montrent qu’AMAD opère avec une bonne précision de détection. / Hardware virtualisation is the core technology which enables resource sharing among multiple virtual machines possibly belonging to different tenants within cloud infrastructures. Resources haring is the main feature that enables cost effectiveness of cloud platforms, achieved through dynamic resource management. However, resource sharing brings several new security concerns. Several proofs of concepts have demontrated new attack strategies brought by the resource sharing paradigm, known as cross-virtual machine attacks. Even so, it is also showed that the priviligied position of the virtualisation layer can be leveraged to offer better security protection mecanisms than the ones offered in non virtualized platfoms.This thesis follows two main objectives. The first one is related to the domain of cloud-specific vulnerabilities. We have demonstrated a new attack, called the abusive virtual machine migration attack, in which an attacker can leverage the sharing of resources, through the manipulation of the amounts of resources consumed by virtual machines under his control, to abusively enforce the dynamic resource management system to trigger virtual machine migrations. We have demonstrated this attack on a virtualized platform composed of five physical machines, the necessary conditions for the attack to succeed and the vulnerability exposure of clusters against this kind of attack is also analyzed. The second main contribution of this thesis aims at leveraging the privilged position of the cloud provider who has both a more reliable view of the ressource utilisation and a more complete view of the virtual machine execution contexts compared to the limited view of cloud users, to provide better security. We propose AMAD (Abusive Virtual Machine Migration Attack Detection), a system designed for detecting an abusive use of the dynamic virtual machine migration, in the case of the abusive virtual machine migration attack. AMAD identifies the virtual machines possibly at the origin of the attack by analyzing their resource consumption profiles which show fluctuation and correlation in the usage of resources. We have implemented AMAD on top of our laboratory platform and evaluated it with the help of virtual machine resource consumption traces collected from real cloud. Our evaluation results show that AMAD identifes the attacking virtual machines with high detection accuracy.

Ce mémoire présente un langage déclaratif de description de scénarios et de modèles d’attaques, ainsi qu’un moteur de détection qui lui est associé. Le langage s’inspire fortement de l’état de l’art dans le domaine des IDS (système de détection d’intrusions) et il s’approprie les qualités de plusieurs de ses références telles que LTL, Snort, Lambda, ou Chronicle. Il représente aussi une évolution majeure de la première version introduite dans un précédent travail, dans le sens où nous avons introduit de nouveaux opérateurs, nous avons associé une sémantique formelle au langage, ainsi qu’un système de règles de réécriture permettant le calcul d’une forme normale ; nous offrons aussi la possibilité de définir des modèles d’attaques. Les modèles étant différents des scénarios, le comportement du moteur de détection a été enrichi, augmentant l’expressivité du langage par rapport à sa version initiale.

L'internet est devenu un environnement omniprésent dans le monde du travail et du loisir. La popularité sans cesse croissante des applications web ainsi que des services associés entraînent l'exécution de nombreuses transactions critiques, qui soulèvent des questions de sécurité. Du fait de cette croissance, des efforts ont été entrepris durant cette dernière décennie pour rendre les applications web plus sûres. Malgré ces efforts, de récents rapports provenant de l'institut SANS estiment que plus de 60 % des attaques commises sur l'Internet ciblent les applications web en se concentrant sur les vulnérabilités inhérentes aux problèmes de validation, comme le Cross-Site Scripting ou les injections SQL. Dans cette thèse, nous avons conduit deux études de recherche empirique, analysant un grand nombre d'application web vulnérables. Nous avons assemblé une base de données contenant plus de 10.000 rapports de vulnérabilités depuis l'an 2000. Ensuite, nous avons analysé ces données pour déterminer si les développeurs ont pris conscience des problématiques de sécurité web de nos jours, comparé à la période où ces applications émergeaient. Puis nous avons analysé l'étroit lien entre le langage de programmation utilisé pour développer l'application web et le nombre de vulnérabilité reporté. Avec ces résultats empiriques comme base, nous présentons notre solution IPAAS qui aide les développeurs novice en termes de sécurité à écrire des applications sécurisées par défaut. Nous montrons par ailleurs que cette technique améliore de manière probante la sécurité des applications web. / The web has become a backbone of our industry and daily life. The growing popularity of web applications and services and the increasing number of critical transactions being performed, has raised security concerns. For this reason, much effort has been spent over the past decade to make web applications more secure. Despite these efforts, recent data from SANS institute estimates that up to 60% of Internet attacks target web applications and critical vulnerabilities such as cross-site scripting and SQL injection are still very common. In this thesis, we conduct two empirical studies on a large number of web applications vulnerabilities with the aim of gaining deeper insights in how input validation flaws have evolved in the past decade and how these common vulnerabilities can be prevented. Our results suggest that the complexity of the attacks have not changed significantly and that many web problems are still simple in nature. Our studies also show that most SQL injection and a significant number of cross-site scripting vulnerabilities can be prevented using straight-forward validation mechanisms based on common data types. With these empirical results as foundation, we present IPAAS which helps developers that are unaware of security issues to write more secure web applications than they otherwise would do. It includes a novel technique for preventing the exploitation of cross-site scripting and SQL injection vulnerabilities based on automated data type detection of input parameters. We show that this technique results in significant and tangible security improvements for real web applications.

Titre de l'écran-titre (visionné le 5 juin 2023) / Les menaces internes, ou en anglais Insider Threat, surviennent lorsqu'un individu ayant des accès privilégiés au sein d'une organisation les utilise d'une façon causant du tort à l'organisation. L'employé peut réaliser ces actions dangereuses de façon intentionnelle ou non intentionnelle. Les menaces internes sont très variées ce qui les rend particulièrement complexes à détecter. La confidentialité, l'intégrité et la disponibilité des données sont des préoccupations croissantes pour les organisations d'aujourd'hui. Malgré tout, l'étendue de l'impact des menaces internes est souvent sous-estimée. En effet, même si les menaces internes ne représentent qu'une fraction de toutes les cyberattaques, les dangers en lien avec les menaces internes sont réels. Dans un premier lieu, les attaques internes peuvent causer plus de dommages aux organisations que les attaques traditionnelles. Ceci s'explique en partie par la grande connaissance de l'organisation, ainsi que les accès privilégiés, qu'ont les employés réalisant ces attaques. Ces derniers sont donc en mesure de facilement perpétrer des actions dangereuses sans éveiller de soupçons. De plus, dans les dernières années, plusieurs études suggèrent que la majorité des organisations souffrent de menaces internes chaque année [2]. La détection de menaces internes est ainsi un problème pertinent qui attire beaucoup de chercheurs. Une des stratégies couramment utilisée pour faire la détection de menaces internes est de modéliser les comportements des employés d'une organisation et d'identifier toute divergence significative comme une menace potentielle. Pour ce faire, les journaux d'audit, décrivant tous les évènements réalisés par les membres d'une organisation dans le réseau informatique, sont des sources d'informations privilégiées dans le domaine pour apprendre les comportements typiques des utilisateurs. Dans ce mémoire, nous présentons deux solutions originales de détection de menaces internes utilisant des journaux d'audit et des techniques d'apprentissage automatique non supervisé afin d'apprendre les comportements utilisateur et détecter les comportements malicieux. Les deux solutions présentent des résultats compétitifs par rapport à l'état de l'art, et ce en offrant des caractéristiques qui facilitent leur implémentation dans de vraies organisations. / Insider threats occur when a privileged member of an organization wrong fully uses his access in a way that causes harm to his organization. Those damaging actions can be intentional, as in the case of theft or sabotage, however, un intentional dangerous actions are also to be considered, which adds to the complexity of the insider threat. The insider threat is a broad type of cyber menace, making its detection particularly difficult. For organizations, the confidentiality, integrity, and availability of their information are an increasing concern. Yet many under estimate the magnitude of the insider threats against the maintenance of those ideals. Indeed, even though insider threats are only a fraction of all existing cyber threats, this type of menace presents a real and unique danger for organizations. Firstly, an insider threat can be more damaging to an organization than a traditional cyberattack. This is mainly explicable by the privileged accesses and great domain knowledge that the insider possesses over an outsider. The insider has then a better opportunity to use his access and domain knowledge to carry out efficiently and quietly the attack. Moreover, over the last few years, some reports suggest that most institutions yearly suffer from that kind of cyber threat [2]. Insider threat detection is therefore a relevant problem that attracted many researchers to deploy their efforts in the last decades. One common strategy to detect malicious insiders is by modeling the behaviors of the users and identifying any significant divergence as a potential threat. In that matter, audit data, describing the activity of every member of an organization in the network, are regularly chosen to learn user behaviors using statistical or machine learning models. In the present work, we propose two insider threat detection systems that leverage audit data to learn user behaviors and detect divergent conduct in an unsupervised fashion. Both solutions are competitive with state-of-the-art techniques, and were developed considering many challenges in the field, like being easy to implement in a real-world scenario and considering events dependencies.

Titre de l'écran-titre (visionné le 28 février 2024) / Avec l'avènement de la technologie de la chaîne de blocs, un nouveau type de contrat appelé contrat intelligent a émergé. Les contrats intelligents sont des programmes informatiques permettant de formaliser des accords contractuels complexes tout en assurant automatiquement le respect de ces accords sans l'aide d'intermédiaires de confiance. Aujourd'hui, ils gèrent des millions de dollars en jetons numériques et effectuent des tâches quotidiennes de processus métier. Compte tenu des énormes enjeux financiers, les pirates informatiques sont plus que jamais motivés à exploiter tout bogue dans les contrats intelligents ou l'infrastructure sous-jacente. Une grande prudence est donc requise avant le déploiement des contrats intelligents, d'autant plus qu'ils deviennent immuables (*pas de possibilité de les modifier*) une fois déployés sur la chaîne de blocs. Écrire des contrats intelligents sécurisés et fiables est une tâche ardue et les méthodes existantes de sécurisation des contrats intelligents reposent largement sur l'expérience du programmeur, laissant ainsi place à des erreurs de logique et d'inattention. Dans cette thèse, nous proposons une approche novatrice basée sur la réécriture de programmes pour renforcer la sécurité des contrats intelligents. Plus précisément, étant donné un contrat intelligent *S* et une politique de sécurité *ϕ*, nous dérivons un nouveau contrat intelligent *S'* à partir de *S* et de *ϕ* de telle sorte que *S′* satisfait la politique de sécurité *ϕ* et reste correct par rapport à *S*. Le contrat *S′* (*c'est-à-dire le contrat sécurisé*) est celui qui sera en fin de compte déployé sur la chaîne de blocs. L'approche présentée utilise l'algèbre SBPA$^\textup{*}_\textup{0,1}$ qui est une variante de BPA$^\textup{*}_\textup{0,1}$ (*Basic Process Algebra*) étendue avec des variables, des environnements et des conditions pour formaliser et résoudre le problème. Le problème de trouver la version sécuritaire *S′* à partir de *S* et de *ϕ* se transforme en un problème de résolution d'un système d'équations linéaires pour lequel nous savons déjà comment extraire la solution dans un temps polynomial. Cette recherche contribue à combler le fossé dans la sécurisation des contrats intelligents et ouvre la voie à une adoption plus large de cette technologie révolutionnaire. / With the advent of blockchain technology, a new type of contract called smart contract has emerged. Smart contracts are computer programs to formalize complex contractual agreements while automatically ensuring compliance with these agreements without the help of trusted intermediaries. Today, they manage millions of dollars in digital tokens and perform daily business process tasks. Given the huge financial stakes, hackers are more motivated than ever to exploit any bugs in smart contracts or the underlying infrastructure. Great caution is therefore required before deploying smart contracts, especially since they become immutable (*no possibility to modify them*) once deployed on the blockchain. Writing secure and reliable smart contracts is a daunting task and existing methods of securing smart contracts rely heavily on the experience of the programmer, leaving room for errors of logic and carelessness. In this thesis, we propose an innovative approach based on program rewriting to strengthen the security of smart contracts. Specifically, given a smart contract *S* and a security policy *ϕ*, we derive a new smart contract *S′* from *S* and *ϕ* such that *S′* satisfies the security policy *ϕ* and remains correct with respect to *S*. The *S′* contract (*i.e. the secure contract*) is the one that will ultimately be deployed on the blockchain. The presented approach uses the algebra SBPA$^\textup{*}_\textup{0,1}$ which is a variant of BPA$^\textup{*}_\textup{0,1}$ (*Basic Process Algebra*) extended with variables, environments and conditions to formalize and solve the problem. The problem of finding the secure version *S′* from *S* and *ϕ* turns into a problem of solving a system of linear equations for which we already know how to extract the solution in polynomial time. This research helps bridge the gap in securing smart contracts and paves the way for wider adoption of this game-changing technology.

Dans le monde d'aujourd'hui où la plupart des aspects de la vie moderne sont traités par des systèmes informatiques, la vie privée est de plus en plus une grande préoccupation. En outre, les données ont été générées massivement et traitées en particulier dans les deux dernières années, ce qui motive les personnes et les organisations à externaliser leurs données massives à des environnements infonuagiques offerts par des fournisseurs de services. Ces environnements peuvent accomplir les tâches pour le stockage et l'analyse de données massives, car ils reposent principalement sur Hadoop MapReduce qui est conçu pour traiter efficacement des données massives en parallèle. Bien que l'externalisation de données massives dans le nuage facilite le traitement de données et réduit le coût de la maintenance et du stockage de données locales, elle soulève de nouveaux problèmes concernant la protection de la vie privée. Donc, comment on peut effectuer des calculs sur de données massives et sensibles tout en préservant la vie privée. Par conséquent, la construction de systèmes sécurisés pour la manipulation et le traitement de telles données privées et massives est cruciale. Nous avons besoin de mécanismes pour protéger les données privées, même lorsque le calcul en cours d'exécution est non sécurisé. Il y a eu plusieurs recherches ont porté sur la recherche de solutions aux problèmes de confidentialité et de sécurité lors de l'analyse de données dans les environnements infonuagique. Dans cette thèse, nous étudions quelques travaux existants pour protéger la vie privée de tout individu dans un ensemble de données, en particulier la notion de vie privée connue comme confidentialité différentielle. Confidentialité différentielle a été proposée afin de mieux protéger la vie privée du forage des données sensibles, assurant que le résultat global publié ne révèle rien sur la présence ou l'absence d'un individu donné. Enfin, nous proposons une idée de combiner confidentialité différentielle avec une autre méthode de préservation de la vie privée disponible. / In nowadays world where most aspects of modern life are handled and managed by computer systems, privacy has increasingly become a big concern. In addition, data has been massively generated and processed especially over the last two years. The rate at which data is generated on one hand, and the need to efficiently store and analyze it on the other hand, lead people and organizations to outsource their massive amounts of data (namely Big Data) to cloud environments supported by cloud service providers (CSPs). Such environments can perfectly undertake the tasks for storing and analyzing big data since they mainly rely on Hadoop MapReduce framework, which is designed to efficiently handle big data in parallel. Although outsourcing big data into the cloud facilitates data processing and reduces the maintenance cost of local data storage, it raises new problem concerning privacy protection. The question is how one can perform computations on sensitive and big data while still preserving privacy. Therefore, building secure systems for handling and processing such private massive data is crucial. We need mechanisms to protect private data even when the running computation is untrusted. There have been several researches and work focused on finding solutions to the privacy and security issues for data analytics on cloud environments. In this dissertation, we study some existing work to protect the privacy of any individual in a data set, specifically a notion of privacy known as differential privacy. Differential privacy has been proposed to better protect the privacy of data mining over sensitive data, ensuring that the released aggregate result gives almost nothing about whether or not any given individual has been contributed to the data set. Finally, we propose an idea of combining differential privacy with another available privacy preserving method.

La détection automatique de contenu toxique en ligne est un sujet très important aujourd’hui. Les modérateurs ne peuvent filtrer manuellement tous les messages et les utilisateurs trouvent constamment de nouvelles façons de contourner les filtres automatiques. Dans ce mémoire, j’explore l’impact que peut avoir la détection de sentiment pour améliorer trois points importants de la détection automatique de toxicité : détecter le contenu toxique de façon plus exacte ; rendre les filtres plus difficiles à déjouer et prédire les conversations les plus à risque. Les deux premiers points sont étudiés dans un premier article, où l’intuition principale est qu’il est plus difficile pour un utilisateur malveillant de dissimuler le sentiment d’un message que certains mots-clés à risque. Pour tester cette hypothèse, un outil de détection de sentiment est construit, puis il est utilisé pour mesurer la corrélation entre sentiment et toxicité. Par la suite, les résultats de cet outil sont utilisés comme caractéristiques pour entraîner un modèle de détection de toxicité, et le modèle est testé à la fois dans un contexte classique et un contexte où on simule des altérations aux messages faites par un utilisateur tentant de déjouer un filtre de toxicité. La conclusion de ces tests est que les informations de sentiment aident à la détection de toxicité, particulièrement dans un contexte où les messages sont modifiés. Le troisième point est le sujet d’un second article, qui a comme objectif de valider si les sentiments des premiers messages d’une conversation permettent de prédire si elle va dérailler. Le même outil de détection de sentiments est utilisé, en combinaison avec d’autres caractéristiques trouvées dans de précédents travaux dans le domaine. La conclusion est que les sentiments permettent d’améliorer cette tâche également. / Automatic toxicity detection of online content is a major research field nowadays. Moderators cannot filter manually all the messages that are posted everyday and users constantly find new ways to circumvent classic filters. In this master’s thesis, I explore the benefits of sentiment detection for three majors challenges of automatic toxicity detection: standard toxicity detection, making filters harder to circumvent, and predicting conversations at high risk of becoming toxic. The two first challenges are studied in the first article. Our main intuition is that it is harder for a malicious user to hide the toxic sentiment of their message than to change a few toxic keywords. To test this hypothesis, a sentiment detection tool is built and used to measure the correlation between sentiment and toxicity. Next, the sentiment is used as features to train a toxicity detection model, and the model is tested in both a classic and a subversive context. The conclusion of those tests is that sentiment information helps toxicity detection, especially when using subversion. The third challenge is the subject of our second paper. The objective of that paper is to validate if the sentiments of the first messages of a conversation can help predict if it will derail into toxicity. The same sentiment detection tool is used, in addition to other features developed in previous related works. Our results show that sentiment does help improve that task as well.

Les pare-feu sont des éléments cruciaux pour le renforcement de la politique de sécurité d’un réseau. Ils ont été largement déployés pour sécuriser les réseaux privés, mais leur configuration reste complexe et sujette de plusieurs anomalies. Au cours des dernières années, plusieurs techniques et outils ont été proposés pour configurer correctement un pare-feu. Cependant, la plupart de ces techniques restent informelles et ne prennent pas en compte la performance globale du réseau ou d’autres paramètres de qualités de services. Dans ce mémoire, nous introduisons une approche formelle permettant de configurer optimalement et formellement un réseau de sorte qu’il respecte une politique de sécurité donnée tout en tenant compte de ses qualités de services. / Firewalls are crucial elements in enforcing network security policies. They have been widely deployed for securing private networks but, their configuration remains complex and error prone. During the last years, many techniques and tools have been proposed to correctly configure firewalls. However, most of existing works are informal and do not take into account the global performance of the network or other qualities of its services (QoS). In this thesis we introduce a formal approach allowing to formally and optimally configure a network so that a given security policy is respected and by taking into account the QoS.

La sécurité des systèmes d’information est l’une des préoccupations les plus importantes du domaine de la science informatique d’aujourd’hui. Les particuliers et les entreprises sont de plus en plus touchés par des failles de sécurité et des milliards de dollars ont été perdus en raison de cyberattaques. Cette thèse présente une approche formelle basée sur la réécriture de programmes permettant d’appliquer automatiquement des politiques de sécurité sur des programmes non sécuritaires. Pour un programme P et une politique de sécurité Q, nous générons un autre programme P’ qui respecte une politique de sécurité Q et qui se comporte comme P, sauf si la politique est sur le point d’être violée. L’approche présentée utilise l’algèbre [symbol] qui est une variante de [symbol] (Basic Process Algebra) étendue avec des variables, des environnements et des conditions pour formaliser et résoudre le problème. Le problème de trouver la version sécuritaire P’ à partir de P et de Q se transforme en un problème de résolution d’un système linéaire pour lequel nous savons déjà comment extraire la solution par un algorithme polynomial. Cette thèse présente progressivement notre approche en montrant comment la solution évolue lorsqu’on passe de l’algèbre de [symbol] à [symbol]. / The security of information systems is one of the most important preoccupations of today’s computer science field. Individuals and companies are more and more affected by security flaws and billions of dollars have been lost because of cyber-attacks. This thesis introduces a formal program-rewriting approach that can automatically enforce security policies on non-trusted programs. For a program P and a security policy Q, we generate another program P’ that respects the security policy Q and behaves like P except when the enforced security policy is about to be violated. The presented approach uses the [symbol] algebra that is a variant of the BPA (Basic Process Algebra) algebra extended with variables, environments and conditions to formalize and resolve the problem. The problem of computing the expected enforced program [symbol] is transformed to a problem of resolving a linear system for which we already know how to extract the solution by a polynomial algorithm. This thesis presents our approach progressively and shows how the solution evolves when we move from the [symbol] algebra to the [symbol] algebra.