Dans le cadre du développement de systèmes critiques, des composants de différents niveaux de confiance et de différentes provenances (industrielle, militaire, etc.) peuvent s'exécuter sur un même processeur. Plusieurs approches permettent l'isolation de différents domaines sur une même machine. L'objectif de cette thèse est d'explorer différents mécanismes d'isolation, comme les enclaves ou les capacités (e.g. CHERI), et d'évaluer la mise en œuvre de ces mécanismes en termes de coûts (impact sur le temps d'exécution, l'occupation mémoire, la complexité du circuit, etc.) et de sécurité.
Par ailleurs, l'utilisation de produits de sécurité dans un contexte gouvernemental ou militaire passe par une évaluation de la sécurité de ces produits, typiquement une évaluation Critères Communs à un haut d'assurance (EAL7). Ce niveau d'assurance nécessite le développement d'une preuve formelle de la sûreté et de la sécurité du système. Nous proposons donc de développer des approches permettant de formaliser et prouver ces mécanismes d'isolation qui nécessitent un support à la fois du matériel et du compilateur.
Un premier objectif de cette thèse est d'implémenter, au sein d'un processeur RISC-V, des mécanismes de sécurité matériels, qui permettent d'une part à plusieurs entités ne se faisant pas confiance de s'exécuter simultanément sur un même processeur, et d'autre part de garantir la sûreté des programmes exécutés. Nous proposons de nous focaliser sur deux mécanismes complémentaires : les enclaves et les capacités.
Au-delà de l'implémentation matérielle de ces mécanismes de sécurité, un second objectif est de fournir une preuve formelle de la correction de ces mécanismes de sécurité, par exemple dans l'assistant de preuve Rocq, avec l'aide d'un solveur SMT.
Un troisième objectif est de prouver des propriétés de sécurité (sûreté mémoire, isolation, etc.) sur un système logiciel/matériel où le compilateur tire parti des mécanismes fournis par le matériel.
Ces objectifs de preuve mécanisée à l'interface logiciel/matériel font l'originalité de cette thèse.
La thèse sera co-encadrée par Sandrine Blazy, Guillaume Hiet et Pierre Wilke, et dirigée par Sandrine Blazy. Elle permettra de poursuivre une collaboration initiée dans le PEPR SecurEval autour de la preuve formelle de mécanismes de sécurité logiciel/matériel dans le cadre d'évaluations Critères Communs.
[1] Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala, Arvind. The essence of Bluespec: a core language for rule-based hardware design. PLDI 2020, pp. 243-257.
[2] Matthieu Baty, Pierre Wilke, Guillaume Hiet, Arnaud Fontaine, Alix Trieu. A Generic Framework to Develop and Verify Security Mechanisms at the Microarchitectural Level: Application to Control-Flow Integrity. CSF 2023, pp. 372-387
[3] Tony Law, Delphine Demange, Sandrine Blazy. A Mechanized Semantics for Dataflow Circuits. ACM SIGPLAN Conference on Systems, Programming, Languages, and Applications: Software for Humanity, OOPSLA 2025, pp. 507-533.
[4] Xavier Leroy. Formal verification of a realistic compiler. Communications of the ACM, 2009.
[5] Cyprien Jules, Pierre Wilke, Guillaume Hiet and Gabriel Desfrene. heRVé: towards a formally verified RISC-V processor with security mechanisms (Work in Progress). HS3 2025 (ESORICS workshop).
[6] Joonwon Choi, Jaewoo Kim, Jeehoon Kang. Revamping Verilog Semantics for Foundational Verification. OOPSLA 2025.
[7] https://gitlab.inria.fr/SUSHI-public/FMH/herve
[8] Job Noorman et al. Sancus 2.0: A low-cost security architecture for IoT devices. TOPS 2017.
[9] Fritz Alder, Jo Van Bulck, Frank Piessens, Jan Tobias Mühlberg. Aion: Enabling Open Systems through Strong Availability Guarantees for Enclaves. CCS 2021.
[10] Stella Lau, Thomas Bourgeat, Clément Pit-Claudel, Adam Chlipala. Specification and Verification of Strong Timing Isolation of Hardware Enclaves. CCS 2024.
[11] Andreas Lööw. Lutsig: a verified Verilog compiler for verified circuit development. CPP 2021.
[12] Dayeol Lee and David Kohlbrenner and Shweta Shinde and Krste Asanovic and Dawn Song. Keystone: An Open Framework for Architecting Trusted Execution Environments. EuroSys 2020.
[13] Victor Costan, Ilia A. Lebedev, Srinivas Devadas. Sanctum: Minimal Hardware Extensions for Strong Software Isolation. USENIX Security 2016.
[14] Anna Lena Duque Antón, Johannes Müller, Philipp Schmitz, Tobias Jauch, Alex Wezel, Lucas Deutschmann, Mohammad Rahmani Fadiheh, Dominik Stoffel, Wolfgang Kunz. VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL. ICCAD 2024.
[15] Vadim Zaliva, Kayvan Memarian, Ricardo Almeida, Jessica Clarke, Brooks Davis, Alexander Richardson, David Chisnall, Brian Campbell, Ian Stark, Robert N. M. Watson, Peter Sewell. Formal Mechanised Semantics of CHERI C: Capabilities, Undefined Behaviour, and Provenance. ASPLOS 2024.
[16] Kyndylan Nienhuis, Alexandre Joannou, Thomas Bauereiss, Anthony C. J. Fox, Michael Roe, Brian Campbell, Matthew Naylor, Robert M. Norton, Simon W. Moore, Peter G. Neumann, Ian Stark, Robert N. M. Watson, Peter Sewell. Rigorous engineering for hardware security: Formal modelling and proof in the CHERI design and implementation process. SP 2020.
[17] Jean-Loup Hatchikian-Houdot, Pierre Wilke, Frédéric Besson, Guillaume Hiet. Formal Hardware/Software Models for Cache Locking Enabling Fast and Secure Code. ESORICS (3) 2024.