La crescente complessità delle applicazioni web insieme ai protocolli sottostanti di sicurezza ha fatto rapidamente crescere la necessità di un'analisi automatica tramite metodologie e applicativi. In questa tesi, tratto questo problema proponendo due nuovi approcci formali per la verifica dei protocolli di sicurezza e di applicazioni web. Il primo è un metodo per la verifica di protocolli di sicurezza a tempo di design basato sull'interpolazione. Questo metodo comincia da una specifica di un protocollo e combina interpolazione di Craig, esecuzione simbolica e il modello standard di intruder Dolev-Yao per cercare possibili attacchi al protocollo. Gli interpolanti vengono generati come risposta ad un insuccesso durante la ricerca per poter eliminare tracce inutili e velocizzare l'esplorazione. Il secondo è un metodo per l'analisi di sicurezza a runtime che cerca errori di implementazione e logici su un sistema (web) concreto. In particolare, mi sono concentrato su come usare il modello di intruder Dolev-Yao per cercare attacchi Cross-Site Request Forgery (CSRF). CSRF compare nella lista dei 10 attacchi più critici per la sicurezza web di Open Web Application Security Project (OWASP).

The increasing complexity of web applications together with their underling security protocols has rapidly increased the need of automatic security analysis methods and tools. In this thesis, I address this problem by proposing two new formal approaches for the security verification of security protocols and web applications. The first is a design time interpolation-based method for security protocol verification. This method starts from a protocol specification and combines Craig interpolation, symbolic execution and the standard Dolev-Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. The second is a runtime (model-based) security analysis technique that searches for logic and implementation flaws on concrete (web-based) systems. In particular, I focused on how to use the Dolev-Yao intruder model to search for Cross-Site Request Forgery (CSRF) attacks. CSRF is listed in the top ten list of the Open Web Application Security Project (OWASP) as one of the most critical threats to web security.

Methods and tools for design time and runtime formal analysis of security protocols and web applications

Rocchetto, Marco
2015-01-01

Abstract

The increasing complexity of web applications together with their underling security protocols has rapidly increased the need of automatic security analysis methods and tools. In this thesis, I address this problem by proposing two new formal approaches for the security verification of security protocols and web applications. The first is a design time interpolation-based method for security protocol verification. This method starts from a protocol specification and combines Craig interpolation, symbolic execution and the standard Dolev-Yao intruder model to search for possible attacks on the protocol. Interpolants are generated as a response to search failure in order to prune possible useless traces and speed up the exploration. The second is a runtime (model-based) security analysis technique that searches for logic and implementation flaws on concrete (web-based) systems. In particular, I focused on how to use the Dolev-Yao intruder model to search for Cross-Site Request Forgery (CSRF) attacks. CSRF is listed in the top ten list of the Open Web Application Security Project (OWASP) as one of the most critical threats to web security.
2015
Model Checking; information security; craig interpolation
La crescente complessità delle applicazioni web insieme ai protocolli sottostanti di sicurezza ha fatto rapidamente crescere la necessità di un'analisi automatica tramite metodologie e applicativi. In questa tesi, tratto questo problema proponendo due nuovi approcci formali per la verifica dei protocolli di sicurezza e di applicazioni web. Il primo è un metodo per la verifica di protocolli di sicurezza a tempo di design basato sull'interpolazione. Questo metodo comincia da una specifica di un protocollo e combina interpolazione di Craig, esecuzione simbolica e il modello standard di intruder Dolev-Yao per cercare possibili attacchi al protocollo. Gli interpolanti vengono generati come risposta ad un insuccesso durante la ricerca per poter eliminare tracce inutili e velocizzare l'esplorazione. Il secondo è un metodo per l'analisi di sicurezza a runtime che cerca errori di implementazione e logici su un sistema (web) concreto. In particolare, mi sono concentrato su come usare il modello di intruder Dolev-Yao per cercare attacchi Cross-Site Request Forgery (CSRF). CSRF compare nella lista dei 10 attacchi più critici per la sicurezza web di Open Web Application Security Project (OWASP).
File in questo prodotto:
File Dimensione Formato  
PhD_thesis_MarcoRocchetto.pdf

non disponibili

Tipologia: Tesi di dottorato
Licenza: Accesso ristretto
Dimensione 3.06 MB
Formato Adobe PDF
3.06 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/913185
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact