Made available in DSpace on 2014-12-17T15:48:00Z (GMT). No. of bitstreams: 1 SimoneOS_DISSERT_capa_ate_pag44.pdf: 4276014 bytes, checksum: c178262769ab9981c0bbfc10faf1c633 (MD5) Previous issue date: 2012-02-10 / Coordena??o de Aperfei?oamento de Pessoal de N?vel Superior / The development of smart card applications requires a high level of reliability. Formal methods provide means for this reliability to be achieved. The BSmart method and tool contribute to the development of smart card applications with the support of the B method, generating Java Card code from B specifications. For the development with BSmart to be effectively rigorous without overloading the user it is important to have a library of reusable components built in B. The goal of KitSmart is to provide this support. A first research about the composition of this library was a graduation work from Universidade Federal do Rio Grande do Norte, made by Thiago Dutra in 2006. This first version of the kit resulted in a specification of Java Card primitive types byte, short and boolean in B and the creation of reusable components for application development. This work provides an improvement of KitSmart with the addition of API Java Card specification made in B and a guide for the creation of new components. The API Java Card in B, besides being available to be used for development of applications, is also useful as a documentation of each API class. The reusable components correspond to modules to manipulate specific structures, such as date and time. These structures are not available for B or Java Card. These components for Java Card are generated from specifications formally verified in B. The guide contains quick reference on how to specify some structures and how some situations were adapted from object-orientation to the B Method. This work was evaluated through a case study made through the BSmart tool, that makes use of the KitSmart library. In this case study, it is possible to see the contribution of the components in a B specification. This kit should be useful for B method users and Java Card application developers / O desenvolvimento de aplica??es para smart cards requer um alto grau de confiabilidade. M?todos formais fornecem meios para que esta confiabilidade seja alcan?ada. O m?todo e a ferramenta BSmart fornecem uma contribui??o para que o desenvolvimento para smart cards seja feito com o aux?lio do m?todo formal B, gerando c?digo Java Card a partir de especifica??es B. Para que o desenvolvimento com o BSmart seja efetivamente rigoroso sem sobrecarregar o usu?rio do m?todo ? importante que haja uma biblioteca de componentes reutiliz?veis feitos em B. O KitSmart tem como objetivo prover esse aux?lio. Um primeiro estudo sobre a composi??o dessa biblioteca foi tema de uma monografia de gradua??o do curso de Bacharelado em Ci?ncia da Computa??o da Universidade Federal do Rio Grande do Norte, feita por Thiago Dutra em 2006. Esta primeira vers?o do kit resultou na especifica??o dos tipos primitivos permitidos em Java Card (byte, short e boolean) em B e a cria??o de componentes reutiliz?veis para o desenvolvimento de aplica??es. Esta disserta??o prov? o aperfei?oamento do KitSmart com o acr?scimo da especifica??o da API Java Card em B, e um guia para o desenvolvimento de novos componentes. A API Java Card especificada em B, al?m de estar dispon?vel para ser usada no desenvolvimento de projetos, serve como documenta??o ao especificar restri??es de uso para cada classe da API. Os componentes reutiliz?veis correspondem a m?dulos para manipula??o de estruturas espec?ficas, como data e hora, por exemplo. Estes tipos de estruturas n?o est?o dispon?veis em B ou Java Card. Os componentes reutiliz?veis para Java Card s?o gerados a partir das especifica??es verificadas formalmente em B. O guia cont?m informa??es de consulta r?pida para especifica??o de diversas estruturas e como algumas situa??es foram contornadas para adaptar a orienta??o a objetos ao M?todo B. Este trabalho foi avaliado atrav?s de um estudo de caso feito com a ferramenta BSmart que faz uso da biblioteca KitSmart. Neste estudo de caso, ? poss?vel ver a contribui??o dos componentes em uma especifica??o B. Este kit dever? ser ?til tanto para usu?rios do m?todo B como para desenvolvedores de aplica??es Java Card em geral

La mise à jour dynamique des programmes consiste en la modification de ceux-ci sans en arrêter l'exécution. Cette caractéristique est primordiale pour les applications critiques en continuelles évolutions et nécessitant une haute disponibilité. Le but de notre travail est d'effectuer la vérification formelle de la correction de la mise à jour dynamique d'applications Java Card à travers l'étude du système EmbedDSU. Pour ce faire, nous avons premièrement établi la correction de la mise à jour du code en définissant une sémantique formelle des opérations de mise à jour sur le code intermédiaire Java Card en vue d'établir la sûreté de typage des mises à jour. Nous avons ensuite proposé une approche pour vérifier la sémantique du code mis à jour à travers la définition d'une transformation de prédicats. Nous nous sommes ensuite intéressés à la vérification de la correction concernant la détection de points sûrs de la mise à jour. Nous avons utilisé la vérification de modèles. Cette vérification nous a permis de corriger d'abord un problème d'inter blocage dans le système avant d'établir d'autres propriétés de correction : la sûreté d'activation et la garantie de mise à jour. La mise à jour des données est effectuée à travers les fonctions de transfert d'état. Pour cet aspect, nous avons proposé une solution permettant d'appliquer les fonctions de transfert d’état tout en préservant la consistance du tas de la machine virtuelle Java Card et en permettant une forte expressivité dans leurs écritures. / Dynamic Software Updating (DSU) consists in updating running programs on the fly without any downtime. This feature is interesting in critical applications that are in continual evolution and that require high availability. The aim of our work is to perform formal verification the correctness of dynamic software updating in Java Card applications by studying the system EmbedDSU. To do so, we first established the correctness of code update. We achieved this by defining formal semantics for update operations on java Card bytecode in order to ensure type safety. Then, we proposed an approach to verify the semantics of updated programs by defining a predicate transformation. Afterward, we were interested in the verification of correction concerning the safe update point detection. We used model checking. This verification allowed us first to fix a deadlock situation in the system and then to establish other correctness properties: activeness safety and updatability. Data update is performed through the application of state transfer functions. For this aspect, we proposed a solution to apply state transfer functions with the preservation of the Java Card virtual machine heap consistency and by allowing a high expressiveness when writing state transfer functions.

Les cartes à puce Java comportent plusieurs mécanismes de sécurité, dont le vérifieur de code intermédiaire (\emph{$ \ll $Java Card bytecode verifier$ \gg $}), qui est composé de deux parties, la vérification de structure et la vérification de type. Ce mémoire porte sur la génération de tests de vulnérabilité pour la vérification de structure. Il s'inspire des travaux sur la vérification de type de l'outil \textsc{VTG} (\emph{$ \ll $Vulnerability Tests Generator$ \gg $}) développé par Aymerick Savary. Notre approche consiste à modéliser formellement la spécification de la structure des fichiers \textsf{CAP} avec le langage \textsf{Event-B}, en utilisant des contextes. Cette modélisation permet de donner une définition formelle d'un fichier \textsf{CAP} valide. Nous utilisons ensuite la mutation de spécification pour insérer des fautes dans cette définition dans le but de générer des fichiers \textsf{CAP} (\emph{$ \ll $Converted APplet$ \gg $}) invalides. Nous utilisons \textsc{ProB}, un explorateur de modèles \textsf{Event-B}, pour générer des tests abstraits de fichiers CAP invalides. La spécification formelle étant d'une taille importante qui entraîne une forte explosion combinatoire (plus de 250 constantes, 450 axiomes, 100 contextes), nous guidons \textsc{ProB} dans sa recherche de modèles en utilisant des valeurs prédéterminées pour un sous-ensemble de symboles de la spécification. Ce mémoire propose un ensemble de patrons de spécification pour représenter les structures des fichiers CAP. Ces patrons limitent aussi l'explosion combinatoire, tout en facilitant la tâche de spécification. Notre spécification \textsf{Event-B} comprend toute la définition des structures des fichiers CAP et une partie des contraintes. Des tests abstraits sont générés pour une partie du modèle, à titre illustratif. Ces tests ont permis de mettre en lumière des imprécisions dans la spécification \textsf{Java Card}. Ces travaux ont permis d'étendre la méthode de génération de test de vulnérabilité aux contextes \textsf{Event-B}. De plus, le modèle proposé permet de tester, à l'aide du \textsc{VTG}, une partie plus importante de la vérification de structure du vérifieur de code intermédiaire.

Computer security is a growing field in the IT industry. One of the important aspects of the computer security is authentication. Using passwords (something you know) is one of the most common ways of authentications. But passwords have proven to provide weak level of security as they can be easily compromised. Some other ways of authenticating a user are using physical tokens, (something you possess) and biometrics, (something you are). Using any one of these techniques to secure a system always has its own set of threats. One way to make sure a system is secure is to use multiple factors to authenticate. One of the ways to use multiple factors is to use all the three factors of authentication, something you possess, something you are and something you know. This thesis discusses about different ways of authentication and implements a system using three factor authentication. It takes many security aspects of the system into consideration while implementing it, to make it secure.

Smart cards are small, portable, tamper-resistant computers used in security-sensitive applications ranging from identification and access control to payment systems. Side-channel attacks, which use clues from timing, power consumption, or even electromagnetic (EM) signals, can compromise the security of these devices and have been an active research area since 1996. Newer ``contactless'' cards communicate using radio frequency (RF), without physical contact. These contactless smart cards are sometimes grouped with radio frequency identification (RFID) devices in popular usage of the term. This thesis investigates devices that use the ISO 14443 (proximity card) protocol, a large class of contactless/RFID devices. Although contactless smart cards are increasingly common, very few reproducible practical attacks have been published. Presently, there are no known documented side-channel attacks against contactless Java Cards (open standard multi-application cards) using generic unmodified hardware. This thesis develops a research-friendly platform for investigating side-channel attacks on ISO 14443 contactless smart cards. New techniques for measurement and analysis, as well as the first fully documented EM side-channel monitoring procedure, are presented for a contactless Java Card. These techniques use unmodified, commercial off-the-shelf hardware and are both practical and broadly applicable to a wide range of ISO 14443 devices, including many payment cards and electronic passports.

Smart cards are small, portable, tamper-resistant computers used in security-sensitive applications ranging from identification and access control to payment systems. Side-channel attacks, which use clues from timing, power consumption, or even electromagnetic (EM) signals, can compromise the security of these devices and have been an active research area since 1996. Newer ``contactless'' cards communicate using radio frequency (RF), without physical contact. These contactless smart cards are sometimes grouped with radio frequency identification (RFID) devices in popular usage of the term. This thesis investigates devices that use the ISO 14443 (proximity card) protocol, a large class of contactless/RFID devices. Although contactless smart cards are increasingly common, very few reproducible practical attacks have been published. Presently, there are no known documented side-channel attacks against contactless Java Cards (open standard multi-application cards) using generic unmodified hardware. This thesis develops a research-friendly platform for investigating side-channel attacks on ISO 14443 contactless smart cards. New techniques for measurement and analysis, as well as the first fully documented EM side-channel monitoring procedure, are presented for a contactless Java Card. These techniques use unmodified, commercial off-the-shelf hardware and are both practical and broadly applicable to a wide range of ISO 14443 devices, including many payment cards and electronic passports.

Il devient important d'assurer que tout système critique est fiable. Pour cela différentes techniques existent, telles que le test ou l'utilisation de méthodes formelles. S'assurer que le comportement d'un vérifieur de byte code Java Card n'entraînera pas de faille de sécurité est une tâche complexe. L'automatisation totale de cette vérification n'à popr le moment pas été realisee. Des jeux de tests coûteux ont été produits manuellement, mais ils doivent être refaits à chaque nouvelle spécification. Les travaux présentés dans ce mémoire proposent une nouvelle méthode pour la génération automatique de tests de vulnérabilité. Ceux-ci reposent sur l'utilisation et la transformation automatique de modèles formels. Pour valider cette méthode, un outil à été développé puis utilisé sur différentes implémentations du vérifieur de byte code Java Card. Le langage de modelisation que nous avons utilisé est Event-B. Nos modèles représentent le comportement normal du système que l'on souhaite tester. Chaque instruction est modélisée comme un événement. Leur garde représente l'ensemble des conditions que doit satisfaire une instruction pour être acceptable. À partir de ce modèle initial, une succession de dérivations automatiques génère un ensemble de modèles dérivés. Chacun de ces modèles dérivés représente une faute particulière. On extrait de ces nouveaux modèles les tests de vulnérabilité abstraits. Ceux-ci sont ensuite concrétisés puis envoyés à un système à tester. Ce processus est assuré par notre logiciel qui repose sur les API Rodin, ProB, CapMap et OPAL.

Zugl.: Augsburg, Universiẗat, Diss., 2008.

This study concerns machine-to-machine (M2M) applications that use smartcards. More specifically,The Subscriber Identity Module (SIM) smart card is used for the purpose of monitoring a continuousnetwork connection between a host device and a server. Multicom Security is a security company thatoffers several secure communication connection services (e.g. payment transactions, alarm signals). Themonitoring of these connections is carried out with continuous heart-beat messages sent from thedevice to a server. Today they provide this heart-beat service through logic in their own manufactureddevices, but they have a desire to place the logic on a SIM card in order to be able to move such serviceswith this card and not with a device. Such services can then also be offered on devices not necessarilymanufactured by Multicom Security.The work consisted of investigation of current telecommunication standards, papers regardingsmartcard applications and the current monitoring service, in order to consider possible solutions toimplement a proof of concept of such solution and evaluate it. One aspect of the study was to checkwhether the implemented solution was general and would work in different mobile equipments and alsoto determine the limitations of such smartcard applications.Three solutions were considered for implementation of which one was successfully implemented andtested. The successful heart-beat application was developed using a network subscription enabled JavaCard smart card and using SMS as bearer for the heart-beat messages. By evaluating the solution withbasic tests of functionality, robustness, performance and compatibility the solution was considered to begeneral and compliant with most new mobile equipments. The evaluation was performed in realenvironment with the application running on an actual SIM card with network subscription tested indifferent mobile devices such as cell phones, built-in communication modules and alarm control panels.An alternative solution based on GRPS instead of SMS was also realized but the tests could not becarried out completely due to lack of access to the SIM card implementation by the card provider.

La vérification de la résistance aux attaques des implémentations embarquées des vérifieurs de code intermédiaire Java Card est une tâche complexe. Les méthodes actuelles n'étant pas suffisamment efficaces, seule la génération de tests manuelle est possible. Pour automatiser ce processus, nous proposons une méthode appelée VTG (Vulnerability Test Generation, génération de tests de vulnérabilité). En se basant sur une représentation formelle des comportements fonctionnels du système sous test, un ensemble de tests d'intrusions est généré. Cette méthode s'inspire des techniques de mutation et de test à base de modèle. Dans un premier temps, le modèle est muté selon des règles que nous avons définies afin de représenter les potentielles attaques. Les tests sont ensuite extraits à partir des modèles mutants. Deux modèles Event-B ont été proposés. Le premier représente les contraintes structurelles des fichiers d'application Java Card. Le VTG permet en quelques secondes de générer des centaines de tests abstraits. Le second modèle est composé de 66 événements permettant de représenter 61 instructions Java Card. La mutation est effectuée en quelques secondes. L'extraction des tests permet de générer 223 tests en 45 min. Chaque test permet de vérifier une précondition ou une combinaison de préconditions d'une instruction. Cette méthode nous a permis de tester différents mécanismes d'implémentations de vérifieur de code intermédiaire Java Card. Bien que développée pour notre cas d'étude, la méthode proposée est générique et a été appliquée à d'autres cas d'études.