La cryptanalyse traditionnelle repose souvent sur des méthodes heuristiques et statistiques, mais les outils automatisés ont récemment suscité une attention particulière. Cette thèse explore leur application pour améliorer la cryptanalyse de chiffrements spécifiques. Nous revisitons d’abord les attaques boomerang à clés liées sur AES, en introduisant un modèle MILP avancé pour gérer les générations de sous-clés non linéaires, ce qui permet de réduire considérablement la complexité temporelle par rapport aux approches précédentes. Ensuite, nous améliorons l’attaque par rebond sur la fonction de hachage Grøstl avec un modèle MILP unifié qui automatise la recherche de chemins différentiels dans les phases entrantes et sortantes. Enfin, nous étendons le cadre MITM différentiel des chiffrements AndRX orientés mots aux chiffrements orientés bits, en proposant le premier modèle bit par bit automatisé pour identifier les attaques MITM différentielles complètes pour ces chiffrements. Les résultats présentés dans cette thèse mettent en évidence le potentiel des outils automatisés pour améliorer la cryptanalyse des chiffrements par blocs modernes et des fonctions de hachage, ouvrant la porte à de nouvelles avancées possibles dans la lutte contre des conceptions cryptographiques de plus en plus complexes.

Les dispositifs haptiques portables procurent des sensations tactiles tout en restant compacts. Ils ont été peu utilisés en réalité augmentée (RA), où le contenu virtuel est intégré à la perception du monde réel. Dans cette thèse, nous étudions leur utilisation pour améliorer les interactions de la main avec des objets virtuels et augmentés en RA. Nous commençons par étudier l'impact du rendu visuel sur la perception des textures vibrotactiles virtuelles qui augmentent des surfaces réelles touchées directement par le doigt. Nous proposons un système d’augmentation de textures visuo-haptiques à l'aide d'un casque de RA et d'un dispositif vibrotactile portable. Nous évaluons ensuite comment la rugosité perçue des textures augmentées diffère lorsqu'elles sont touchées via une main virtuelle, en réalité virtuelle (RV) et en RA, ou par sa propre main. Nous étudions alors le réalisme et la cohérence de la combinaison des textures augmentées visuelles et haptiques en RA. Nous étudions ensuite comment des retours sensoriels visuo-haptiques augmentant la main améliorent les performances et l’expérience utilisateur lors de la manipulation d'objets virtuels en RA. Nous commençons par étudier l'effet de six retours visuels de la main virtuelle comme augmentation de la main réelle. Nous évaluons ensuite deux techniques de contact vibrotactile à quatre endroits différents sur la main et nous les comparons à deux augmentations visuelles de la main.

Cette thèse porte sur la synthèse automatique de processeurs à jeu d'instructions en utilisant la synthèse de haut niveau (HLS). En particulier, nous visons à générer automatiquement des cœurs de processeurs pipelinés in-order à partir d'une description de haut niveau en C sous la forme d'un simulateur de jeu d'instructions (ISS). Au cours de notre travail, nous avons développé un flot de conception matérielle entièrement automatisé qui permet de compiler une description algorithmique en circuit spéculatif, SpecHLS. Nous proposons un ensemble de transformations de code basées sur le pipeline spéculatif de boucles, afin de révéler des opportunités de spéculation sur le flot de contrôle et la mémoire dans du code C, et nous générons du code spéculatif synthétisable à l'aide d'une chaîne d'outils de HLS commerciale. SpecHLS est capable de gérer plusieurs spéculations entremêlées, des spéculations indépendantes dans des modules matériels découplés, ainsi que la spéculation mémoire. Notre travail aboutit à un flot de conception capable de générer plusieurs instances de processeurs RISC-V in-order à partir d'un ISS. Nous montrons que nous pouvons explorer efficacement un espace de conception avec des centaines de milliers de configurations matérielles spéculatives possibles en quelques minutes, et générer des processeurs compétitifs avec des cœurs de processeurs embarqués.

Cette dissertation introduit et formalise la notion de structures comme moyen mathématique de capturer diverses propriétés dans plusieurs domaines scientifiques. Nous définissons les représentations structurelles comme des arbres ou des graphes acycliques dirigés (DAG) de structures, où la sémantique globale est la composition des structures individuelles, permettant un raisonnement inductif et modulaire. Nous formaliserons les notions de représentations inductives et de représentations canoniquement inductives. Nous étudions les conditions nécessaires et suffisantes pour que les représentations structurelles soient canoniques, en introduisant le concept de « confluence structurelle », non formalisée auparavant, et en proposant plusieurs approximations. Nous appliquons notre théorie aux fonctions Booléennes, montrant qu'elle unifie la plupart des variantes de diagrammes de décision binaire tout en suggérant une manière systématique d'en concevoir de nouvelles. Enfin, nous discutons brièvement de leur mise en œuvre et des résultats expérimentaux encourageants, qui soutiennent notre affirmation selon laquelle les représentations basées sur la structure sont conçues pour une utilisation pratique.

Depuis 2018, la technologie blockchain a vu émerger de nombreuses applications, allant de la crypto-monnaie aux systèmes de santé. La plupart des blockchains existantes adoptent un modèle de réplication complète. D'un point de vue juridique, la nature entièrement répliquée des blockchains signifie que les données personnelles sont susceptibles d'être stockées sur des nœuds répartis dans différents pays. D'un point de vue technique, la réplication complète offre une bonne tolérance aux pannes, mais au détriment de la mise à l'échelle. Il est nécessaire de développer des solutions qui peuvent garantir la tolérance aux pannes avec des niveaux de réplication plus raisonnables, tout en protégeant la vie privée et en évitant les conflits avec les réglementations. Pour répondre à ces problèmes, nous proposons deux systèmes. Le premier est basé sur le partitionnement horizontal (sharding) de la blockchain afin de mieux répartir les coûts de stockage et de traitement des données entre des sous-ensembles de pairs. Le second ne repose pas sur le consensus. Il peut donc effectuer des transactions indépendantes simultanément. Cette solution introduit également un ensemble de primitives cryptographiques dont la combinaison permet d'anonymiser les échanges de données des utilisateurs et de vérifier leur légitimité, sans révéler ni stocker de données sensibles.

Les futurs réseaux mobiles, 5G et au-delà, sont confrontés à des défis importants pour répondre aux demandes croissantes de services plus rapides, plus fiables et plus innovants. Pour y faire face, les technologies d'intelligence artificielle (IA) peuvent être utilisées pour optimiser les performances du réseau en fonction des besoins et du comportement des utilisateurs. Notre travail présente une méthode pour comprendre le comportement des utilisateurs dans les réseaux mobiles, en mettant l'accent sur l'identification de l'environnement de l'utilisateur et du type d'application. Nous utilisons des modèles d'apprentissage profond pour analyser les mesures radio et le trafic réseau. Nous avons également exploré la combinaison d'informations a priori avec des modèles d'apprentissage automatique pour améliorer les performances, en utilisant une approche d'optimisation du comportement de l'utilisateur (UBO). De plus, nous avons démontré le potentiel de l'apprentissage de représentation et de l'apprentissage fédéré dans les réseaux mobiles, qui peuvent préserver les ressources de bande passante et atténuer les préoccupations concernant la centralisation des données.

Cette thèse porte sur la preuve automatique de propriétés concernant la relation entrée/sortie de programmes fonctionnels manipulant des types de données algébriques (ADT). De récents résultats montrent comment approximer un programme fonctionnel en utilisant un automate d'arbre. Bien qu'expressives, ces techniques ne peuvent pas prouver de propriété reliant l'entrée et la sortie d'une fonction, par exemple qu'inverser une liste préserve sa longueur. Dans cette thèse, nous nous appuyons sur ces résultats et définissons une procédure pour calculer ou sur-approximer une telle relation. Formellement, le problème de la vérification de programmes se réduit à la satisfiabilité de clauses, que nous résolvons en exhibant un modèle. Dans cette thèse, nous proposons deux représentations relationnelles de ces modèles de Herbrand : les automates d'arbres convolués et les shallow Horn clauses. Les automates d'arbres convolués généralisent les automates d'arbres et sont généralisés par les shallow Horn clauses. Le problème d'inférence du modèle de Herbrand découlant de la vérification relationnelle étant indécidable, nous proposons une procédure d'inférence incomplète mais correcte. Les expériences montrent que cette procédure est performante en pratique par rapport aux outils actuels, à la fois pour la vérification des propriétés et pour la recherche de contre-exemples.

La programmation temps constant est utilisée pour produire des programmes immunisés contre les attaques temporelles. Cependant, cette discipline impose plusieurs contraintes au développeur de logiciels, ce qui rend la mise en œuvre complexe et les programmes résultants parfois plus lents. Nous proposons un nouveau mécanisme de protection spécialisé pour les systèmes embarqués qui est implémenté dans le matériel mais utilisable à partir du logiciel. Grâce à cette protection, les contraintes de la programmation temps constant peuvent être assouplies, ce qui rend cette discipline plus simple et permet de produire des programmes plus rapides. Cette protection fonctionne en verrouillant des parties de la mémoire dans le cache, de sorte que les accès vers ces parties de la mémoire soient protégés contre les attaques temporelles. Nous réutilisons les techniques de preuve utilisées pour certifier le compilateur CompCert. Dans notre cas, nous l'utilisons pour certifier qu'aucune attaque par cache ne peut exposer nos accès mémoire protégés. Nous montrons le gain de performance permis par notre nouvelle protection sur plusieurs algorithmes cryptographiques, et nous proposons une nouvelle méthode de tri rapide qui est temps constant grâce ce mécanisme de verrouillage du cache.

Cette thèse se penche sur les systèmes distribués tolérants les pannes, et s'intéresse plus particulièrement au problème de la diffusion fiable dans des environnements asynchrones sujets à des défaillances hybrides. Elle introduit un nouveau modèle de calcul combinant des défaillances byzantines de processus avec un adversaire de messages. Elle définit ensuite l'abstraction de Diffusion Fiable Byzantine Tolérante aux Adversaires de Messages (MBRB) et prouve sa condition de résilience optimale. Elle propose enfin trois algorithmes clés pour réaliser cette abstraction : un algorithme MBRB simple basé sur les signatures, une nouvelle primitive appelée k2l-cast pour des implémentations MBRB sans cryptographie, et un algorithme MBRB basé sur les codes correcteurs d'erreurs optimisant la complexité de communication. Ces contributions font progresser la compréhension des systèmes distribués tolérants les pannes, et participent aux fondations nécessaires à la conception d'algorithmes répartis résilients et efficaces, avec des applications dans les infrastructures critiques, les systèmes financiers et les technologies blockchain.

Un défi majeur pour les systèmes autonomes est de fonctionner dans des conditions d’incertitude du monde réel. Les robots s’appuient sur des modèles de leur environnement et d’eux-mêmes pour prendre des décisions, mais ces modèles sont intrinsèque- ment des approximations. Par conséquent, des paramètres incertains peuvent entraîner des écarts significatifs entre le comportement prévu et réel du système. Cette thèse aborde le problème des incertitudes paramétriques en développant des trajectoires intrinsèque- ment robustes. En optimisant ces trajectoires dans le cadre du système en boucle fermée à l’aide de nouveaux concepts de sensibilités d’état et d’entrée introduits dans ce travail, l’approche améliore les performances des robots dans des conditions incertaines. L’objectif principal de cette thèse est d’étendre et d’appliquer ces méthodes basées sur la sensibilité pour la planification de trajectoires robustes. La validité du cadre d’optimisation proposé est évaluée empiriquement à travers de vastes campagnes statistiques, tant en simulation que dans des expériences réelles, sur deux plateformes robotiques largement utilisées : un drone quadrirotor et un manipulateur robotique.