La conception de circuits complexes, tels que les processeurs, nécessite un prototypage itératif afin d’explorer diverses caractéristiques micro architecturales et d’obtenir des performances optimales. Ce processus repose usuellement sur l’utilisation des langages de description matérielle comme Verilog qui nécessitent beaucoup de travail et sont sujets aux erreurs. Modifier un design impose souvent une réécriture significative du code HDL, rendant la conception itérative et l’exploration de l’espace de conception fastidieuses et inefficaces, en particulier avec l’augmentation de la complexité matérielle. La synthèse de haut niveau (HLS) offre une alternative en permettant aux concepteurs de décrire le comportement des processeurs dans des langages de haut niveau comme le C/C++. Cependant, comme la HLS repose sur un ordonnancement statique, elle gère de manière conservatrice les dépendances dans le processeur, dégradant ainsi les performances en augmentant l’intervalle d’initiation (II). Ce manuscrit propose une méthodologie pour concevoir des processeurs entièrement pipelinés en HLS sans exposer les détails du pipeline dans la spécification de haut niveau. Les contributions principales incluent des techniques de multi-threading statique et dynamique, un mécanisme d’ordonnancement dynamique et une architecture multi-coeur. Ces innovations permettent un pipelining efficace, une exploration rapide de l’espace de conception ainsi qu’une exécution performante. Les designs proposés sont validées sur FPGA, démontrant leur praticité et leur performances.

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.

Les modèles d'apprentissage profond basés sur les CNNs offrent des performances de pointe dans les tâches de traitement d'images et de vidéos, en particulier pour l'amélioration ou la classification d'images. Cependant, ces modèles sont lourds en calcul et en empreinte mémoire, ce qui les rend inadaptés aux contraintes de temps réel sur des FPGA embarqués. Il est donc essentiel de compresser ces CNNs et de concevoir des architectures d'accélérateurs pour l'inférence qui intègrent la compression dans une approche de co-conception matérielle et logicielle. Bien que des optimisations logicielles telles que l'élagage aient été proposées, elles manquent souvent de structure nécessaire à une intégration efficace de l'accélérateur. Pour répondre à ces limitations, cette thèse se concentre sur l'accélération des CNNs sur FPGA tout en respectant les contraintes de temps réel sur les systèmes embarqués. Cet objectif est atteint grâce à plusieurs contributions clés. Tout d'abord, elle introduit l'élagage des motifs, qui impose une structure à la sparsité du réseau, permettant une accélération matérielle efficace avec une perte de précision minimale due à la compression. Deuxièmement, un accélérateur pour l'inférence de CNN est présenté, qui adapte son architecture en fonction des critères de performance d'entrée, des spécifications FPGA et de l'architecture du modèle CNN cible. Une méthode efficace d'intégration de l'élagage des motifs dans l'accélérateur et un flux complet pour l'accélération de CNN sont proposés. Enfin, des améliorations de la compression du réseau sont explorées grâce à la quantification de Shift\&Add, qui modifie les méthodes de multiplication sur FPGA tout en maintenant la précision du réseau de base.

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.

Dans cette thèse, nous nous intéressons aux systèmes de gestion d’identité totalement distribués respectant la vie privée. Ces systèmes ont pour but de permettre à un utilisateur de s’authentifier et d’être autorisé par un fournisseur de services, tout en ne lui révélant que les informations strictement nécessaires. De plus, ces systèmes doivent être résilients à la présence de processus malveillant. Dans ce contexte, nous nous intéressons à deux points. D’abord, aux certificats anonymes et à leur propriétés de respect de la vie privée. Nous identifions un manque qui réduit cette propriété dans l’état de l’art, et nous le corrigeons grâce à un nouveau type de signature : les certificats anonymes à émetteurs cachés. Ensuite, nous nous intéressons aux algorithmes distribués utilisés pour les propriétés annexes des systèmes de gestion d’identité distribués, notamment pour la révocation de certificats, ou la gestion de clés publiques. Nous analysons formellement ces problèmes, notamment du point de vue de leur consensus number. Ces analyses nous permettent finalement de proposer des algorithmes pour implémenter un système de gestion de l’identité totalement distribué qui nécessite une synchronisation réduite. En d’autres termes, un système où l’utilisation d’algorithmes de consensus est réduite au minimum.

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.