logo EDITE Sujets de doctorat

Analyse de robustesse et sécurisation de code assembleur soumis à des attaques physiques

Sujet proposé par
Directeur de thèse:
Encadré par
Doctorant: Ines BEN EL OUAHMA
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 sécurité des systèmes intégrés est une préoccupation de plus en plus importante. Les systèmes intégrés sur puce se développent pour de très nombreuses applications de la vie courante, et manipulent de plus en plus de données sensibles voire confidentielles. Ces systèmes sont la cible d’attaques, ces attaques sont actives ou passives, ou une combinaison des deux. Les attaques actives, dites 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, …). Les attaques passives, dites aussi par observation ou par canaux cachés, reposent sur l’analyse statistique d’une quantité (puissance, temps) 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. Concernant les attaques en faute, cela peut être par modification du signal d’horloge [1] ou de la tension du système, par injection d’impulsion laser ou electro-magnétique [2]. Certains circuits présentent des mécanismes de protection permettant de résister à certains types d’attaque (power reduction / clock glitch) ; néanmoins ils restent vulnérables aux attaques par impulsion laser ou électro-magnétique. Coté attaque par canaux cachés, les circuits ou implémentations logicielles peuvent intégrer des contremesures basées sur l’équilibrage ou la randomisation [3]. La problématique est de s’assurer que les protections sont efficaces tout en limitant leur impact sur l’ensemble du système (performance, coût, etc.). La sécurisation des systèmes est une problématique actuelle et majeure qui gagne en importance autant dans le monde académique qu’industriel avec l’accroissement des objets connectés et en conséquence de la surface d’attaque.

En pratique, la vulnérabilité des systèmes est analysée expérimentalement, ou à partir de modèles exécutables. L’analyse consiste à simuler les attaques et à estimer leurs effets. Il s’agit ici d’analyser le comportement macroscopique du système soumis à des fautes ou à modéliser ce qu’un attaquant par observation pourrait mesurer. Cette approche nécessite la mise en œuvre 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 à masquer… Cette approche reste largement empirique, même si des approches statistiques permettent d’estimer la marge de confiance des résultats partiels obtenus par simulation [3].

Par ailleurs, les exigences de certification augmentent, ce qui induit une demande croissante d’utilisation de méthodes formelles pour donner des garanties 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 model-checking [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 model-checking 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 plate-forme 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ériel/logiciel ou des méthodes et outils pour estimer la vulnérabilité d’algorithmes ou implémentations cryptographiques [15, 16, 17]. La combinaison de protections pour se prémunir des deux types d’attaques mais aussi de leur combinaison reste peu étudiée alors que les approches combinées sont considérées comme réalisables et s’avèrent puissantes.

Enjeux

Sujet de thèse

L’objectif de cette thèse est de développer des méthodes et outils pour l’analyse de la robustesse et la sécurisation d’un code soumis à des attaques en faute et par observation, comportant potentiellement des combinaisons de protections logicielles. Le code analysé sera décrit au niveau assembleur, car plus proche de celui qui s’exécute, et les techniques d’analyse et de sécurisation visées combineront judicieusement l’analyse statique et l’optimisation de code telle que mise en œuvre dans les compilateurs ainsi que les méthodes formelles (model-checking).

Cette problématique nécessite le développement de représentations adéquates du programme en cours d’exécution, des éléments caractérisant les fautes et les fuites, et des propriétés de sécurité, exprimées à partir des éléments précédents. Il faudra identifier différents types de propriétés analysables, caractérisant la robustesse du code et proposer une modélisation du programme, des fautes injectées et des quantités mesurées/mesurables ainsi que des critères de robustesse adéquate pour être analysée par model-checking. L’analyse de robustesse aura pour but d’identifier les zones sensibles du programme, qui pourront être alors renforcées par introduction de contre-mesures adaptées. On cherchera également à prouver la validité des contre-mesures et leur combinaison. La vérification de ces propriétés pourra être mise en œuvre en utilisant un solveur SAT-Modulo-Theory, par exemple CVC4 [19] ou Z3 [20]. Dans un premier temps, on se concentrera sur la combinaison des théories des vecteurs booléens et des entiers naturels (arithmétique de Presburger), permettant de représenter l’évolution des variables du programme au niveau binaire ou entier.

Une démarche itérative entre les étapes de modélisation du système – modélisation des propriétés de sécurité – vérification sera adoptée. Une attention particulière sera portée sur l’efficacité de la vérification des propriétés de sécurité, qui relève d’un équilibre entre précision de la modélisation, acuité de la propriété à vérifier, et possibilité de découpage du problème global en une collection de sous-problèmes plus simples ; ce dernier point influe évidemment sur la granularité de la modélisation (insertion des protections au niveau des instructions, ou des blocs de base, ou des fonctions du programme) ; de plus, un découpage de l’analyse d’un code en analyses par morceaux de code est nécessaire pour être capable d’analyser un code entier et contourner les limitations des méthodes de vérification formelle visées. Des informations issues de passes de compilation ou d’analyses de code telles que mises en œuvre dans les compilateurs pourront être utilisées à profit pour cibler l’analyse de robustesse et permettre une combinaison d’analyses pour contourner les problèmes d’explosion combinatoire.

La méthode proposée sera implantée dans un outil de vérification automatique, en extension de l’outil Robusta issu de nos travaux récents sur l’analyse de robustesse de code assembleur soumis à des fautes transitoires [21]. La méthode sera appliquée sur plusieurs contre-mesures existantes (certaines basées sur des fautes et d’autres sur des observations) combinées ; on cherchera tout particulièrement à identifier les interférences néfastes de ces combinaisons.

Par la suite, d’autres théories pourront être étudiées (notamment les fragments décidables de théories manipulant les réels), afin d’analyser des modèles de fuites probabilisés et d’établir, puis de vérifier, des propriétés sécuritaires pour ces modèles.

Ouverture à l'international

Collaboration en cours avec l'Université de Gand (Belgique)

Bibliographie

[1] Josep Balasch, Benedikt Gierlichs, and Ingrid Verbauwhede, An In-depth and Black-box Characterization of the Effects of Clock Glitches on 8-bit MCUs, FDTC 2011: 105-114.

[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: 502-506

[5] R. Leveugle. A new approach for early dependability evaluation based on formal property checking and controlled mutation. In Proc. IEEE International On-Line Testing Symposium, pages 260–265. IEEE Computer Society, 2005.

[6] S. Seshia, W. Li, and S. Mitra. Verification-guided 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): 1239-1252 (2011)

[8] Souheib Baarir, Cécile Braunstein, Emmanuelle Encrenaz, Jean-Michel Ilié, Isabelle Mounier, Denis Poitrenaud, Sana Younès: Feasibility analysis for robustness quantification by symbolic model checking. Formal Methods in System Design 39(2): 165-184 (2011)

[9] Vérification de logiciels : Méthodes et Outils du Model-Checking, P. Schnoebelen et al. Vuibert, 1999.

[10] Pascal Berthomé, Karine Heydemann, Xavier Kauffmann-Tourkestansky, Jean-François Lalande : High Level Model of Control Flow Attacks for Smart Card Functional Security. ARES 2012: 224-229.

[11] A.G. Bayrak, F. Regazzoni, D. Novo, P. Ienne:
Sleuth: Automated Verification of Software Power Analysis Countermeasures. CHES 2013: 293-310

[12] H. Eldib, C. Wang, and P. Schaumont: SMT-based verification of software countermeasures against side-channel attacks,. International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pp. 62-77. 2014.

[13] Outil Orchids, proposé et développé sous la direction de J. Goubault-Larrecq (LSV) : http://www.lsv.ens-cachan.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 260-269. 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 Co-verification 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] http://cvc4.cs.nyu.edu

[20] http://research.microsoft.com/en-us/um/redmond/projects/z3/

[21] L. Goubet, K. Heydemann, E. Encrenaz. R. De Keulaner. Efficient Design and Evaluation of Countermeasures against Fault Attacks Using Formal Verification. CARDIS 2015: 177-192 Remarques additionnelles

Remarques additionnelles

Connaissances souhaitées :

Modélisation et vérification de systèmes numériques concurrents.

- Automates/Réseaux de Petri. - Analyse par exploration de l’espace d’états (model-checking), preuves de programmes (logique de Hoare, analyse statique)

Connaissances en compilation et analyse statique/représentation d’un programme

Notions en architecture des ordinateurs et programmation assembleur.

Connaissances en cryptographie et/ou en sécurité contre les attaques physiques éventuellement