Contribuições para verificação automática de applets javacard

The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification

O grande crescimento do uso de smart cards (por bancos, companhias de transporte, celulares, etc) trouxe um fato importante, que deve ser considerado: a necessidade de ferramentas que possam ser usadas para verificar os cartões, para que se possa garantir a corretude de seu software. Como a grande maioria dos cartões desenvolvidos hoje em dia usa a tecnologia JavaCard em sua camada de software, o uso da Java Modeling Language (JML) para especificar os programas aparece como uma solu¸ao natural. JML é uma linguagem de especificação formal ligada ao Java. Ela foi inspirada pelas metodologias de Larch e Eiffel, e foi largamente adotada como a linguagem de facto em se tratando da especificação de qualquer programa relacionado à Java. Várias ferramentas que fazem uso de JML já foram desenvolvidas, cobrindo uma grande gama de funcionalidades, entre elas, a verificação em tempo de execução e estática. Mas as ferramentas existentes até o momento para a verificação estática não são totalmente automatizadas, e, aquelas que são, não oferecem um nível adequado de completude e segurança. Nosso objetivo é contribuir com uma série de técnicas, que podem ser usadas para alcançar uma verificação completamente automática e segura para applets JavaCard. Nesse trabalho nós apresentamos os primeiros passos nessa direção. Com o uso de uma plataforma de software composta pelo Krakatoa, Why e haRVey, nós desenvolvemos um conjunto de técnicas para reduzir o tamanho da teoria necessária para verificar as especificações. Tais técnicas deram resultados muito bons, com ganhos de quase 100% em todos os testes que realizamos, e se provou como uma técnica que deve ser sempre considerAda, não somente nesse, mas na maioria dos problemas reais relacionado com verificação automática