Thesis : Analyse formelle de fuite et modélisation réaliste des fuites de la micro-architecture
Project PhD thesis
Les attaques par canaux auxiliaires (SCA) consistent à mesurer des grandeurs physiques d'un système informatique (consommation, radiations électro-magnétiques) durant l'exécution d'un algorithme cryptographique, et de les utiliser afin de retrouver la clé de chiffrement [1, 2]. Ces attaques ciblent plus particulièrement les dispositifs embarqués, tels que les cartes de paiement, pour lesquels la clé de chiffrement ne doit pas être connue de l'utilisateur.
Les SCA n'ont cessé de gagner en popularité depuis le début des années 2000. Pour limiter leur impact, deux techniques principales sont apparues : le "hiding" [3] et le masquage [4]. Ce dernier consiste à décomposer le secret en plusieurs parties (shares) à l’aide de masques (variables suivant une distribution aléatoire uniforme entre plusieurs exécutions), dont seule la recomposition permet de déduire de l'information, et d'appliquer un traitement indépendant à chacune des parties.
Différents travaux se sont intéressés à prouver de tels schémas de masquage à l'aide d'outils : il s'agit, à partir d'une description du programme, de vérifier pour toutes les expressions obtenues que leurs distributions sont statistiquement indépendantes des secrets (typiquement la clé de chiffrement). Cela se base sur l'hypothèse que la valeur observée de la fuite physique est liée à la valeur de l'expression manipulée à ce moment. Or, il apparait bien souvent que ce niveau de description est insuffisant pour donner des garanties sur l’absence de fuite dans le système réel. D’une part, ces expressions ne sont pas forcément celles manipulées par le programme compilé, et d’autre part la transition en matériel entre deux expressions bien masquées peut révéler des informations secrètes en annulant les masques. Afin de réaliser une analyse de fuites d'un code masqué en vue d'en garantir l'absence, il faut donc disposer du code assembleur (ou binaire) du programme et d’un modèle suffisamment précis du processeur [5], prenant typiquement en compte la micro-architecture de celui-ci.
Un autre aspect essentiel à cette analyse concerne la méthode d’analyse de l’indépendance d’une expression donnée vis-à-vis des secrets. Plusieurs algorithmes et outils symboliques ont vu le jour récemment [6, 7, 8, 9], mais la question de leur rapidité, scalabilité, et précision pour les vérifications d’expression issues du code binaire n’a pas été bien étudiée.
L’objectif de la thèse est de proposer une méthode générale qui, étant donné une description matérielle d’un processeur et un code masqué, permet la vérification de l’absence de fuites lors de l’exécution. Comprendre les sources les fuites dans les processeurs sera un aspect important afin de proposer un modèle pertinent pour l’analyse, voire une méthode de modélisation. La vérification formelle devra quant à elle être correcte et la plus complète possible, avec un accent mis sur les performances et la taille maximale possible des expressions analysées. Enfin, l’analyse devra être aussi automatisée que possible et pourra se baser sur les travaux récents effectués notamment dans l’équipe. La thèse comportera un volet expérimental afin de valider les différentes propositions (modèle et analyse).
Cette thèse est financée par le projet ANR IDROMEL démarré en 2021. Ce projet a pour objectif d’analyser les sources de fuite dans la micro-architecture et de proposer différentes méthodes et outils pour renforcer la sécurité logicielle et matérielle des systèmes face aux attaques par canal auxiliaire. Le consortium regroupe Arm France, le CEA, l’IRISA, le LAAS et le LIP6. L’objectif général de la thèse est la prise en compte de la micro-architecture du processeur dans l’analyse des fuites au niveau logiciel. Elle poursuit notamment la thèse d’Inès Ben El Ouahma effectuée également dans l’équipe ALSOC. La date de démarrage prévue est le 1er septembre 2021, mais il est envisageable de démarrer la thèse plus tôt si nécessaire.
[1] S. Mangard, E. Oswald, and T. Popp. Power analysis attacks: Revealing the secrets of smart cards,Vol. 31. Springer Science & Business Media, 2008.
[2] Q. L. Meunier. FastCPA: Efficient Correlation Power Analysis Computation with a Large Number of Traces, in CS2'19, 2019, Valencia, Spain
[3] N. Belleville, D. Couroussé, K. Heydemann and H.-P. Charles. Automated software protection for the masses against side-channel attacks, ACM Transactions on Architecture and Code Optimization (TACO) 15.4 (2018): 47.
[4] Y. Ishai, A. Sahai, D. Wagner. Private circuits: Securing hardware against probing attacks, in Annual International Cryptology Conference. Springer, Berlin, Heidelberg, 2003.
[5] D. Zoni, A. Barenghi, G. Pelosi, W. Fornaciari. A Comprehensive Side-Channel Information Leakage Analysis of an In-Order RISC CPU Microarchitecture, ACM Transactions on Design Automation of Electronic Systems (TODAES) 23.5 (2018): 57.
[6] G. Barthe, S. Belaïd, G. Cassiers, P.-A. Fouque, B. Grégoire, F.-X. Standaert. maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults, European Symposium on Research in Computer Security. Springer, Cham, 2019.
[7] Q. L. Meunier, I. Ben El Ouahma, and K. Heydemann. SELA: a Symbolic Expression Leakage Analyzer. International Workshop on Security Proofs for Embedded Systems. 2020.
[8] I. Ben El Ouahma, Q. L. Meunier, K. Heydemann, E. Encrenaz. Side-channel robustness analysis of masked assembly codes using a symbolic approach, Journal of Cryptographic Engineering (JCEN), March 2019
[9] Pengfei, G., Hongyi, X., Sun, P., Zhang, J., Song, F., & Chen, T. (2020). Formal Verification of Masking Countermeasures for Arithmetic Programs. IEEE Transactions on Software Engineering.
L’objectif de la thèse est de proposer une méthode générale qui, étant donné une description matérielle d’un processeur et un code masqué, permet la vérification de l’absence de fuites lors de l’exécution. Comprendre les sources les fuites dans les processeurs sera un aspect important afin de proposer un modèle pertinent pour l’analyse, voire une méthode de modélisation. La vérification formelle devra quant à elle être correcte et la plus complète possible, avec un accent mis sur les performances et la taille maximale possible des expressions analysées. Enfin, l’analyse devra être aussi automatisée que possible et pourra se baser sur les travaux récents effectués notamment dans l’équipe. La thèse comportera un volet expérimental afin de valider les différentes propositions (modèle et analyse).
Cette thèse est financée par le projet ANR IDROMEL démarré en 2021. Ce projet a pour objectif d’analyser les sources de fuite dans la micro-architecture et de proposer différentes méthodes et outils pour renforcer la sécurité logicielle et matérielle des systèmes face aux attaques par canal auxiliaire. Le consortium regroupe Arm France, le CEA, l’IRISA, le LAAS et le LIP6. L’objectif général de la thèse est la prise en compte de la micro-architecture du processeur dans l’analyse des fuites au niveau logiciel. Elle poursuit notamment la thèse d’Inès Ben El Ouahma effectuée également dans l’équipe ALSOC. La date de démarrage prévue est le 1er septembre 2021, mais il est envisageable de démarrer la thèse plus tôt si nécessaire.
[1] S. Mangard, E. Oswald, and T. Popp. Power analysis attacks: Revealing the secrets of smart cards,Vol. 31. Springer Science & Business Media, 2008.
[2] Q. L. Meunier. FastCPA: Efficient Correlation Power Analysis Computation with a Large Number of Traces, in CS2'19, 2019, Valencia, Spain
[3] N. Belleville, D. Couroussé, K. Heydemann and H.-P. Charles. Automated software protection for the masses against side-channel attacks, ACM Transactions on Architecture and Code Optimization (TACO) 15.4 (2018): 47.
[4] Y. Ishai, A. Sahai, D. Wagner. Private circuits: Securing hardware against probing attacks, in Annual International Cryptology Conference. Springer, Berlin, Heidelberg, 2003.
[5] D. Zoni, A. Barenghi, G. Pelosi, W. Fornaciari. A Comprehensive Side-Channel Information Leakage Analysis of an In-Order RISC CPU Microarchitecture, ACM Transactions on Design Automation of Electronic Systems (TODAES) 23.5 (2018): 57.
[6] G. Barthe, S. Belaïd, G. Cassiers, P.-A. Fouque, B. Grégoire, F.-X. Standaert. maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults, European Symposium on Research in Computer Security. Springer, Cham, 2019.
[7] Q. L. Meunier, I. Ben El Ouahma, and K. Heydemann. SELA: a Symbolic Expression Leakage Analyzer. International Workshop on Security Proofs for Embedded Systems. 2020.
[8] I. Ben El Ouahma, Q. L. Meunier, K. Heydemann, E. Encrenaz. Side-channel robustness analysis of masked assembly codes using a symbolic approach, Journal of Cryptographic Engineering (JCEN), March 2019
[9] Pengfei, G., Hongyi, X., Sun, P., Zhang, J., Song, F., & Chen, T. (2020). Formal Verification of Masking Countermeasures for Arithmetic Programs. IEEE Transactions on Software Engineering.
Ce projet de recherche doctorale a été déposé par un porteur disposant d’une source de financement propre. Le candidat doit soumettre un dossier complet auprès du porteur de ce projet qui pourra donner lieu à la remise de livrables intermédiaires en fonction de la source de financement (notamment dans le cas de projets — ANR, Europe, etc.)
Contact :Karine Heydemann