Thèse Vérification Formelle et Co-Conception Matériel-Logiciel pour la Sécurité Spéculative sur Architectures à Capacités H/F - Doctorat.Gouv.Fr

Établissement : Université Côte d'Azur École doctorale : STIC - Sciences et Technologies de l'Information et de la Communication Laboratoire de recherche : Secure Programming Languages & Tools for Security Direction de la thèse : Tamara REZK ORCID 0000000337440248 Début de la thèse : 2026-09-01 Date limite de candidature : 2026-05-03T23:59:59 Modern processors rely on speculative execution to improve performance, but this introduces side channels capable of bypassing architectural security guarantees. Capability architectures, such as CHERI, strengthen memory isolation and compartmentalization, but recent work shows that these guarantees are insufficient against speculative attacks. At the same time, lightweight mechanisms such as dfence propose fine-grained speculative barriers that are more efficient than traditional fences, while other approaches rely on hardware tracking of secrets.This PhD aims to develop formal foundations and practical mechanisms for speculative security on RISC-V/CHERI architectures, with extensions toward Arm Morello and x86. The goal is to combine confidentiality guarantees, performance, and deployability.

The work will be structured around four main axes.
(1) **Formal modeling:** define semantic models of speculative capability processors, incorporating pipelines, prediction, forwarding, contention, and caches, in order to reason about properties such as speculative constant-time and robust constant-time.
(2) **Analysis of existing architectures:** systematically study recent proposals such as Capability Speculation Contract, BLACKOUT, and dfence; identify their limitations under stronger attacker models; and experimentally reproduce selected attacks (port contention, speculative store/load bypass, stack leaks).
(3) **New hardware-software defenses:** design selective barriers, secret stacks, double-stack mechanisms, controlled declassification mechanisms, and integration with CHERI capabilities to express authority and confinement. Particular attention will be given to implementation in gem5 and on RISC-V cores.
(4) **Verification and compilation:** develop type systems, invariants, and mechanized proofs guaranteeing the correct placement of protections and the preservation of security properties at the compiled level, with exploration of links to Rust and CHERI.

Expected contributions include: a reproducible methodology for evaluating speculative leaks on capability architectures; new low-cost protection mechanisms; formal security proofs; and experimental prototypes on RISC-V/CHERI. This research will contribute to the design of future hardware platforms that reconcile high performance with strong confidentiality guarantees.
Les processeurs modernes utilisent l'exécution spéculative pour améliorer les performances, mais celle-ci introduit des vulnérabilités microarchitecturales. Les architectures à capacités comme CHERI renforcent l'isolation mémoire, sans garantir à elles seules la sécurité face aux attaques spéculatives. Ce projet s'inscrit à l'intersection de l'architecture des processeurs, de la cybersécurité et de la vérification formelle.

Le candidat recherché possède une solide formation en informatique, avec de bonnes bases en architecture des processeurs, systèmes, cybersécurité et méthodes formelles. Des compétences en programmation bas niveau (C assembleur) et en environnement Linux sont attendues. Une expérience en vérification formelle, compilation, microarchitecture et simulation matérielle (gem5) est indispensable. Le candidat devra faire preuve d'autonomie, de rigueur scientifique et d'un bon niveau d'anglais.