Contexte et objectifs

Ces dernières années, une multitude d'objets électroniques miniatures ont envahi notre quotidien. Téléphones mobiles, étiquettes RFID ou encore bracelets connectés, ces dispositifs ont pour objectif d'améliorer notre confort. Pour mener à bien leur tâche, ces objets sont susceptibles de stocker ou d'échanger des données personnelles, des données sensibles, convoitées pour leur haute valeur marchande. Leur nature embarquée et miniature les rend manipulables par des utilisateurs malveillants qui cherchent à extraire des informations. Pour atteindre leur objectifs, ces attaquants peuvent réaliser des observations physiques (consommation, temps d'exécution, rayonnement électromagnétique) leur permettant d'obtenir des informations sur l'exécution du programme, sur les données manipulées et d'en déduire des informations sur les données secrètes.

Les solutions proposées pour se prémunir de ces attaques consiste à ajouter de l’aléa dans le code ou les données afin de décorreler les informations observées lors de l'exécution du programme et les données secrètes manipulées [Bayrak 2015].

Les modèles de fuites permettent de représenter la quantité d'information mesurable par un attaquant et peut être utilisés ensuite pour déterminer si une implémentation est robuste à ce type d'attaque.

L'objectif de ce stage est d'étudier et de mettre en place une solution d'analyse de la robustesse d'un code assembleur vis à vis des attaques par observation. L'analyse aura recours à des méthodes formelles de type SAT/SMT solver pour s'intégrer dans la plateforme existante RobustA [Goubet 2015].

La modélisation formelle s'inspirera des travaux récents sur la synthèse de code parfaitement masqué [Bayrak 2013, Eldib 2014a, Eldib 2014b] utilisant un modèle de robustesse au niveau code source. Il s'agira de le transposer au niveau assembleur et de l'étendre pour couvrir des codes plus divers (opérations non linéaires) et d'autres modèles de fuite.

Déroulement du stage envisagé 

1. Etude bibliographique sur les attaques, les modèles de fuite et les outils d'analyse de robustesse

2. Proposition de modélisation

3. Implémentation de la solution et intégration dans l'outil RobustA.

4. Evaluation sur des exemples simples et connus issus de la littérature

Encadrement

Karine Heydemann et Emmanuelle Encrenaz

Lieu

Laboratoire Informatique de Paris 6

Contact 

karine.heydemann(at)lip6(.)fr, emmanuelle.encrenaz@lip6.fr

Remunération

indemnités de stage fixées par décret (environ 600 euros/mois)

 

Bibliographie

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

[Eldib14b] H. Eldib and C. Wang. Synthesis of Masking Countermeasures against Side Channel Attacks. International Conference on Computer Aided Verification (CAV), pp. 114-130. 2014.

[Goutbet 2015] L. Goubet, K. Heydemann, E. Encrenaz, R. De Keulenaer : “Efficient Design and Evaluation of Countermeasures against Fault Attack with Formal Verification”, 14^th Smart Card Research and Advanced Application Conference, CARDIS 2015, Bochum, Germany (2015)

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

[Bayrak15] A.G. Bayrak, F. Regazzoni,  D. Novo,  P. Brisk,  F-X. Standaert and P. Ienne, Automatic Application of Power Analysis Countermeasures. Computers, IEEE Transactions on, vol.64, no.2, pp.329,341, Feb. 2015