| Binary analysis for microarchitectural security (Analyse de code binaire pour la sécurité microarchitecturale) | ||
Geimer, Antoine - (2025-12-02) / Université de Rennes Binary analysis for microarchitectural security Langue : Anglais Directeur de thèse: Maurice, Clémentine; Blazy, Sandrine Laboratoire : IRISA Ecole Doctorale : MATISSE Thématique : Informatique | ||
Mots-clés : canaux auxiliaires, constant-time, Spectre, exécution symbolique, SGX, Systèmes informatiques -- Mesures de sûreté Résumé : Les attaques microarchitecturales menacent l’isolation dans les environnements cloud, permettant à une VM malveillante ou au fournisseur cloud d’accéder à des données sensibles. Pour s'y prémunir, les développeurs recourent à des techniques de programmation "temps constant" et des mécanismes d'enclave comme Intel SGX, des approches demeurant imparfaites. Dans cette thèse, nous renforçons la sécurité microarchitecturale à travers trois contributions. Nous proposons d’abord une rétrospective des outils de détection de vulnérabilités par canal auxiliaire, avec une classification multi-critère. Nous concevons un benchmark commun permettant de les comparer correctement, et de les évaluer sur des vulnérabilités connues. Nous identifions alors des fonctionnalités manquantes et formulons des recommandations pour de futurs outils de détection. Nous étendons ce benchmark pour créer une approche de test différentiel, identifiant les vulnérabilités par canal auxiliaire introduites par la compilation. Nous analysons manuellement ces vulnérabilités afin d’identifier précisément les optimisations problématiques. Nos résultats montrent que la désactivation ciblée de celles-ci améliore significativement la résilience à ce type d'attaque, sans dégradation notable des performances. Enfin, nous étendons un outil d’exécution symbolique dédié aux binaires SGX afin de détecter les vulnérabilités Spectre. Notre approche est inspirée de travaux antérieurs mais adaptée au modèle mémoire spécifique utilisé. Elle permet d’améliorer significativement le passage l'échelle de l’analyse des enclaves SGX, rendant ainsi l’exploration de larges programmes réalisable en pratique. Résumé (anglais) : Microarchitectural attacks threaten isolation in cloud environments, allowing a malicious VM or the provider to retrieve sensitive data. Developers protect themselves with constant-time programming and secure hardware such as Intel SGX, however these approaches are imperfect. In this thesis, we improve microarchitectural security in three contributions. We offer a retrospective on the literature on side-channel vulnerability detection with a multi-criteria classification of proposed tools. We create a common benchmark to compare them fairly and evaluate them on known vulnerabilities. Using these insights, we identified missing features and issued recommendations to the community for future detection tools. We then extend this benchmark to create a differential testing approach for finding compiler-introduced side-channel vulnerabilities. With this corpus of vulnerabilities, we manually analyze the optimization pipeline to properly identify a set of problematic optimizations. We found that disabling these optimizations improved the side-channel security of cryptographic libraries, without sacrificing performance. Finally, we extend a symbolic execution tool for SGX binaries to find Spectre vulnerabilities. Our approach is inspired from previous works, adapted to the specific memory model used. This improves significantly the scalability of SGX enclave analysis, making exploration beyond toy examples feasible. Identifiant : rennes1-ori-wf-1-21803 | ||
| Exporter au format XML |