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 ar...

ver descrição completa

Na minha lista:

Detalhes bibliográficos
Autor principal:	Silva, Antonio Augusto Viana da
Outros Autores:	Déharbe, David Boris Paul
Formato:	Dissertação
Idioma:	por
Publicado em:	Universidade Federal do Rio Grande do Norte
Assuntos:	Veri&#64257 cação formal Sistemas embarcados Java JML Provadores de teorema Formal veri&#64257 cation Embedded systems Theorem proving CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
Endereço do item:	https://repositorio.ufrn.br/jspui/handle/123456789/18084
Tags:	Adicionar Tag Sem tags, seja o primeiro a adicionar uma tag!

id	ri-123456789-18084
record_format	dspace
institution	Repositório Institucional
collection	RI - UFRN
language	por
topic	Veri&#64257 cação formal Sistemas embarcados Java JML Provadores de teorema Formal veri&#64257 cation Embedded systems Java JML Theorem proving CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
spellingShingle	Veri&#64257 cação formal Sistemas embarcados Java JML Provadores de teorema Formal veri&#64257 cation Embedded systems Java JML Theorem proving CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO Silva, Antonio Augusto Viana da Contribuições para verificação automática de applets javacard
description	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 Eiﬀel, and has been widely adopted as the de facto language when dealing with speciﬁcation 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 oﬀer 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 conﬁdent veriﬁcation of JavaCard applets. In this work we present the ﬁrst 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 speciﬁcations. 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 veriﬁcation
author2	Déharbe, David Boris Paul
author_facet	Déharbe, David Boris Paul Silva, Antonio Augusto Viana da
format	masterThesis
author	Silva, Antonio Augusto Viana da
author_sort	Silva, Antonio Augusto Viana da
title	Contribuições para verificação automática de applets javacard
title_short	Contribuições para verificação automática de applets javacard
title_full	Contribuições para verificação automática de applets javacard
title_fullStr	Contribuições para verificação automática de applets javacard
title_full_unstemmed	Contribuições para verificação automática de applets javacard
title_sort	contribuições para verificação automática de applets javacard
publisher	Universidade Federal do Rio Grande do Norte
publishDate	2014
url	https://repositorio.ufrn.br/jspui/handle/123456789/18084
work_keys_str_mv	AT silvaantonioaugustovianada contribuicoesparaverificacaoautomaticadeappletsjavacard
_version_	1773957677429293056
spelling	ri-123456789-180842017-11-04T16:36:04Z Contribuições para verificação automática de applets javacard Silva, Antonio Augusto Viana da Déharbe, David Boris Paul http://lattes.cnpq.br/3769079916577408 http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5 Silva, Ivan Saraiva http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4780113E2 Perkusich, Angelo http://lattes.cnpq.br/9439858291700830 Veri&#64257 cação formal Sistemas embarcados Java JML Provadores de teorema Formal veri&#64257 cation Embedded systems Java JML Theorem proving CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO 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 Eiﬀel, and has been widely adopted as the de facto language when dealing with speciﬁcation 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 oﬀer 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 conﬁdent veriﬁcation of JavaCard applets. In this work we present the ﬁrst 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 speciﬁcations. 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 veriﬁcation 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 veriﬁcar 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 especiﬁcar os programas aparece como uma solu¸ao natural. JML é uma linguagem de especiﬁcaçã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 especiﬁcaçã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 veriﬁcação em tempo de execução e estática. Mas as ferramentas existentes até o momento para a veriﬁcaçã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 veriﬁcaçã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 veriﬁcar as especiﬁcaçõ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 veriﬁcação automática 2014-12-17T15:48:07Z 2007-06-28 2014-12-17T15:48:07Z 2004-10-13 masterThesis SILVA, Antonio Augusto Viana da. Contribuições para verificação automática de applets javacard. 2004. 125 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2004. https://repositorio.ufrn.br/jspui/handle/123456789/18084 por Acesso Aberto application/pdf application/pdf Universidade Federal do Rio Grande do Norte BR UFRN Programa de Pós-Graduação em Sistemas e Computação Ciência da Computação

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

Registros relacionados