Evaluation d’applications de paiement sur carte à puce
Institution:
CaenDisciplines:
Directors:
Abstract EN:
This thesis deals with high-level evaluation of applications in smartcards. The proposed method combines observation of the communication and detection of violated properties. The goal is to detect anomalies on smart cards (and more precisely on its implementation) and provide a better documentation on this error and on the reasons that triggered this error. We can know on the fly if an application has an error of implementation. The user of the tool configures a set of properties corresponding to the expected behavior of the application. To ascertain compliance of the behavior of the card application with the theory (specifications), the first step is the generation of the oracle, reference used during verification and validation activity. We quickly directed to a smarter technique to target the most interesting behaviors to check for our study. We worked on a generation method based on a genetic algorithm taking as input a set of transaction logs to automatically generate a set of properties (i. E. A set of local and expected behaviors of the applications). The evaluation methodology is developed through the WSCT framework. Two plugins were created and used to communicate with the smart card application, but also to observe and detect an abnormality in the behavior of the application. We used a JavaCard applet developed in the laboratory to test the feasibility of the method for two use cases: during the test phase, the methodology can be used in parallel by the certification firm and during the development of an application, for example, allowing improving the teaching of the JavaCard development and the evaluation of application.
Abstract FR:
Cette thèse traite des méthodes d'évaluation de haut niveau, proche des applications. Une méthode d'évaluation d'application sur cartes à puces, complémentaire aux méthodes existantes, a été définie durant de la thèse. Le but est de détecter les anomalies présentes sur cartes à puce (et plus précisément sur l'application de la carte à puce) et de fournir une documentation accrue sur cette erreur ainsi que les raisons déclencheurs de cette erreur. L'utilisateur de l'outil configure un ensemble de propriétés correspondant aux comportements attendus de l'application qu'il va vérifier. Afin de connaître la conformité du comportement de l'application carte vis à vis de la théorie (spécifications), la première étape est la génération de l'oracle, élément de référence lors d'une activité de vérification et validation. Nous nous sommes orientés vers une technique plus intelligente basée sur un algorithme génétique prenant en entrée un ensemble de logs de transaction qui permet de générer automatiquement un ensemble de propriétés (c'est à dire un ensemble de comportements locaux et attendus de l'application carte). La méthode de vérification est développée grâce au framework WSCT. Nous avons utilisé une applet JavaCard développée au laboratoire afin de tester la faisabilité de la méthode pour deux cas d'usages : lors de la phase de test, la méthodologie peut être utilisée en parallèle de la méthode utilisée par l'entreprise de certification et lors du développement de l'application, l'utilisation de cette méthodologie permet un guidage du développement, ce qui permet de l'utiliser dans le cadre de l'enseignement du développement JavaCard et de l'évaluation d'applications.