• Bytecode Java
• Flusso di Informazioni
• Sicurezza
• Verificatore di Bytecode

La estrema velocità con cui si è espanso l'utilizzo di Internet e di dispositivi come le smart card ha spinto la ricerca nel campo della verifica della sicurezza del Java Bytecode. È proprio la versatilità offerta dalle smart card che ha contribuito alla loro diffusione e quindi ha reso necessario lo sviluppo di strumenti atti alla verifica della sicurezza delle informazioni in tale ambito. A causa delle risorse limitate a disposizione nelle smart card è nata l'idea di utilizzare l’algoritmo del Verificatore di bytecode Java come strumento per il controllo del flusso delle informazioni, poichè esso è già presente all'interno della Java Virtual Machine (JVM). Il bytecode in ingresso al verificatore viene opportunamente trasformato in modo che un errore di tipo, rilevato dal verificatore stesso, corrisponda ad una possibile violazione della segretezza delle informazioni nel codice originale. In questa tesi, è stato presentato un modello per la verifica del flusso sicuro delle informazioni, nel bytecode Java, basato sul controllo di tipo. Il modello estende uno strumento esistente (Tool SFT). L’assegnamento dei livelli di sicurezza, in origine, prevedeva la possibilità di assegnare livelli esclusivamente alle classi. Questo modello è stato ampliato in modo da poter attribuire un livello diverso ad ogni singolo campo all'interno di una classe. È stato reso possibile inoltre determinare una politica di assegnamento dei livelli di sicurezza ai parametri di un metodo, in funzione dell'ambiente di chiamata del metodo stesso. Il codice del Tool SFT è stato modificato per supportare le nuove funzionalità.