Direction de recherche : Damien VERGNAUD

Co-encadrement : Sonia BELAÏD et Matthieu RIVAIN

Implémentations cryptographiques sûres et vérifiées dans le modèle «Random Probing»

La contre-mesure de masquage fait partie des contre-mesures les plus puissantes contre les attaques par canaux auxiliaires. Des modèles de fuite ont été introduits pour raisonner théoriquement sur la sécurité de telles implémentations masquées. Jusqu'à présent, le modèle de fuite le plus largement utilisé est le modèle nommé “probing”, mais il a été récemment remis en question car il ne rend pas pleinement compte des capacités d’un adversaire par canaux auxiliaires. Ainsi, un autre modèle a été introduit, appelé “random probing”. Dans ce modèle, à partir d'un paramètre de fuite p, chaque fil du circuit fuit sa valeur avec probabilité p. Le modèle random probing est pratique grâce à sa réduction au modèle “noisy leakage”, qui est admis comme la formalisation appropriée pour la fuite pendant les attaques par canaux auxiliaires. De plus, le modèle random probing est bien plus pratique que le modèle noisy leakage pour prouver la sécurité des implémentations masquées.
Dans cette thèse, nous étudions de plus près le modèle random probing et définissons le premier cadre qui lui est dédié. Nous formalisons une propriété de composition pour les gadgets sécurisés dans ce modèle et montrons sa relation avec la notion de non-interférence forte (SNI) utilisée dans le modèle de sécurité “probing”. Nous revisitons ensuite l'idée d'expansion proposée par Ananth, Ishai et Sahai (CRYPTO 2018) et introduisons un compilateur qui construit un circuit sécurisé dans le modèle random probing à partir de petits gadgets de base. Nous proposons ensuite une analyse approfondie, permettant d'obtenir des instanciations beaucoup plus efficaces de la technique d'expansion, avec des constructions tolérant une probabilité de fuite allant jusqu'à 2^-7, contre 2^-26 pour les constructions précédentes et une complexité améliorée de O kappa^3.2 contre O kappa^7.87 pour les constructions précédentes, où kappa est le paramètre de sécurité. Nous montrons également que nos constructions atteignent une complexité quadratique en kappa asymptotiquement en augmentant le nombre de partages pendant le masquage. D'autres tentatives d'optimisation des constructions incluent la généralisation de l'approche en considérant un choix dynamique des gadgets de base à chaque étape de l'expansion. Nous montrons que de telles techniques peuvent réduire davantage la complexité du quadratique au quasi-linéaire tout en tolérant de bons taux de fuite.
Enfin, nous présentons IronMask, un nouvel outil de vérification polyvalent pour la sécurité des circuits masqués. IronMask est le premier à vérifier les notions de sécurité standard basées sur la simulation dans le modèle probing et les notions récentes du modèle random probing. Il prend en charge tous les gadgets masqués qui utilisent des variables aléatoires de façon linéaire (par exemple, les gadgets d'addition et de copie) ainsi que les gadgets quadratiques (par exemple, les gadgets de multiplication) qui peuvent inclure des variables aléatoires non linéaires, tout en fournissant des résultats de vérification complets. pour les deux types de gadgets.
Nous concluons cette thèse en discutant des projets de recherche en cours dans le modèle random probing et en suggérant des travaux futurs.

Publications 2020-2023

• 2023
  • A. Taleb : “Secure and Verified Cryptographic Implementations in the Random Probing Model”, thèse, soutenance 07/11/2023, direction de recherche Vergnaud, Damien, co-encadrement : Sonia, BELAÏD et Matthieu RIVAIN (2023)
  • Q. Meunier, A. Taleb : “VerifMSI: Practical Verification of Hardware and Software Masking Schemes Implementations”, Proceedings of the 20^th International Conference on Security and Cryptography SECRYPT, vol. 1, Rome, Italy, pp. 520-527, (SciTePress), (ISBN: 978-989-758-666-8) (2023)
• 2022
  • S. Belaid, D. Mercadier, M. Rivain, A. Taleb : “IronMask: Versatile Verification of Masking Security”, 2022 IEEE Symposium on Security and Privacy (SP), San Francisco, United States, pp. 142-160, (IEEE) (2022)
• 2021
  • S. Belaid, M. Rivain, A. Taleb, D. Vergnaud : “Dynamic Random Probing Expansion with Quasi Linear Asymptotic Complexity”, Advances in Cryptology – Asiacrypt 2021, vol. 13091, Lecture Notes in Computer Science, Singapour, Singapore, pp. 157-188, (Springer) (2021)
  • S. Belaid, M. Rivain, A. Taleb : “On the Power of Expansion: More Efficient Constructions in the Random Probing Model”, Advances in Cryptology - EUROCRYPT 2021 - 40^th Annual International Conference on the Theory and Applications of Cryptographic Techniques, vol. 12697, Lecture Notes in Computer Science, Zagreb, Croatia, pp. 313-343, (Springer International Publishing) (2021)
  • A. Taleb, D. Vergnaud : “Speeding-Up Verification of Digital Signatures”, Journal of Computer and System Sciences, vol. 116, pp. 22-39, (Elsevier) (2021)
• 2020
  • S. Belaid, J.‑S. Coron, E. Prouff, M. Rivain, A. Taleb : “Random Probing Security: Verification, Composition, Expansion and New Constructions”, Advances in Cryptology - CRYPTO}2020 - 40^th Annual International Cryptology Conference, {CRYPTO} 2020, Santa Barbara, CA, USA, August 17-21, 2020, Proceedings, Part I, vol. 12170, Lecture Notes in Computer Science, Santa Barbara, CA / Virtual, United States, pp. 339-368, (Springer) (2020)