ETD system

Electronic theses and dissertations repository

 

Tesi etd-11212003-112245


Thesis type
Tesi di laurea vecchio ordinamento
Author
Masci, Paolo
email address
paolo.masci@email.it
URN
etd-11212003-112245
Title
Progetto e sviluppo di un verificatore efficiente del bytecode java
Struttura
INGEGNERIA
Corso di studi
INGEGNERIA INFORMATICA
Commissione
relatore Bernardeschi, Cinzia
Parole chiave
  • strutture dinamiche
  • verifica
  • tesi
  • ipd
  • bytecode Java
Data inizio appello
18/12/2003;
Consultabilità
completa
Riassunto analitico
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.