logo SBA

ETD

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

Tesi etd-04272010-110934


Tipo di tesi
Tesi di dottorato di ricerca
Autore
MARTINI, LUCA
URN
etd-04272010-110934
Titolo
Checking Secure Information Flow in Programs
Settore scientifico disciplinare
ING-INF/05
Corso di studi
INGEGNERIA DELL'INFORMAZIONE
Relatori
tutor Prof.ssa De Francesco, Nicoletta
Parole chiave
  • Nessuna parola chiave trovata
Data inizio appello
22/05/2006
Consultabilità
Non consultabile
Data di rilascio
22/05/2046
Riassunto
This thesis is concerned with static code analysis. More particularly, with code analysis techniques for checking information flows in programs. First this thesis describes why is important to trace the information flows in a program, it introduces some fundamental concepts and presents the state of art. Then, two methods for checking secure information flow are proposed. The first is based on code transformation, and reuses the type analysis of the Java byte code Verifier. This method analyses programs written in a subset of the Java Virtual Machine Language. The second approach, named instruction-level security typing, has been defined in the framework of Abstract Interpretation end ha been shown more precise than standard typing approaches. This method has been applied to check the classical non-interference property in stack-based assembly programs and in high-level language programs.
File