Ce stage a déjà Ã©té attribué.

Sujet proposé et encadré par Emmanuelle Encrenaz et Karine Heydemann
Unité de recherche UMR 7606 Laboratoire d'informatique de Paris 6

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, notamment des attaques en faute qui ont pour but de modifier le comportement du système afin d’inférer des informations sur les données sensibles. De nombreuses attaques en faute ont pu être réalisées, et ce par différents moyens. Cela peut être par modification du signal d’horloge [1] ou de la tension du système, par injection d’impulsion laser ou électro-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. C’est pourquoi la sécurisation des systèmes est une problématique importante.

En pratique, la vulnérabilité des systèmes est analysée expérimentalement, ou à partir de modèles exécutables. L’analyse consiste à introduire des fautes et à estimer, pour chaque faute introduite, les effets de cette faute sur le comportement macroscopique du système. 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, …. 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 fautes. Par exemple, au niveau circuit [4], [5], [6] et [7] ont proposé des méthodes complémentaires basées sur le model-checking [8] pour caractériser les comportements d’un système fauté. Au niveau programme, des fautes de type « saut d’instruction Â» et « corruption de données Â» ont pu être analysées [9]. Au niveau protocole cryptographique, la plate-forme ORCHID [10] et l’outil TOOKAN [11] permettent d’identifier des failles pour des attaques logiques (différentes des attaques en faute). Dans nos récents travaux nous avons utilisé des techniques de model-checking à base de BDD pour prouver la validité et la correction de contremesures logicielles, que nous avons mis au point pour un modèle d‘attaque de type saut d’une instruction assembleur.

Sujet de stage

Nos premiers travaux ont permis la mise au point de contremesures vérifiées formellement. La modélisation actuelle et le schéma de vérification repose sur la technique de model-checking à base de BDD. Cette approche est bien adaptée au niveau de modélisation choisi et aux propriétés à vérifier, mais se heurte rapidement au problème de l’explosion combinatoire de l’espace d’états du système à analyser. Notre solution actuelle proposant une séquence de remplacement pour chaque instruction d’un jeu d’instructions, l’utilisation de BDD n’était pas limitative. Toutefois, l’extension de la portée des contremesures à une granularité plus large (bloc d’instructions, boucles) nécessite d’utiliser d’autres techniques de vérification. Une alternative intéressante consiste à transposer le modèle et la vérification en un problème de satisfiabilité (SAT) et à utiliser des outils de résolutions plus puissants.

L’objectif de ce stage est d’étudier la modélisation SAT de nos solutions actuelles de contremesure pour un certain type de faute et éventuellement d’enrichir cette modélisation pour étendre les travaux existants à d’autres types de fautes [12] ou d’autres granularités de contremesure. Les codes visés par cette analyse sont considérés au niveau assembleur, et les techniques d’analyse pourront combiner profitablement l’analyse statique et les méthodes formelles (bounded model-checking). Par ailleurs, coté implémentation, un outil pour aider l’automatisation des preuves (lien avec des SAT-solveurs) sera désigné et développé au cours de ce stage.

Contact

Emmanuelle Encrenaz : Emmanuelle.Encrenaz(at)lip6(.)fr

Karine Heydemann : Karine.Heydemann(at)lip6(.)fr

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] Régis Leveugle, A. Calvez, Paolo Maistri, Pierre Vanhauwaert: Statistical fault injection: Quantified error and confidence. DATE 2009: 502-506

[4] 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.

[5] 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.

[6] 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)

[7] 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)

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

[9] 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.

[10] Outil Orchids, proposé et développé sous la direction de J. Goubault-Larrecq (LSV) : www.lsv.ens-cachan.fr/Software/orchids/ Orchids

[11] 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.

[12] N. Moro, « Stratégies de sécurité évoluées pour composants de sécurité Â», thèse de doctorat en cours de préparation ; école doctorale EDITE.

[13] K. Heydemann, N. Moro, E. Encrenaz, B. Robisson. Formal verification of a software countermeasure against instruction skip attacks. PROOFS 2013.

 

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)

Compilation.