Les volumes de données multimédia ont fortement crus ces dernières années. Facebook stocke plus de 100 milliards d'images, 200 millions sont ajoutées chaque jour. Cela oblige les systèmes de recherche d'images par le contenu à s'adapter pour fonctionner à ces échelles. Les travaux présentés dans ce manuscrit vont dans cette direction. Deux observations essentielles cadrent nos travaux. Premièrement, la taille des collections d'images est telle, plusieurs téraoctets, qu'il nous faut obligatoirement prendre en compte les contraintes du stockage secondaire. Cet aspect est central. Deuxièmement, tous les processeurs sont maintenant multi-cœurs et les grilles de calcul largement disponibles. Du coup, profiter de parallélisme et de distribution semble naturel pour accélérer tant la construction de la base que le débit des recherches par lots. Cette thèse décrit une technique d'indexation multidimensionnelle s'appelant eCP. Sa conception prend en compte les contraintes issues de l'usage de disques et d'architectures parallèles et distribuées. eCP se fonde sur la technique de quantification vectorielle non structurée et non itérative. eCP s'appuie sur une technique de l'état de l'art qui est toutefois orientée mémoire centrale. Notre première contribution se compose d'extensions destinées à permettre de traiter de très larges collections de données en réduisant fortement le coût de l'indexation et en utilisant les disques au mieux. La seconde contribution tire profit des architectures multi-cœurs et détaille comment paralléliser l'indexation et la recherche. Nous évaluons cet apport sur près de 25 millions d'images, soit près de 8 milliards de descripteurs SIFT. La troisième contribution aborde l'aspect distribué. Nous adaptons eCP au paradigme Map-Reduce et nous utilisons Hadoop pour en évaluer les performances. Là, nous montrons la capacité de eCP à traiter de grandes bases en indexant plus de 100 millions d'images, soit 30 milliards de SIFT. Nous montrons aussi la capacité de eCP à utiliser plusieurs centaines de cœurs. / The scale of multimedia collections has grown very fast over the last few years. Facebook stores more than 100 billion images, 200 million are added every day. In order to cope with this growth, methods for content-based image retrieval must adapt gracefully. The work presented in this thesis goes in this direction. Two observations drove the design of the high-dimensional indexing technique presented here. Firstly, the collections are so huge, typically several terabytes, that they must be kept on secondary storage. Addressing disk related issues is thus central to our work. Secondly, all CPUs are now multi-core and clusters of machines are a commonplace. Parallelism and distribution are both key for fast indexing and high-throughput batch-oriented searching. We describe in this manuscript a high-dimensional indexing technique called eCP. Its design includes the constraints associated to using disks, parallelism and distribution. At its core is an non-iterative unstructured vectorial quantization scheme. eCP builds on an existing indexing scheme that is main memory oriented. Our first contribution is a set of extensions for processing very large data collections, reducing indexing costs and best using disks. The second contribution proposes multi-threaded algorithms for both building and searching, harnessing the power of multi-core processors. Datasets for evaluation contain about 25 million images or over 8 billion SIFT descriptors. The third contribution addresses distributed computing. We adapt eCP to the MapReduce programming model and use the Hadoop framework and HDFS for our experiments. This time we evaluate eCP's ability to scale-up with a collection of 100 million images, more than 30 billion SIFT descriptors, and its ability to scale-out by running experiments on more than 100 machines.

Les problèmes d'ordonnancement peuvent être rencontrés dans plusieurs situations de la vie courante. Organiser des activités quotidiennes, planifier un itinéraire de voyage sont autant d'exemples de petits problèmes d'optimisation que nous tentons de résoudre tous les jours sans nous en rendre compte. Mais quand ces problèmes prennent des proportions plus grandes, il devient difficile au cerveau humain de gérer tous ces paramètres et le recours à une solution informatique s'impose. Les problèmes d'ordonnancement en contexte industriel sont nombreux et celui qui retient particulièrement notre attention dans le cadre de ce mémoire est le problème d'ordonnancement de commandes sur machine unique avec temps de réglages dépendant de la séquence. Ce problème fait partie de la classe de problèmes NP-Difficiles. Etant donnée sa complexité, ce problème ne peut être résolu par une méthode exacte. Les métaheuristiques représentent ainsi une bonne alternative pour obtenir des solutions de bonne qualité dans des délais très courts. Les algorithmes génétiques, qui font partie des algorithmes évolutionnaires, sont utilisés dans ce travail pour résoudre ce problème d'ordonnancement. La prolifération des architectures parallèles a ouvert la voie à un nouvel éventail d'approches pour optimiser les algorithmes et plus spécialement les métaheuristiques. Ce mémoire propose une stratégie de parallélisation de l'algorithme génétique pour en étudier les bénéfices. Le premier algorithme génétique proposé est implémenté sur le modèle d'un algorithme de la littérature. Cet algorithme ne s'est pas avéré performant pour toute la série de problèmes test et, pour cette raison, des modifications de paramètres ont été rendues nécessaires. Ces modifications ont donné naissance à une deuxième version séquentielle dont les résultats se sont avérés satisfaisants. Une troisième version a ensuite été implémentée avec une optique d'exécution parallèle selon un modèle en îlot et une topologie en anneau unidirectionnel. Un plan d'expérience a ensuite été mis au point selon plusieurs variables et vise à identifier les meilleures configurations de l'algorithme tant sur le plan de la qualité des résultats que sur le plan de l'accélération. Les résultats obtenus dans ce mémoire montrent que l'introduction de la parallélisation dans un algorithme génétique est bénéfique à ce dernier tant sur le plan qualité des résultats que sur le plan accélération. Dans un premier temps, la version sans communications n'a pas amélioré une grande partie des problèmes mais a pu atteindre des accélérations linéaires. Par la suite, l'introduction des échanges a nettement influé sur la qualité des résultats. En effet, en adoptant une stratégie de division de la taille de la population par le nombre de processeurs, l'algorithme génétique parallèle parvient à donner des résultats équivalents voire meilleurs que la version séquentielle, et ceci pour plusieurs fréquences d'échanges entre les populations.

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 travail a été effectué dans le contexte d'un projet financé par l'ERC, Defying Amdahl's Law (DAL), dont l'objectif est d'explorer les techniques micro-architecturales améliorant la performance des processeurs multi-cœurs futurs. Le projet prévoit que malgré les efforts investis dans le développement de programmes parallèles, la majorité des codes auront toujours une quantité signifiante de code séquentiel. Pour cette raison, il est primordial de continuer à améliorer la performance des sections séquentielles des-dits programmes. Le travail de recherche de cette thèse porte principalement sur l'étude des différences entre les sections parallèles et les sections séquentielles de programmes multithreadés (MT) existants. L'exploration de l'espace de conception des futurs processeurs multi-cœurs est aussi traitée, tout en gardant à l'esprit les exigences concernant ces deux types de sections ainsi que le compromis performance-surface. / This thesis work is done in the general context of the ERC, funded Defying Amdahl's Law (DAL) project which aims at exploring the micro-architectural techniques that will enable high performance on future many-core processors. The project envisions that despite future huge investments in the development of parallel applications and porting it to the parallel architectures, most applications will still exhibit a significant amount of sequential code sections and, hence, we should still focus on improving the performance of the serial sections of the application. In this thesis, the research work primarily focuses on studying the difference between parallel and serial sections of the existing multi-threaded (MT) programs and exploring the design space with respect to the processor core requirement for the serial and parallel sections in future many-core with area-performance tradeoff as a primary goal.

La parallélisation est une solution possible pour améliorer un simulateur séquentiel s'il devient trop lent dû à une surcharge de calculs et qu'on ne désire pas concevoir à neuf un nouveau simulateur parallèle. Ce mémoire présente la conception UML d'une architecture pour un simulateur parallèle flexible et extensible capable de gérer différents environnements de déploiement par une configuration au temps d'exécution. Ce projet a vu le jour dans le but d'améliorer les performances de l'architecture KARMA, une architecture séquentielle pour la simulation d'engagements d'armes, pour réussir à atteindre le temps-réel dans une simulation haute-fidélité avec matériel dans la boucle. L'approche retenue propose une architecture non commerciale et développable à faibles coûts. L'implémentation et les tests préliminaires ont été basés sur un logiciel source libre et portable sur plusieurs plates-formes nommé ACE.

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.

Ce document présente SCOOP, un nouveau cadriciel Python pour la distribution automatique de hiérarchies de tâches dynamiques axé sur la simplicité. Une hiérarchie de tâches réfère à des tâches qui peuvent récursivement générer un nombre arbitraire de sous-tâches. L’infrastructure de calcul sous-jacente consiste en une simple liste de ressources de calcul. Le cas d’utilisation typique est l’exécution d’un programme principal sous la tutelle du module SCOOP, qui devient alors la tâche racine pouvant générer des sous-tâches au travers de l’interface standard des « futures » de Python. Ces sous-tâches peuvent elles-mêmes générer d’autres sous-sous-tâches, etc. La hiérarchie de tâches complète est dynamique dans le sens où elle n’est potentiellement pas entièrement connue jusqu’à la fin de l’exécution de la dernière tâche. SCOOP distribue automatiquement les tâches parmi les ressources de calcul disponibles en utilisant un algorithme de répartition de charge dynamique. Une tâche n’est rien de plus qu’un objet Python pouvant être appelé en conjonction avec ses arguments. L’utilisateur n’a pas à s’inquiéter de l’implantation du passage de message ; toutes les communications sont implicites. / This paper presents SCOOP, a new Python framework for automatically distributing dynamic task hierarchies focused on simplicity. A task hierarchy refers to tasks that can recursively spawn an arbitrary number of subtasks. The underlying computing infrastructure consists of a simple list of resources. The typical use case is to run the user’s main program under the umbrella of the SCOOP module, where it becomes a root task that can spawn any number of subtasks through the standard “futures” API of Python, and where these subtasks may themselves spawn other subsubtasks, etc. The full task hierarchy is dynamic in the sense that it is unknown until the end of the last running task. SCOOP automatically distributes tasks amongst available resources using dynamic load balancing. A task is nothing more than a Python callable object in conjunction with its arguments. The user need not worry about message passing implementation details; all communications are implicit.

Dans ce travail, nous définissons une nouvelle algèbre de processus basée sur CCS. Cette algèbre, qui est destinée à la sécurisation formelle de réseaux, est munie d'un opérateur de surveillance qui permet de contrôler les entrées et les sorties d'un processus, ou d'un sous-processus, à l'image d'un pare-feu dans un réseau informatique. L'algèbre permet donc de modéliser des réseaux munis de moniteurs, et également, n'importe quel système communicant devant être contrôlé par des moniteurs. Avant d'entrer dans le vif du sujet, nous débutons par une revue des approches globales en détection d'intrusions, soient l'approche comportementale et l'approche par scénarios. Nous parcourons par la suite différents langages formels destinés à la modélisation de systèmes communicants, en prêtant une attention particulière aux algèbres de processus.

Se procurer les outils les plus récents et les plus performants liés à la sécurisation de réseaux informatique est loin d'être suffisant pour réduire les risques d'intrusions. En effet, le maillon le plus faible dans la chaîne de la sécurité informatique est souvent l'intervention humaine qui est parfois nécessaire pour installer et configurer ces outils. Limiter cette intervention humaine permettra sans doute de réduire à la fois les risques et les coûts engendrés par la sécurité. Il est important, par exemple, de développer des méthodes sûres permettant de configurer automatiquement un réseau informatique de sorte que son comportement soit conforme à une politique de sécurité donnée. C'est dans cet axe de recherche que se situe ce travail. En effet, nous proposons une méthode formelle permettant de générer à partir d'une politique de sécurité (spécifiée par une formule logique) et d'un réseau informatique (spécifié par un processus) une configuration sécuritaire de ce réseau.

Cette thèse se place dans le cadre de la modélisation et de l'analyse de systèmes parallèles et répartis. Plus précisément, nous nous intéressons à la modélisation, la vérification et la supervision de systèmes, composés d'entités indépendantes interagissant localement par mémoire partagée et globalement par échange asynchrone de messages.<br /><br />Dans ce contexte, plutôt que de modéliser séparément chaque entité, puis d'analyser les comportements qui peuvent se produire lorsque ces entités interagissent, nous fournissons une théorie permettant de modéliser globalement le système considéré tout en conservant des propriétés de vérification et de supervision décidables. Cette théorie se base sur le formalisme des ordres partiels étiquetés (appelés "pomsets").<br /><br />Dans ce but, nous définissons le modèle des HMSC causaux qui étend le formalisme des HMSC en autorisant, comme pour les traces de Mazurkiewicz, certains événements à commuter sur chaque processus. Nous montrons, tout d'abord, qu'une restriction syntaxique des HMSC causaux a le même pouvoir d'expression que les réseaux bornés d'automates mixtes, un modèle qui étend les réseaux d'automates asynchrones de Zielonka et les réseaux d'automates communicants. De plus, nous montrons que les méthodes classiques de model-checking de systèmes séquentiels peuvent s'appliquer aux modèles plus concis basés sur les pomsets, comme les HMSC causaux, sans perte d'efficacité. Enfin, nous proposons des méthodes de traitement efficace d'observations volumineuses d'exécutions réparties, ainsi que des techniques de supervision, telles que le diagnostic ou la corrélation d'événements, qui utilisent des modèles basés sur les pomsets.