Date de démarrage envisagée : février 2027
Localisation du poste : Palaiseau (91)
Gratification : 1200 € net mensuel
Référence de l’offre à mentionner dans l’objet dans votre e-mail de candidature : STAGE-2027-11-Explo
Au sein de l’Institut de Recherche Technologique SystemX, situé au cœur du campus scientifique d’excellence mondiale de Paris-Saclay, vous prendrez une part active au développement d’un centre de recherche technologique de niveau international dans le domaine de l’ingénierie numérique des systèmes. Adossé aux meilleurs organismes de recherche français du domaine et constitué par des équipes mixtes d’industriels et d’académiques, ce centre a pour mission de générer de nouvelles connaissances et solutions technologiques en s’appuyant sur les percées de l’ingénierie numérique et de diffuser ses compétences dans tous les secteurs économiques. Vous serez encadré par un ingénieur-chercheur SystemX du domaine de sécurité numérique et cryptographie. Vous travaillerez au sein du projet exploratoire « EFFECT-PQ: Effective Security Assurance for Hybrid Post-Quantum Systems » .
Le poste est basé à l’IRT SystemX – Palaiseau
La transition vers la cryptographie post-quantique entre aujourd’hui dans une phase de déploiement concret. Les mécanismes classiques et post-quantiques sont progressivement combinés au sein de protocoles existants afin de maintenir la sécurité pendant cette transition. Dans TLS 1.3, des mécanismes d’échange de clés hybrides permettent ainsi de combiner plusieurs mécanismes cryptographiques avec l’objectif de conserver la confidentialité tant qu’au moins l’un d’entre eux reste sûr [1]. En parallèle, les travaux de standardisation sur les signatures hybrides montrent que leur sécurité dépend de propriétés de composition plus fines, telles que la composabilité des preuves ou la non-séparabilité des signatures [2]. Cependant, la présence de mécanismes post-quantiques dans un protocole ne suffit pas à établir la sécurité post-quantique du système dans son ensemble. Un déploiement peut, par exemple, utiliser un échange de clés hybride tout en conservant une authentification classique. Des travaux récents montrent également que des informations post-quantiques peuvent être présentes dans un certificat X.509 sans nécessairement participer à la décision finale du vérificateur [5]. D’un autre côté, la sécurité de TLS 1.3 a fait l’objet d’analyses cryptographiques approfondies permettant d’associer différentes propriétés de sécurité aux clés produites au cours du protocole [3]. Des travaux plus récents montrent également qu’il est possible de vérifier formellement des implémentations post-quantiques de TLS 1.3 [4], tandis que des validateurs X.509 peuvent désormais bénéficier de garanties formelles sur leur comportement [6]. Il reste néanmoins une question ouverte entre ces différents niveaux d’analyse :
Comment déterminer les garanties de sécurité effectivement fournies par un système hybride déployé à partir des garanties de ses composants, de leur composition et des évidences observables sur le système réel ?
Le stage vise à explorer cette question sur un périmètre volontairement limité à TLS 1.3 et X.509, afin de construire une approche à la fois formelle, exécutable et expérimentalement vérifiable.
Objectifs du stage
L’objectif principal du stage est de proposer un cadre d’assurance de sécurité effective pour les protocoles hybrides classiques/post-quantiques. Une première partie du travail consistera à modéliser les garanties apportées par les différents composants d’un déploiement TLS 1.3/X.509 et à étudier comment ces garanties peuvent être composées. L’objectif n’est pas de produire une qualification globale « sécurisé / non sécurisé », mais de raisonner séparément sur les propriétés importantes du système, en particulier la confidentialité et l’authentification. La résistance au downgrade pourra être étudiée comme extension si l’avancement du stage le permet.
Une deuxième question portera sur le lien entre les propriétés formelles et les évidences réellement observables sur un déploiement : paramètres négociés lors du handshake TLS, certificats, configuration ou comportement du vérificateur. Il s’agira notamment d’identifier quelles évidences sont suffisantes pour justifier une garantie et dans quels cas aucune conclusion ne peut être formulée. Enfin, le modèle proposé sera décliné sous la forme d’un prototype de plateforme d’assurance, capable d’analyser un déploiement TLS/X.509 et de produire des garanties de sécurité explicites et justifiées par les évidences collectées.
Missions :
Références bibliographiques
[1] D. Stebila, S. Fluhrer, S. Gueron, Hybrid Key Exchange in TLS 1.3, RFC 9954, IETF, July 2026.
[2] N. Bindel, B. Hale, D. Connolly, F. Driscoll, Hybrid Signature Spectrums, RFC 9955, IETF, July 2026.
[3] B. Dowling, M. Fischlin, F. Günther, D. Stebila, A Cryptographic Analysis of the TLS 1.3 Handshake Protocol, Journal of Cryptology, vol. 34, article 37, 2021, DOI: 10.1007/s00145-021-09384-1.
[4] K. Bhargavan, L. L. Hansen, F. Kiefer, J. Schneider-Bensch, B. Spitters, Formal Security and Functional Verification of Cryptographic Protocol Implementations in Rust, Proceedings of ACM CCS 2025, pp. 2729–2743, DOI: 10.1145/3719027.3765213.
[5] T. Kim, B. Chung, K. Kim, Y. Kang, Classical Acceptance Is Not Hybrid Authentication: Measuring X.509 Verifier Semantics in Post-Quantum Migration, arXiv:2607.20800, 2026.
[6] Z. Lin, M. McLoughlin, P. Singh, R. Brennan-Jones, P. Hitchcox, J. Gancher, B. Parno, Towards Practical, End-to-End Formally Verified X.509 Certificate Validators with Verdict, 34th USENIX Security Symposium, 2025, pp. 5035–5052.
De formation : BAC +5 / école d’ingénieur ou université, Master 2 en informatique, cybersécurité, cryptographie ou sécurité des systèmes et réseaux.
Compétences souhaitées
Aptitudes personnelles
Merci de joindre CV, lettre de motivation, relevé de notes et autres documents utiles comme une lettre de recommandations
Offre d'emploi
Rejoignez l’IRT SystemX afin d’imaginer et concevoir un monde numérique plus sûr, plus performant et plus durable.
Offre d'emploi
Vous travaillerez au sein du programme CYBELIA
Offre d'emploi
Vous travaillez dans le projet XHUB