Desenvolvimento formal de aplicações para smartcards

Smart card applications represent a growing market. Usually this kind of application manipulate and store critical information that requires some level of security, such as financial or confidential information. The quality and trustworthiness of smart card software can be improved through a rigorous development process that embraces formal techniques of software engineering. In this work we propose the BSmart method, a specialization of the B formal method dedicated to the development of smart card Java Card applications. The method describes how a Java Card application can be generated from a B refinement process of its formal abstract specification. The development is supported by a set of tools, which automates the generation of some required refinements and the translation to Java Card client (host) and server (applet) applications. With respect to verification, the method development process was formalized and verified in the B method, using the Atelier B tool [Cle12a]. We emphasize that the Java Card application is translated from the last stage of refinement, named implementation. This translation process was specified in ASF+SDF [BKV08], describing the grammar of both languages (SDF) and the code transformations through rewrite rules (ASF). This specification was an important support during the translator development and contributes to the tool documentation. We also emphasize the KitSmart library [Dut06, San12], an essential component of BSmart, containing models of all 93 classes/interfaces of Java Card API 2:2:2, of Java/Java Card data types and machines that can be useful for the specifier, but are not part of the standard Java Card library. In other to validate the method, its tool support and the KitSmart, we developed an electronic passport application following the BSmart method. We believe that the results reached in this work contribute to Java Card development, allowing the generation of complete (client and server components), and less subject to errors, Java Card applications.

A practical approach for biometric authentication based on smartcards

Cryptographic systems are safe. However, the management of cryptographic keys of these systems is a tough task. They are usually protected by the use of password-based authentication mechanisms, which is a weak link on conventional cryptographic systems, as the passwords can be easily copied or stolen. The usage of a biometric approach for releasing the keys is an alternative to the password-based mechanisms. But just like passwords, we need mechanisms to keep the biometrical signal safe. One approach for such mechanism is to use biometrical key cryptography. The cryptographic systems based on the use of biometric characteristics as keys are called biometrical cryptographic systems. This article presents the implementation of Fuzzy Vault, a biometrical cryptographic system written in Java, along with its performance evaluation. Fuzzy Vault was tested on a real application using smartcards.

Benchmarking de uma aproximação de ticketing as a service (Taas)

Dissertação de natureza científica realizada para obtenção do grau de Mestre em Engenharia de Redes de Computadores e Multimédia

Sähköisten reseptien hallinta

Sähköinen reseptijärjestelmä nykyisessä muodossaan sai alkunsa Sosiaali- ja terveysministeriön aloitteesta ja Kansaneläkelaitoksen toimesta vuoden 2001 aikana. Käytössä oleva kansallinen reseptipalvelin mahdollistaa potilaiden oikeudet muun muassa apteekin vapaaseen valintaan ja lääkkeiden suorakorvausmenetelmään. Sähköinen resepti pyritään integroimaan olemassa olevien potilasrekisterijärjestelmien yhteyteen, joten semanttisen webin tuomat teknologiat kuten Web-palvelut ja XML-pohjaiset kielet ovat tärkeässä asemassa reseptien hallinnassa. Tässä työssä pyritään esittämään sähköisen reseptijärjestelmän toimintaa ja sen mahdollistavia jo olemassa olevia tekniikoita. Esille tuodaan myös uusia lisäarvoa tuovia tekniikoita, kuten RDF(S)-kuvauskielet, jotka mahdollistavat muun muassa resepteihin kohdistuvat kyselyt ja täten uudet terveyspalvelut sekä potilaille että lääkäreille. Oleellista on tietenkin myös tietoturva, sillä organisaatioiden välillä resepteissä liikkuu arkaluontoisia tietoja. Turvallisuutta pyritään edistämään muun muassa sähköisillä allekirjoituksilla ja älykorttien avulla tapahtuvalla järjestelmään tunnistautumisella. Jotta sähköinen resepti toimisi tulevaisuudessakin halutulla tavalla ja mahdollistaisi lisäarvopalveluita, on siinä panostettava sisällön lisäksi senkuvaamiseen. Sisällön ja sen suhteiden tarkka määrittely auttaa muun muassa reseptikyselyjen tekemisessä, mikä onkin olennainen osa potilasturvallisuuden ylläpitoa. Kuvauskielien ja ontologioiden käyttö voi myös auttaa lääkehoidon määrittämisessä useiden erilaisten ja jatkuvasti lisääntyvien lääkkeiden viidakossa, kun lääkkeitä voidaan etsiä tietokannoista reseptin kirjoituksen yhteydessä.