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.
- Directrice de thèse: Clémentine MAURICE, Chargée de recherche, CNRS, France. - Co-directrice de thèse: Sandrine BLAZY, Professeure, Université de Rennes, France. - Président: Mohamed SABT, Professeur, Université de Rennes, France. - Examinateur: Aurélien FRANCILLON, Professeur, EURECOM, France. - Examinateur: Peter SCHWABE, Scientific Director, Max Planck Institute for Security and Privacy, Allemagne. - Rapporteur: Jean-Yves MARION, Professeur, Université de Lorraine, France. - Rapporteur: Mathias PAYER, Associate Professor, EPFL, Suisse.
Thesis of the team Spirals defended on 02/12/2025
français
English