Outils d'aide à la recherche de vulnérabilités dans l'implantation d'applications embarquées sur carte à puce / Philippe Andouard ; sous la direction de Olivier Ly et de Mohamed Mosbah

Date :

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Catalogue Worldcat

Cartes à mémoire

Systèmes embarqués (informatique) -- Fiabilité

Microcontrôleurs

Assembleurs (informatique)

Classification Dewey : 004

Ly, Olivier (1973-....) (Directeur de thèse / thesis advisor)

Mosbah, Mohamed (1964-....) (Directeur de thèse / thesis advisor)

Chaumette, Serge (1966-....) (Président du jury de soutenance / praeses)

Goubin, Louis (1970-....) (Rapporteur de la thèse / thesis reporter)

Belhassen, Zouari (Rapporteur de la thèse / thesis reporter)

Rouillard, Davy (1973-....) (Membre du jury / opponent)

Université Bordeaux-I (1971-2013) (Organisme de soutenance / degree-grantor)

École doctorale de mathématiques et informatique (Talence, Gironde) (Ecole doctorale associée à la thèse / doctoral school)

Laboratoire bordelais de recherche en informatique (Laboratoire associé à la thèse / thesis associated laboratory)

Résumé / Abstract : Les travaux présentés dans cette thèse ont pour objectif de faciliter les évaluations sécuritaires des logiciels embarqués dans les cartes à puce. En premier lieu, nous avons mis au point un environnement logiciel dédié à l'analyse de la résistance d'implémentations d'algorithmes cryptographiques face à des attaques par analyse de la consommation de courant. Cet environnement doit être vu comme un outil pour rechercher des fuites d'information dans une implémentation en vue d'évaluer la faisabilité d'une attaque sur le produit réel. En second lieu, nous nous sommes intéressé à l'analyse de programmes écrits en langage d'assemblage AVR dans le but de vérifier s'ils sont vulnérables aux \textsl{timing attacks}. Nous avons donc développé un outil qui consiste à décrire des chemins du flot de contrôle d'un programme grâce à des expressions régulières qui seront par la suite interprétées par notre outil afin de donner leur temps exact d'exécution (en terme de cycles d'horloge). Enfin, nous avons étudié comment faciliter la compréhension de programmes écrits en langage C dans le but de vérifier si des politiques de sécurité sont correctement implémentées. D'une part, nous fournissons des assistants de navigation qui au travers d'informations concernant les variables et procédures rencontrées, facilitent la compréhension du programme. D'autre part, nous avons au point une manière de vérifier les politiques de sécurité sans modélisation préalable (e.g. avec un automate à états finis) au moyen de requêtes exprimées dans la logique CTL.

Résumé / Abstract : The work presented in this thesis aims at easing the evaluation process of smartcards embedded software. On one hand, we set up a software environment dedicated to analyze the implementation resistance of cryptographic to power analysis attacks. This environment must be seen as a tool that facilitates a real attack by giving a way to find information leakages in an implementation. On the other hand, we focused on analyzing program written in AVR assembly language in order to check whether they are vulnerable to timing attacks. To achieve this goal we have developed a tool that makes possible the description of a path in the control flow of the program thanks to regular expressions. Those regular expressions will be interpreted by our tool in order to give the exact execution timing (expressed in clock cycles). Finally, we studied how to ease the global comprehension of a program written in C language in order to check whether security policies are well implemented. First, we provide graphical navigation assisants that helps to understand the progam being analyzed by giving information on variables and procedures. Then, we provide a way to check the security policies through the use of requests expressed with the CTL logic. This approach does not need prior modelisation of the program.