logo SBA

ETD

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

Tesi etd-03062007-123926


Tipo di tesi
Tesi di laurea specialistica
Autore
Italiano, Emilio
URN
etd-03062007-123926
Titolo
Politically Correct: Uno strumento per la verifica di Politiche di Sicurezza su History Expressions.
Dipartimento
SCIENZE MATEMATICHE, FISICHE E NATURALI
Corso di studi
INFORMATICA
Relatori
Relatore Ferrari, Gian Luigi
Relatore Bartoletti, Massimo
Relatore Zunino, Roberto
Parole chiave
  • Lambda Calcolo
  • History Expression
  • Model Checking
Data inizio appello
05/04/2007
Consultabilità
Completa
Riassunto
Viene presentato il prototipo di un Model Checker per la verifica statica di proprietá di sicurezza, in un contesto di servizi distribuiti descritti tramite espressioni lambda-req. Queste sono un'estensione del lambda-calcolo per rappresentare reti di servizi. In questo modello, sia i servizi che i loro client possono proteggersi imponendo dei vincoli di sicurezza sul comportamento delle altre entitá tramite un meccanismo di invocazione per proprietá.

L'approccio utilizzato permette di comporre i vari servizi, garantendo che la loro esecuzione sia sicura, senza dover ricorrere a verifiche dinamiche. Questo è realizzabile in quanto, a partire dalle espressioni lambda-req, si possono inferire a priori le possibili sequenze di eventi critici per la sicurezza, descritte tramite History Expression.

Le proprietá di sicurezza vengono rappresentate come automi di Büchi, in accordo alle piú diffuse tecniche di Model Checking, le quali vengono prese in esame in conclusione del lavoro.

Lo strumento è stato realizzato principalmente in Ocaml, con un'interfaccia grafica Java per la definizione degli automi.
File