logo EDITE Sujets de doctorat

Quantification de la sécurité des applications en présence d'attaques physiques et détection de chemins d'attaques

Sujet proposé par
Directeur de thèse:
Encadré par
Doctorant: Jean-Baptiste BREJON
Unité de recherche UMR 7606 Laboratoire d'informatique de Paris 6

Domaine: Sciences et technologies de l'information et de la communication

Projet

Contexte La multiplication des systèmes embarqués contenant des informations sensibles (données personnelles, confidentielles, etc.) et l’accroissement de l’interconnexion de ces objets (IoT) a pour conséquence d’augmenter la surface d’attaque de ces systèmes. En particulier, ces systèmes peuvent être la cible d’attaques physiques qui sont extrêmement puissantes. Parmi cellesci, les attaques dites actives ou en faute, ont pour but de modifier le comportement du système afin d’inférer des informations sur des données sensibles (clé cryptographique, éléments personnels et confidentiels, …). Une faute peut être injectée par modification du signal d’horloge [1] ou de la tension du système, par impulsion laser ou électromagnétique [2]. Les attaques passives, dites aussi par observation ou par canaux cachés, reposent sur l’analyse statistique d’une quantité (puissance, temps, émanation électromagnétique) mesurée lors de l’exécution du programme pour en déduire des informations. De nombreuses attaques ont pu être réalisées, et ce par différents moyens, parfois en combinant les approches passives et actives. De nombreuses protections ont été proposées aussi bien au niveau logiciel que matériel [3, 12, 18]. Ces protections permettent typiquement de se prémunir d’un type d’attaque voire uniquement d’une catégorie d’attaque dans un des deux types d’attaque. Par exemple, certains circuits présentent des mécanismes de protection permettant de résister à certains types d’attaque (power reduction / clock glitch) mais ils restent néanmoins vulnérables aux attaques par impulsion laser ou électromagnétique. Concernant les attaques par canaux cachés, les circuits ou implémentations logicielles peuvent intégrer des contremesures basées sur de l’équilibrage ou utilisant des techniques de randomisation [3] visant un type d’observation mais pas un autre. En pratique, les acteurs industriels tentent de s’en prémunir en multipliant les protections. Un point très difficile est d’assurer un niveau de protection donné en considérant la multiplicité des attaques possibles tout en limitant l’impact des protections sur l’ensemble du système (performance, surface, consommation, temps de mise sur le marché, etc.). Cela rend la sécurité des systèmes intégrés cibles de ces attaques une des préoccupations majeures des acteurs industriels. La problématique sousjacente est d’être capable d’analyser la vulnérabilité des systèmes soumis à des attaques physiques. Actuellement, ces systèmes sont analysés expérimentalement en les soumettant à des attaques physiques réelles ou en simulant cellesci afin de pouvoir analyser le comportement macroscopique du système soumis à l’attaque. Cette approche nécessite le plus souvent la mise en oeuvre de très lourdes campagnes d’expérimentation (sur banc physique ou par prototypage virtuel). Elle permet toutefois de déduire les zones sensibles du système (registres ou portion de code à protéger en priorité), les chemins de propagation des fautes, les variables à protéger… Cette approche reste largement empirique et ne permet pas de d’estimer la couverture des effets possibles des attaques. Les approches par simulation limitent le nombre d’attaques en faute considérées, mais des techniques statistiques permettent d’estimer la marge de confiance de résultats partiels obtenus [4]. Par ailleurs, les exigences de certification augmentent pour offrir demain des systèmes sécurisés là où ils ne le sont pas aujourd’hui mais aussi pour que les systèmes sécurisés d’aujourd’hui soient toujours concurrentiels demain. Cela explique la demande croissante d’utilisation de méthodes formelles permettant de donner des garanties plus fortes sur la sécurité des systèmes développés. Les approches formelles peuvent être utilisées à différents niveaux pour évaluer la robustesse d’un système soumis à des attaques. Par exemple, au niveau circuit [5], [6], [7] et [8] ont proposé des méthodes complémentaires basées sur le modelchecking [9] pour caractériser les comportements d’un système fauté. Au niveau programme source ou assembleur, des fautes de type « saut d’instruction » et « corruption de données » ont pu être analysées [10, 18, 21]. Les techniques de modelchecking ont également été utilisées pour évaluer la robustesse d’un programme source visàvis d’attaques par observation [11], [12]. Au niveau protocole cryptographique, la plateforme ORCHID [13] et l’outil TOOKAN [14] permettent d’identifier des failles pour des attaques logiques (différentes des attaques en faute). D’autres approches formelles ont proposé des analyses conjointes matérielle/logicielle ou des méthodes et outils pour estimer la vulnérabilité d’algorithmes ou implémentations cryptographiques [15, 16, 17].

Enjeux

Sujet de thèse L’objectif de cette thèse est de concevoir une méthode et sa mise en oeuvre dans un outil pour l’analyse de la robustesse de code, comportant potentiellement des protections logicielles, vis à vis des attaques en faute. L’analyse a pour but d’aider les concepteurs en détectant, en quantifiant et caractérisant les vulnérabilités éventuelles d’une application ; elle vise à offrir des garanties de robustesse le cas échéant. Par exemple, savoir que tout remplacement d’une instruction précise par une autre modifiant un registre bien identifié par une valeur non nulle résulte en une attaque qui réussit est bien plus précieux que de savoir qu’il existe un remplacement par une valeur non nulle qui permet une attaque. Des codes de niveau assembleur seront considérés car ils reflètent ceux qui s’exécutent, et les modèles des effets des attaques sont plus fidèles à ce niveau tout en restant exploitables. Par ailleurs, l’ensemble des informations requises à ce niveau de code pour permettre l’analyse de robustesse seront d’abord déterminées puis considérées données en entrée de l’analyse. Les méthodes proposées seront implantées dans un outil capable d’effectuer de la vérification automatique reposant sur un solveur SMT (par exemple CVC4 [21] ou Z3 [22]) compatible avec le standard SMTlib [23]. L’outil Robusta issu de nos travaux récents sur l’analyse de robustesse de code assembleur soumis à des fautes transitoires [19] constituera un point de départ. La problématique adressée dans cette thèse nécessite le développement de représentations adéquates des éléments caractérisant les fautes possibles, l’objectif étant d’étendre les fautes adressées dans nos travaux précédents (saut d’instruction et quelques remplacement d’instructions). Elle nécessite aussi d’étendre l’analyse de robustesse issue de ces travaux, pour analyser et quantifier la robustesse visàvis d’un grand nombre de fautes possibles (modification du contenu de registres du processeur, de données, saut aléatoire dans le code, ...). Cela nécessite notamment de pouvoir déterminer dans quelle(s) configuration(s) de l’exécution une faute rend le code vulnérable et de quantifier le nombre de ces configurations tout en les confrontant à la probabilité d’injection d’une telle faute [20]. Ce travail s’effectuera dans le cadre du projet ANR PROSECCO et en collaboration avec le partenaire du projet, notamment concernant les informations disponibles sur les applications afin de pouvoir analyser leur niveau de sécurité au niveau assembleur. La thèse s’effectuera aussi en étroite collaboration avec une autre thèse en cours au LIP6 s’attaquant au problème du découpage de l’analyse en sousanalyse pour contourner les limitations de la vérification (explosion combinatoire ou de la mémoire requise) et à l’analyse de robustesse visàvis des attaques par observation ou combinées. L’analyse de robustesse développée sera appliquée notamment à des applications bas niveau telles que des codes systèmes, des codes de périphérique, éventuellement des codes cryptographiques. Dans une seconde partie de la thèse, la recherche d’attaques expliquant un résultat d’expérimentation réelle pourra être abordée. La recherche de chemins d’attaque pour invalider une propriété de sécurité donnée (par exemple : ne pas pouvoir élever le niveau de privilèges) en combinant judicieusement différent types de fautes ou types d’attaques pourra aussi être étudiée. A titre d’illustration, l’outil Lazart étudie les chemins d’attaque pour l’inversion de branchement [25]. Ce travail pourra surement utiliser à profit des analyses statiques, ou de l’exécution symbolique [24] ou concolique [26] pour déterminer une méthode de recherche de chemins d’attaque sur un cas précis issu d’une analyse préalable d’un code système.

Ouverture à l'international

Collaborations possibles avec l'Université de Gand.

Remarques additionnelles

Encadrants: Emmanuelle Encrenaz emmanuelle.encrenaz@lip6.fr Karine Heydemann karine.heydemann@lip6.fr Bibliographie [1] Josep Balasch, Benedikt Gierlichs, and Ingrid Verbauwhede, An Indepth and Blackbox Characterization of the Effects of Clock Glitches on 8bit MCUs, FDTC 2011: 105114. [2] Electromagnetic Glitch on the AES Round Counter, N. Moro et al. workshop COSADE 2013. [3] S. Renner. « Protection des algorithmes cryptographiques embarqués », thèse de doctorat. Juin 2014, université de Bordeaux, école doctorale de mathématiques et informatique de Bordeaux. [4] Régis Leveugle, A. Calvez, Paolo Maistri, Pierre Vanhauwaert: Statistical fault injection: Quantified error and confidence. DATE 2009: 502506 [5] R. Leveugle. A new approach for early dependability evaluation based on formal property checking and controlled mutation. In Proc. IEEE International OnLine Testing Symposium, pages 260–265. IEEE Computer Society, 2005. [6] S. Seshia, W. Li, and S. Mitra. Verificationguided soft error resilience. In Proc. Conference on Design, Automation and Test in Europe, pages 1442–1447. EDA Consortium, 2007. [7] Görschwin Fey, André Sülflow, Stefan Frehse, Rolf Drechsler: Effective Robustness Analysis Using Bounded Model Checking Techniques. IEEE Trans. on CAD of Integrated Circuits and Systems 30(8): 12391252 (2011) [8] Souheib Baarir, Cécile Braunstein, Emmanuelle Encrenaz, JeanMichel Ilié, Isabelle Mounier, Denis Poitrenaud, Sana Younès: Feasibility analysis for robustness quantification by symbolic model checking. Formal Methods in System Design 39(2): 165184 (2011) [9] Vérification de logiciels : Méthodes et Outils du ModelChecking, P. Schnoebelen et al. Vuibert, 1999. [10] Pascal Berthomé, Karine Heydemann, Xavier KauffmannTourkestansky, JeanFrançois Lalande : High Level Model of Control Flow Attacks for Smart Card Functional Security. ARES 2012: 224229. [11] A.G. Bayrak, F. Regazzoni, D. Novo, P. Ienne: Sleuth: Automated Verification of Software Power Analysis Countermeasures. CHES 2013: 293310 [12] H. Eldib, C. Wang, and P. Schaumont: SMTbased verification of software countermeasures against sidechannel attacks,. International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 6277. 2014. [13] Outil Orchids, proposé et développé sous la direction de J. GoubaultLarrecq (LSV) : http://www.lsv.enscachan. fr/Software/orchids/ Orchids [14] M. Bortolozzo, M. Centenaro, R Focardi and G. Steel. Attacking and Fixing PKCS#11 Security Tokens. In CCS’10, pages 260269. ACM Press, 2010. [15] P. Rauzy. « Formal Software Methods for Cryptosystems Implementation Security », thèse de doctorat, juillet 2015, école doctorale EDITE. [16] EasyCrypt. http://www.easycrypt.info [17] L. Erkok, M. Carlsson, A. Wick, Hardware/Software Coverification of Cryptographic Algorithms using Cryptol, FMCAD 2009, outil cryptol développé par Galois.inc [18] N. Moro, « Stratégies de sécurité évoluées pour composants de sécurité », thèse de doctorat, novembre 2014, Université Pierre et Marie Curie, école doctorale EDITE. [19] L. Goubet, K. Heydemann, E. Encrenaz. R. De Keulaner. Efficient Design and Evaluation of Countermeasures against Fault Attacks Using Formal Verification. CARDIS 2015: 177192 [20] Louis Dureuil, MarieLaure Potet, Philippe de Choudens, Cécile Dumas, Jessy Clédière: From Code Review to Fault Injection Attacks: Filling the Gap Using Fault Model Inference. CARDIS 2015: 107124 [21] http://cvc4.cs.nyu.edu [22] http://research.microsoft.com/enus/ um/redmond/projects/z3/ [23] http://smtlib.cs.uiowa.edu [24] Vitaly Chipounov, Volodymyr Kuznetsov, George Candea. The S2E Platform: Design, Implementation, and Applications. ACM Trans. Comput. Syst. 30(1): 2 (2012) [25] MarieLaure Potet, Laurent Mounier, Maxime Puys, Louis Dureuil. Lazart: A Symbolic Approach for Evaluation the Robustness of Secured Codes against Control Flow Injections. ICST 2014: 213222 [26] Cristian Cadar, Koushik Sen. Symbolic execution for software testing: three decades later. Commun. ACM 56(2): 8290 (2013