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.

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior

As aplicações para smart cards representam um mercado que cresce a cada ano. Normalmente, essas aplicações manipulam e armazenam informações que requerem garantias de segurança, tais como valores monetários ou informações confidenciais. A qualidade e a segurança do software para cartões inteligentes pode ser aprimorada através de um processo de desenvolvimento rigoroso que empregue técnicas formais da engenharia de software. Neste trabalho propomos o método BSmart, uma especialização do método formal B dedicada ao desenvolvimento de aplicações para smart cards na linguagem Java Card. O método descreve, em um conjunto de etapas, como uma aplicação smart card pode ser gerada a partir de refinamentos em sua especificação formal. O desenvolvimento é suportado por um conjunto de ferramentas, automatizando a geração de parte dos refinamentos e a tradução para as aplicações Java Card cliente (host) e servidora (applet). Ressalta-se que o processo de especificação e refinamento descrito no método foi formalizado e verificado utilizando o próprio método B, com o auxílio da ferramenta Atelier B [Cle12a]. Destaca-se que a aplicação Java Card é traduzida a partir do último passo de refinamento, denominado de implementação. A especificação dessa tradução foi feita na linguagem ASF+SDF [BKV08]. Inicialmente, descreveu-se as gramáticas das linguagens B e Java (SDF) e, em uma etapa posterior, especificou-se as transformações de B para Java Card através de regras de reescrita de termos (ASF). Essa abordagem foi um importante auxílio durante o processo de tradução, além de servir ao propósito de documentálo. Cumpre destacar a biblioteca KitSmart [Dut06, San12], componente essencial ao método BSmart, que inclui modelos em B de todas as 93 classes/interfaces da API Java Card na versão 2:2:2, dos tipos de dados Java e Java Card e de máquinas que podem ser úteis ao especificador, mas que não estão presentes na API padrão. Tendo em vista validar o método, seu conjunto de ferramentas e a biblioteca KitSmart, procedeu-se com o desenvolvimento, seguindo o método BSmart, de uma aplicação de passaporte eletrônico. Os resultados alcançados neste trabalho contribuem para o desenvolvimento smart card, na medida em que possibilitam a geração de aplicações Java Card completas (cliente e servidor) e menos sujeitas a falhas.