ETD

Archivio digitale delle tesi discusse presso l'Università di Pisa

Tesi etd-11212003-112245


Tipo di tesi
Tesi di laurea vecchio ordinamento
Autore
Masci, Paolo
Indirizzo email
paolo.masci@email.it
URN
etd-11212003-112245
Titolo
Progetto e sviluppo di un verificatore efficiente del bytecode java
Dipartimento
INGEGNERIA
Corso di studi
INGEGNERIA INFORMATICA
Relatori
relatore Bernardeschi, Cinzia
Parole chiave
  • strutture dinamiche
  • verifica
  • tesi
  • ipd
  • bytecode Java
Data inizio appello
18/12/2003
Consultabilità
Completa
Riassunto
La tecnologia Java Card costituisce il punto di contatto tra il linguaggio di programmazione Java e l’ambiente operativo di sistemi con un numero limitato di risorse. Java è un linguaggio interpretato: il codice assemblato viene eseguito su una macchina virtuale, la Java Virtual Machine (JVM), che garantisce l’indipendenza del codice dalla particolare piattaforma hardware/software. La JVM gioca inoltre un ruolo centrale per quanto riguarda la sicurezza e la correttezza del codice eseguito: la sicurezza è legata a meccanismi che controllano i diritti di accesso a informazioni e funzionalità, la correttezza garantisce invece che i meccanismi di sicurezza non vengano by-passati. Il “verificatore” è il modulo della JVM che analizza la correttezza del codice: la tecnologia corrente non consente l’implementazione di un verificatore “standard” direttamente on-card perché il processo di verifica richiede in genere un numero elevato di risorse. In questa tesi viene proposto un verificatore che ottimizza l’utilizzo delle risorse attraverso una analisi del grafo di flusso del codice: l’idea di base è di scomporre il codice in blocchi indipendenti e di rendere dinamica l’allocazione delle risorse applicando l’algoritmo di verifica ad ogni blocco. Le risorse da allocare sono solo quelle necessarie alla verifica di un sotto-insieme di istruzioni: la complessità del processo di verifica diminuisce e la realizzazione di un verificatore on-card diventa un obiettivo raggiungibile. E’ stato inoltre sviluppato un prototipo a partire dal codice di un verificatore open-source.