Facultad de Ingeniería Proyecto de Taller V año 2000 Especificación Formal de la Máquina Virtual Java Card 1



Descargar 309,5 Kb.
Página1/7
Fecha de conversión24.03.2017
Tamaño309,5 Kb.
  1   2   3   4   5   6   7

Especificación Formal de la Máquina Virtual Java Card 2.1 Taller V

Facultad de Ingeniería
Proyecto de Taller V
Año 2000

Especificación Formal de la Máquina Virtual Java Card 2.1



Autores:

Jorge Erlich

Leonardo Grandillo
Tutores

Gustavo Betarte

Alberto Pardo

Resumen
Este documento presenta resultados sobre el desarrollo de una especificación formal de la Máquina Virtual Java Card (JCVM) y de la implementación de un prototipo. Como herramienta de especificación se usó Semántica Operacional Estructural (SOS).

El prototipo está implementado en el lenguaje de programación Java. El código del mismo está fuertemente basado en la especificación obtenida, permitiendo simular ejecuciones de esta máquina abstracta.

Relacionado con el resultado de la especificación formal de la JCVM, se indica como se generan sus áreas de datos.

Asimismo, se introduce al lector al mundo de las tarjetas inteligentes, y en particular, a la tecnología Java Card.


Los apéndices que se adjuntan a este documento reflejan los resultados obtenidos en forma detallada, del funcionamiento interno de la JCVM, de la semántica de las instrucciones ejecutadas por la misma; de la definición de sus áreas de datos, de las decisiones tomadas al realizar la semántica de las instrucciones ejecutadas por la JCVM y del diseño detallado del prototipo implementado.

Indice

1 Introducción 7

1.1 Objetivos del Proyecto 8

1.2 Estructura del Documento 8

2 Conceptos Básicos de la Tecnología Java Card 9

2.1 Introducción a la Java Card 9

2.1.1 ¿Qué es una Tarjeta Inteligente? 9

2.1.2 ¿Qué es una Java Card? 11

2.1.2.1 El tiempo de vida de una Java Card 11

2.1.2.2 El tiempo de Vida de una JCVM 12

2.1.2.3 El tiempo de Vida de applets y objetos en la Java Card 12

2.1.2.4 El framework de la Java Card 2.1 12

2.2 Ambiente de ejecución 13

2.2.1 Introducción a la JCVM 13

2.2.2 Introducción al JCRE 15

2.2.3 Seguridad de la Java Card 16

2.2.4 Comparación de las áreas de datos de la JCVM y la JVM 16

2.2.4.1 Tipos de Datos 17

2.2.4.2 Palabras 17

2.2.4.3 Areas de datos en tiempo de ejecución 17

3 Especificación Formal de la JCVM 19

3.1 Definición del Area de Datos de la JCVM 19

3.1.1 Tipos Básicos 20

3.1.2 Tipos Tprim , Num y Ref 20

3.1.3 Array de Variables Locales 21

3.1.4 Stack Operando 21

3.1.5 Frame 21

3.1.6 Stack Java 21

3.1.7 Heap 21

3.1.8 Constant Pool 21

3.1.9 Información de Clases e Interfaces 23

3.1.10 Información de Métodos 24

3.1.11 Imagen de Campos Estáticos 25

3.1.12 Registro PC 25

3.1.13 Estado de la JCVM 25

3.2 Formalización de las Instrucciones de la JCVM 26

3.2.1 Lista de Instrucciones de la JCVM Formalizadas 26

3.2.2 Formalización de algunas Instrucciones en Semántica Operacional Estructural 26

3.2.2.1 Instrucción Tload 28

3.2.2.2 Instrucción Tstore 29

3.2.2.3 Instrucción getfield_ 30

3.2.2.4 Instrucción putfield_ 32

3.2.2.5 Instrucción new 34

3.2.2.6 Instrucción invokevirtual 36

3.3 Creación de las áreas de datos de la JCVM a partir del archivo CAP 39

4 Prototipo de la JCVM 41

4.1 MOR 42

4.2 Ejecución de ByteCode 44

5 Conclusiones 51

5.1 Extensiones del proyecto 52

6 Bibliografía 53



Apéndice A: Definición del Area de Datos de la Máquina Virtual Java Card 2.1

Apéndice B: Formalización de las instrucciones de la Máquina Virtual Java Card 2.1

Apéndice C Decisiones

Apéndice D Prototipo de la Máquina Virtual Java Card 2.1







  1. Compartir con tus amigos:
  1   2   3   4   5   6   7


La base de datos está protegida por derechos de autor ©absta.info 2019
enviar mensaje

    Página principal