BACHECA TESI
Edizione 2009
Vincenzo Ampolo (Dipartimento di Elettronica ed Informazione, Politecnico di Milano)
"Bluebat 2.0: Bluetooth Honeypot"
Link esterno alla tesi: http://mercurial.intuxication.org/hg/bluebat-honeypot/raw-file/f5b4986b976c/trunk/TesiLatex/TesiFinal.pdf
Link esterno al gruppo di ricerca: http://www.wombat-project.eu/
"Bluebat 2.0: Bluetooth Honeypot"Link esterno alla tesi: http://mercurial.intuxication.org/hg/bluebat-honeypot/raw-file/f5b4986b976c/trunk/TesiLatex/TesiFinal.pdf
Link esterno al gruppo di ricerca: http://www.wombat-project.eu/
Vincenzo Ampolo (Dipartimento di Elettronica ed Informazione, Politecnico di Milano)
"Bluebat 2.0: Bluetooth Honeypot"
(Relatore: prof. Stefano Zanero).
La tesi di laurea triennale in oggetto discute del protocollo Bluetooth, delle sue flaws di sicurezza e parte dal lavoro svolto finora nel campo delle honeypot Bluetooth per realizzare una honeypot dall'architettura client/server. La honeypot risolve gran parte, se non la totalità, dei problemi che sono stati evidenziati durante lo studio di altre honeypot Bluetooth esistenti, in primis, la tesi di laurea specialistica di Antonio Gerardo Galante, sempre del Politecnico di Milano. La honeypot rientra nel progetto Europeo di ricerca WOMBAT, atto a proteggere cittadini e aziende europee da attacchi di sicurezza informatica. Il progetto punta a costruire una rete di sensori, pluripiattaforma e pluriprotocollo, che collaborano tra di loro e catalogano i dati interrogabili poi tramite richieste XML SOAP. Nel capitolo 2 si introduce e si spiega nel dettaglio le tre operazioni scopo del progetto WOMBAT. Nel capitolo 3 si spiega, nel dettaglio, il protocollo Bluetooth ed i relativi profili di comunicazione. Si esegue inoltre un'analisi di tutto il malware finora registrato e se ne individuano le cause di propagazione. Questa analisi rappresenta un contributo originale non essendo ancora disponibile nella letteratura di settore. Nel capitolo 4 si analizza Bluebat honeypot v 1.0 e si illustra il design della versione 2.0. Il codice della honeypot è totalmente incluso nel documento nell'appendice C. Nell'appendice A si illustrano i livelli ISO OSI dal quale il protocollo Bluetooth prende ispirazione. Infine nell'appendice B si descrivono i test effettuati per testare la honeypot v 2.0.
Link esterno alla tesi: http://mercurial.intuxication.org/hg/bluebat-honeypot/raw-file/f5b4986b976c/trunk/TesiLatex/TesiFinal.pdf
Link esterno al gruppo di ricerca: http://www.wombat-project.eu/
"Bluebat 2.0: Bluetooth Honeypot"(Relatore: prof. Stefano Zanero).
La tesi di laurea triennale in oggetto discute del protocollo Bluetooth, delle sue flaws di sicurezza e parte dal lavoro svolto finora nel campo delle honeypot Bluetooth per realizzare una honeypot dall'architettura client/server. La honeypot risolve gran parte, se non la totalità, dei problemi che sono stati evidenziati durante lo studio di altre honeypot Bluetooth esistenti, in primis, la tesi di laurea specialistica di Antonio Gerardo Galante, sempre del Politecnico di Milano. La honeypot rientra nel progetto Europeo di ricerca WOMBAT, atto a proteggere cittadini e aziende europee da attacchi di sicurezza informatica. Il progetto punta a costruire una rete di sensori, pluripiattaforma e pluriprotocollo, che collaborano tra di loro e catalogano i dati interrogabili poi tramite richieste XML SOAP. Nel capitolo 2 si introduce e si spiega nel dettaglio le tre operazioni scopo del progetto WOMBAT. Nel capitolo 3 si spiega, nel dettaglio, il protocollo Bluetooth ed i relativi profili di comunicazione. Si esegue inoltre un'analisi di tutto il malware finora registrato e se ne individuano le cause di propagazione. Questa analisi rappresenta un contributo originale non essendo ancora disponibile nella letteratura di settore. Nel capitolo 4 si analizza Bluebat honeypot v 1.0 e si illustra il design della versione 2.0. Il codice della honeypot è totalmente incluso nel documento nell'appendice C. Nell'appendice A si illustrano i livelli ISO OSI dal quale il protocollo Bluetooth prende ispirazione. Infine nell'appendice B si descrivono i test effettuati per testare la honeypot v 2.0.
Link esterno alla tesi: http://mercurial.intuxication.org/hg/bluebat-honeypot/raw-file/f5b4986b976c/trunk/TesiLatex/TesiFinal.pdf
Link esterno al gruppo di ricerca: http://www.wombat-project.eu/
Elena Chiara Beltrami (DTI Crema / Università degli Studi di Milano)
"Strumenti per il controllo della corrispondenza informatica del lavoratore e responsabilità penale"
"Strumenti per il controllo della corrispondenza informatica del lavoratore e responsabilità penale"Elena Chiara Beltrami (DTI Crema / Università degli Studi di Milano)
"Strumenti per il controllo della corrispondenza informatica del lavoratore e responsabilità penale"
(Relatore: Prof.ssa Sabrina De Capitani Di Vimercati / Prof.ssa Claudia Pecorella).
Con l’evolversi della moderna società dell’informazione la posta elettronica ha assunto un’importanza sempre più rilevante, andando dapprima ad affiancare ed in molti casi a sostituire il ruolo svolto dalla posta cartacea tradizionale. I mezzi di comunicazione elettronici e tradizionali sono utilizzati quotidianamente sia in ambito privato sia lavorativo, ma se la natura tangibile della corrispondenza epistolare implica l’identificazione e la tutela di un oggetto che è unico e collocabile nello spazio, per cui è possibile definire un solo tragitto dalla creazione fino al recapito, la posta elettronica non possiede le medesime caratteristiche di fisicità, consistendo in un flusso di dati trasmessi in rete e per questo tracciabili, intercettabili e duplicabili. Nella forma elettronica la separazione tra posta privata e lavorativa è di difficile attuazione quando il lavoratore è sul posto di lavoro poiché è possibile leggere un messaggio ovunque ci si trovi: basta disporre di un pc e di una connessione a Internet. Nelle aziende è consuetudine l’assegnamento di un indirizzo e-mail al lavoratore che può essere generico e identificare un gruppo, piuttosto che nominativo. La questione assai dibattuta è se la posta elettronica di un lavoratore sia da tutelare, dal punto di vista della privacy, alla stessa stregua della corrispondenza privata. I controlli che il datore di lavoro può effettuare sulla posta elettronica del lavoratore sono molteplici e l’obiettivo di questo studio è la loro analisi, per determinarne le eventuali responsabilità penali in caso di violazione delle norme.
"Strumenti per il controllo della corrispondenza informatica del lavoratore e responsabilità penale"(Relatore: Prof.ssa Sabrina De Capitani Di Vimercati / Prof.ssa Claudia Pecorella).
Con l’evolversi della moderna società dell’informazione la posta elettronica ha assunto un’importanza sempre più rilevante, andando dapprima ad affiancare ed in molti casi a sostituire il ruolo svolto dalla posta cartacea tradizionale. I mezzi di comunicazione elettronici e tradizionali sono utilizzati quotidianamente sia in ambito privato sia lavorativo, ma se la natura tangibile della corrispondenza epistolare implica l’identificazione e la tutela di un oggetto che è unico e collocabile nello spazio, per cui è possibile definire un solo tragitto dalla creazione fino al recapito, la posta elettronica non possiede le medesime caratteristiche di fisicità, consistendo in un flusso di dati trasmessi in rete e per questo tracciabili, intercettabili e duplicabili. Nella forma elettronica la separazione tra posta privata e lavorativa è di difficile attuazione quando il lavoratore è sul posto di lavoro poiché è possibile leggere un messaggio ovunque ci si trovi: basta disporre di un pc e di una connessione a Internet. Nelle aziende è consuetudine l’assegnamento di un indirizzo e-mail al lavoratore che può essere generico e identificare un gruppo, piuttosto che nominativo. La questione assai dibattuta è se la posta elettronica di un lavoratore sia da tutelare, dal punto di vista della privacy, alla stessa stregua della corrispondenza privata. I controlli che il datore di lavoro può effettuare sulla posta elettronica del lavoratore sono molteplici e l’obiettivo di questo studio è la loro analisi, per determinarne le eventuali responsabilità penali in caso di violazione delle norme.
Angelo Tommaso Capossele (Corso di Laurea Specialistica in Informatica)
"Soluzioni per lo scambio di chiavi nelle reti di sensori"
"Soluzioni per lo scambio di chiavi nelle reti di sensori"Angelo Tommaso Capossele (Corso di Laurea Specialistica in Informatica)
"Soluzioni per lo scambio di chiavi nelle reti di sensori"
(Relatore: Prof.ssa Chiara Petrioli).
Nonostante i numerosi anni di intensa ricerca, l'area della sicurezza e della crittografia nelle Wireless Sensor Networks presenta ancora diverse lacune. Molte sono le soluzioni di sicurezza proposte in letteratura, ma poche di queste sono state effettivamente realizzate e analizzate in termini di efficienza energetica. L'obiettivo di questo lavoro comprende lo studio delle soluzioni presenti in letteratura, l'individuazione di schemi crittografici che permettano la realizzazione di un framework di sicurezza generale, a basso consumo energetico ed implementabile su dispositivi con limitate risorse computazioni e di memoria, la progettazione e l'implementazione e test di tale framework. Il lavoro è stato impostato pensando ad uno stack protocollare per reti di sensori wireless completo, che si basasse sul protocollo di sicurezza più diffuso su Internet, il TLS. Il framework da noi proposto, TinyTLS, è infatti un adattamento del TLS, reso idoneo per un ambiente come le WSN, grazie anche all'integrazione di un algoritmo di crittografia a chiave pubblica basato sull'identità (IBE), l'ID-NIKDS. Questo algoritmo permette di realizzare un meccanismo per lo scambio di chiavi in modo non interattivo, risparmiando così sulla quantità di messaggi da trasmettere. Con TinyTLS diventa possibile per due nodi instaurare un canale sicuro garantendo confidenzialità, autenticazione e integrità, permettendo di raggiungere l'agreement della chiave con l'invio di soli 72 byte scambiati tra le parti.
"Soluzioni per lo scambio di chiavi nelle reti di sensori"(Relatore: Prof.ssa Chiara Petrioli).
Nonostante i numerosi anni di intensa ricerca, l'area della sicurezza e della crittografia nelle Wireless Sensor Networks presenta ancora diverse lacune. Molte sono le soluzioni di sicurezza proposte in letteratura, ma poche di queste sono state effettivamente realizzate e analizzate in termini di efficienza energetica. L'obiettivo di questo lavoro comprende lo studio delle soluzioni presenti in letteratura, l'individuazione di schemi crittografici che permettano la realizzazione di un framework di sicurezza generale, a basso consumo energetico ed implementabile su dispositivi con limitate risorse computazioni e di memoria, la progettazione e l'implementazione e test di tale framework. Il lavoro è stato impostato pensando ad uno stack protocollare per reti di sensori wireless completo, che si basasse sul protocollo di sicurezza più diffuso su Internet, il TLS. Il framework da noi proposto, TinyTLS, è infatti un adattamento del TLS, reso idoneo per un ambiente come le WSN, grazie anche all'integrazione di un algoritmo di crittografia a chiave pubblica basato sull'identità (IBE), l'ID-NIKDS. Questo algoritmo permette di realizzare un meccanismo per lo scambio di chiavi in modo non interattivo, risparmiando così sulla quantità di messaggi da trasmettere. Con TinyTLS diventa possibile per due nodi instaurare un canale sicuro garantendo confidenzialità, autenticazione e integrità, permettendo di raggiungere l'agreement della chiave con l'invio di soli 72 byte scambiati tra le parti.
Francesco Carata (DTI Crema / Università degli studi di Milano)
"MHIDS - Managed Host Intrusion Detection System"
"MHIDS - Managed Host Intrusion Detection System"Francesco Carata (DTI Crema / Università degli studi di Milano)
"MHIDS - Managed Host Intrusion Detection System"
(Relatore: prof. Marco Cremonini).
Lo scopo della tesi è stato di progettare e realizzare un HIDS al fine di permettere il monitoraggio e la successiva analisi delle attività svolte a livello di singolo host. La particolare natura interamente managed del sistema dovuta all’adozione di un linguaggio di alto livello come il C#, consente di compiere azioni di basso livello senza ricorrere al classico uso di hook a livello kernel al fine di evitare: Problemi di performance ed instabilità; Errori di programmazione (es. buffer overflow); Attacchi dovuti ad errori di implementazione ( es. bound checking), L'utilizzo del sistema all’interno di una rete aziendale può permettere di effettuare attività di: Auditing in real-time al fine di rilevare condizioni anomale negli host; Confronto tra azioni operate negli host e policy aziendali al fine di determinarne la conformità; Controllo del software distribution e del patch management; Analisi di condizioni anomale anche attraverso tecniche di data fusion e corralazione; Controllo e localizzazione tempestiva di minacce attraverso l'analisi dei dati (es. malware).
"MHIDS - Managed Host Intrusion Detection System"(Relatore: prof. Marco Cremonini).
Lo scopo della tesi è stato di progettare e realizzare un HIDS al fine di permettere il monitoraggio e la successiva analisi delle attività svolte a livello di singolo host. La particolare natura interamente managed del sistema dovuta all’adozione di un linguaggio di alto livello come il C#, consente di compiere azioni di basso livello senza ricorrere al classico uso di hook a livello kernel al fine di evitare: Problemi di performance ed instabilità; Errori di programmazione (es. buffer overflow); Attacchi dovuti ad errori di implementazione ( es. bound checking), L'utilizzo del sistema all’interno di una rete aziendale può permettere di effettuare attività di: Auditing in real-time al fine di rilevare condizioni anomale negli host; Confronto tra azioni operate negli host e policy aziendali al fine di determinarne la conformità; Controllo del software distribution e del patch management; Analisi di condizioni anomale anche attraverso tecniche di data fusion e corralazione; Controllo e localizzazione tempestiva di minacce attraverso l'analisi dei dati (es. malware).
Roberto Carbone (AI-Lab, DIST, Università di Genova)
"LTL Model-Checking for Security Protocols"
Link esterno al gruppo di ricerca: http://www.ai-lab.it
"LTL Model-Checking for Security Protocols"Link esterno al gruppo di ricerca: http://www.ai-lab.it
Roberto Carbone (AI-Lab, DIST, Università di Genova)
"LTL Model-Checking for Security Protocols"
(Relatore: Alessandro Armando).
Since security protocols are at the core of security-sensitive applications, their proper functioning is crucial. They are notoriously error-prone and it is thus of utmost importance to have tools that support the activity of finding flaws. Most model checking techniques for protocols make a number of simplifying assumptions that prevent their applicability in some important cases. This Thesis presents a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analysers. The effectiveness of the approach is assessed against the formal analysis of relevant security protocols, with the detection of a severe security flaw in Google's SAML-based SSO for Google Apps and a previously unknown attack on a patched version of the ASW contract signing protocol.
Link esterno al gruppo di ricerca: http://www.ai-lab.it
"LTL Model-Checking for Security Protocols"(Relatore: Alessandro Armando).
Since security protocols are at the core of security-sensitive applications, their proper functioning is crucial. They are notoriously error-prone and it is thus of utmost importance to have tools that support the activity of finding flaws. Most model checking techniques for protocols make a number of simplifying assumptions that prevent their applicability in some important cases. This Thesis presents a general model for security protocols based on the set-rewriting formalism that, coupled with the use of LTL, allows for the specification of assumptions on principals and communication channels as well as complex security properties that are normally not handled by state-of-the-art protocol analysers. The effectiveness of the approach is assessed against the formal analysis of relevant security protocols, with the detection of a severe security flaw in Google's SAML-based SSO for Google Apps and a previously unknown attack on a patched version of the ASW contract signing protocol.
Link esterno al gruppo di ricerca: http://www.ai-lab.it
Giuseppe Colazzo (Università degli studi di bari)
"la fiducia quale presupposto degli scambi aziendali nella new economy"
"la fiducia quale presupposto degli scambi aziendali nella new economy"Giuseppe Colazzo (Università degli studi di bari)
"la fiducia quale presupposto degli scambi aziendali nella new economy"
(Relatore: Prof. M. Carrassi - Prof. S. Santovito).
In questo lavoro viene analizzato il ruolo assunto dai reati informatici e dal livello di sicurezza nei sistemi informatici nei confronti della fiducia del consumatore che diventa un presupposto fondamentale negli scambi che avvengono sul canale Internet. L'analisi viene focalizzata sul ruolo dell'informazione all'interno dei mercati (tecniche di brand management), sui nuovi canali di contrattazione telematica (social network, economia della conoscenza, tutela della privacy), sui meccanismi di pagamento e contrattazione dell'e-commerce, sui sistemi di sicurezza informatica e relative contromisure tecniche (crittografia, infrastrutture a chiave pubblica), sui reati informatici e sul sitema delle responsabilità su Internet. Vengono quindi evidenziati i punti deboli sui quali concentrare le iniziative legislative ed imprenditoriali al fine di supportare lo sviluppo del commercio elettronico.
"la fiducia quale presupposto degli scambi aziendali nella new economy"(Relatore: Prof. M. Carrassi - Prof. S. Santovito).
In questo lavoro viene analizzato il ruolo assunto dai reati informatici e dal livello di sicurezza nei sistemi informatici nei confronti della fiducia del consumatore che diventa un presupposto fondamentale negli scambi che avvengono sul canale Internet. L'analisi viene focalizzata sul ruolo dell'informazione all'interno dei mercati (tecniche di brand management), sui nuovi canali di contrattazione telematica (social network, economia della conoscenza, tutela della privacy), sui meccanismi di pagamento e contrattazione dell'e-commerce, sui sistemi di sicurezza informatica e relative contromisure tecniche (crittografia, infrastrutture a chiave pubblica), sui reati informatici e sul sitema delle responsabilità su Internet. Vengono quindi evidenziati i punti deboli sui quali concentrare le iniziative legislative ed imprenditoriali al fine di supportare lo sviluppo del commercio elettronico.
Jacopo Doria (Dipartimento di Ingegneria della Informazione, Politecnico di Milano)
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"Jacopo Doria (Dipartimento di Ingegneria della Informazione, Politecnico di Milano)
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"
(Relatore: Stefano Zanero).
Il mio lavoro è stato svolto in collaborazione con un collega, Riccardo Galbiati, e presso Khamsa, una società che si occupa di comunicazioni sicure. Il progetto ha avuto l’obiettivo di implementare lo standard SMIME in ambito mobile. Grazie alla tecnologia Java ME è stato possibile realizzare un componente che avesse come caratteristica principale l’interoperabilità e fosse rivolto anche ai dispositivi di fascia medio - bassa. Il lavoro è stato strutturato in fasi: per prima cosa abbiamo realizzato uno studio di fattibilità per tenere in considerazione i vincoli dell’ambito mobile; successivamente abbiamo condotto uno studio sul rapporto tra usabilità e sicurezza per evidenziare l’impatto che lo standard SMIME potrebbe avere su un client mail mobile; siamo poi passati alla fase di sviluppo realizzando due prototipi in grado di scambiarsi messaggi cifrati secondo tale standard; infine abbiamo condotto degli accurati test per valutare le performance del componente.
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"(Relatore: Stefano Zanero).
Il mio lavoro è stato svolto in collaborazione con un collega, Riccardo Galbiati, e presso Khamsa, una società che si occupa di comunicazioni sicure. Il progetto ha avuto l’obiettivo di implementare lo standard SMIME in ambito mobile. Grazie alla tecnologia Java ME è stato possibile realizzare un componente che avesse come caratteristica principale l’interoperabilità e fosse rivolto anche ai dispositivi di fascia medio - bassa. Il lavoro è stato strutturato in fasi: per prima cosa abbiamo realizzato uno studio di fattibilità per tenere in considerazione i vincoli dell’ambito mobile; successivamente abbiamo condotto uno studio sul rapporto tra usabilità e sicurezza per evidenziare l’impatto che lo standard SMIME potrebbe avere su un client mail mobile; siamo poi passati alla fase di sviluppo realizzando due prototipi in grado di scambiarsi messaggi cifrati secondo tale standard; infine abbiamo condotto degli accurati test per valutare le performance del componente.
Riccardo Galbiati (Dipartimento di elettronica e informazione - Politecnico di Milano)
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"Riccardo Galbiati (Dipartimento di elettronica e informazione - Politecnico di Milano)
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"
(Relatore: Stefano Zanero).
Il mio lavoro è stato svolto in collaborazione con un collega, Jacopo Doria, e presso Khamsa, una società che si occupa di comunicazioni sicure. Il progetto ha avuto l’obiettivo di implementare lo standard SMIME in ambito mobile. Grazie alla tecnologia Java ME è stato possibile realizzare un componente che avesse come caratteristica principale l’interoperabilità e fosse rivolto anche ai dispositivi di fascia medio - bassa. Il lavoro è stato strutturato in fasi: per prima cosa abbiamo realizzato uno studio di fattibilità per tenere in considerazione i vincoli dell’ambito mobile; successivamente abbiamo condotto uno studio sul rapporto tra usabilità e sicurezza per evidenziare l’impatto che lo standard SMIME potrebbe avere su un client mail mobile; siamo poi passati alla fase di sviluppo realizzando due prototipi in grado di scambiarsi messaggi cifrati secondo tale standard; infine abbiamo condotto degli accurati test per valutare le performance del componente.
"Progettazione e realizzazione di un componente crittografico per la gestione di email in ambito mobile"(Relatore: Stefano Zanero).
Il mio lavoro è stato svolto in collaborazione con un collega, Jacopo Doria, e presso Khamsa, una società che si occupa di comunicazioni sicure. Il progetto ha avuto l’obiettivo di implementare lo standard SMIME in ambito mobile. Grazie alla tecnologia Java ME è stato possibile realizzare un componente che avesse come caratteristica principale l’interoperabilità e fosse rivolto anche ai dispositivi di fascia medio - bassa. Il lavoro è stato strutturato in fasi: per prima cosa abbiamo realizzato uno studio di fattibilità per tenere in considerazione i vincoli dell’ambito mobile; successivamente abbiamo condotto uno studio sul rapporto tra usabilità e sicurezza per evidenziare l’impatto che lo standard SMIME potrebbe avere su un client mail mobile; siamo poi passati alla fase di sviluppo realizzando due prototipi in grado di scambiarsi messaggi cifrati secondo tale standard; infine abbiamo condotto degli accurati test per valutare le performance del componente.
Gianluca Ghettini (Dipartimento di Elettronica e Telecomunicazioni, Università degli Studi di Firenze )
"Studio e realizzazione su piattaforma Trusted Computing di un sistema RSA Identity-Based"
Link esterno al gruppo di ricerca: http://lart.det.unifi.it/
"Studio e realizzazione su piattaforma Trusted Computing di un sistema RSA Identity-Based"Link esterno al gruppo di ricerca: http://lart.det.unifi.it/
Gianluca Ghettini (Dipartimento di Elettronica e Telecomunicazioni, Università degli Studi di Firenze )
"Studio e realizzazione su piattaforma Trusted Computing di un sistema RSA Identity-Based"
(Relatore: Prof. Romano Fantacci).
La tesi propone una soluzione pratica all'ormai riconosciuto problema del certificato digitale come elemento per la sicurezza. Spesso capita che l'utente (persona o agente) venga posto nella condizione di decidere dell'autenticita' di un certificato, annullando la sicurezza di un intero sistema. Esiste da tempo (2001) un nuovo tipo di crittografia asimmetrica che non usa certificati, detto IBC (Identity Based Cryptography). Sebbene superiore sotto molti aspetti, non ha avuto una grande diffusione a causa della natura completamente diversa delle primitive crittografiche utilizzate: cio' comporta l'incompatibilita' con RSA e quindi con quasi tutti i protocolli attuali. La tesi propone finalmente un sistema IBC basato su RSA: la congiunzione e' resa possibile grazie all'utilizzo della tecnologia Trusted Computing, ormai ampiamente diffusa. La soluzione eredita tutti i vantaggi dell'IBC (scalabilita', niente certificati ne CA) e quelli ormai consolidati di RSA (affidabilita')
Link esterno al gruppo di ricerca: http://lart.det.unifi.it/
"Studio e realizzazione su piattaforma Trusted Computing di un sistema RSA Identity-Based"(Relatore: Prof. Romano Fantacci).
La tesi propone una soluzione pratica all'ormai riconosciuto problema del certificato digitale come elemento per la sicurezza. Spesso capita che l'utente (persona o agente) venga posto nella condizione di decidere dell'autenticita' di un certificato, annullando la sicurezza di un intero sistema. Esiste da tempo (2001) un nuovo tipo di crittografia asimmetrica che non usa certificati, detto IBC (Identity Based Cryptography). Sebbene superiore sotto molti aspetti, non ha avuto una grande diffusione a causa della natura completamente diversa delle primitive crittografiche utilizzate: cio' comporta l'incompatibilita' con RSA e quindi con quasi tutti i protocolli attuali. La tesi propone finalmente un sistema IBC basato su RSA: la congiunzione e' resa possibile grazie all'utilizzo della tecnologia Trusted Computing, ormai ampiamente diffusa. La soluzione eredita tutti i vantaggi dell'IBC (scalabilita', niente certificati ne CA) e quelli ormai consolidati di RSA (affidabilita')
Link esterno al gruppo di ricerca: http://lart.det.unifi.it/
Marco Riccardi (UNIVERSITÀ DEGLI STUDI DI MILANO - Facoltà di Scienze Matematiche, Fisiche e Naturali - Corso di Laurea in Sicurezza dei Sistemi e delle Reti Informatiche (Crema) )
"The Dorothy Project: inside the Storm - An automated platform for botnet analyses"
Link esterno alla tesi: http://www.honeynet.it/wp-content/uploads/Chapter_Docs/Dorothy/The_Dorothy_Project.pdf
Link esterno al gruppo di ricerca: http://www.honeynet.it
"The Dorothy Project: inside the Storm - An automated platform for botnet analyses"Link esterno alla tesi: http://www.honeynet.it/wp-content/uploads/Chapter_Docs/Dorothy/The_Dorothy_Project.pdf
Link esterno al gruppo di ricerca: http://www.honeynet.it
Marco Riccardi (UNIVERSITÀ DEGLI STUDI DI MILANO - Facoltà di Scienze Matematiche, Fisiche e Naturali - Corso di Laurea in Sicurezza dei Sistemi e delle Reti Informatiche (Crema) )
"The Dorothy Project: inside the Storm - An automated platform for botnet analyses"
(Relatore: Prof. Marco Cremonini).
The Dorothy project è un progetto che punta alla realizzazione di una piattaforma automatica per l’analisi delle botnet in tempo reale. Dorothy è il nome del software realizzato per adempiere a questo scopo. Il software, come tutto il progetto, è open-source, qualsiasi persona interessata potrà liberamente scaricare tutto il necessario per apportare il suo contributo al progetto. Uno dei punti forza di Dorothy è la visualizzazione dei dati acquisiti delle sue analisi attraverso una serie di grafici generati dinamicamente ogni 30 minuti. In questa maniera è possibile avere una panoramica grafica sulla situazione corrente dei dati processati da Dorothy. Generare una quadro completo riguardo alle analisi correnti è necessario per studiare le botnet in quanto si tratta di un fenomeno che muta le sua caratteristiche giornalmente in maniera imprevedibile. Nella preparazione di questa Tesi di Laurea il primo obiettivo è stato quello di studiare lo stato dell’Arte in materia, ed analizzare i risultati proposti dai vari autori. Successivamente a questo è stato possibile tracciare lo schema di una piattaforma ideale per l’analisi automatica delle botnet al quale è seguita la realizzazione di tali specifiche mediante la prima versione di Dorothy. Lo sviluppo di Dorothy è stato fatto seguendo i principi della programmazione modulare, esaltando qualità come semplicità, leggerezza, ed indipendenza di ogni sotto programma. Per questi motivi è stato scelto il linguaggio di scripting BASH, che offre elevate prestazioni, ed un’elevato livello di compatibilità. Inoltre risulta essere un’ottimo collante per la concatenazione di processi automatici eseguiti da altri software basati su piattaforme Unix. Come verrà mostrato nei risultati, Dorothy si è rilevata un’efficiente mezzo autonomo per l’analisi delle botnet, calcolando le risorse a sua disposizione durante il periodo di acquisizione dati/analisi. Il lavoro svolto in questa Tesi di Laurea sarà propedeutico alla fondazione del nuovo capitolo italiano ufficiale del progetto fondato da Lance Spitzner, The Honeynet Project.
Link esterno alla tesi: http://www.honeynet.it/wp-content/uploads/Chapter_Docs/Dorothy/The_Dorothy_Project.pdf
Link esterno al gruppo di ricerca: http://www.honeynet.it
"The Dorothy Project: inside the Storm - An automated platform for botnet analyses"(Relatore: Prof. Marco Cremonini).
The Dorothy project è un progetto che punta alla realizzazione di una piattaforma automatica per l’analisi delle botnet in tempo reale. Dorothy è il nome del software realizzato per adempiere a questo scopo. Il software, come tutto il progetto, è open-source, qualsiasi persona interessata potrà liberamente scaricare tutto il necessario per apportare il suo contributo al progetto. Uno dei punti forza di Dorothy è la visualizzazione dei dati acquisiti delle sue analisi attraverso una serie di grafici generati dinamicamente ogni 30 minuti. In questa maniera è possibile avere una panoramica grafica sulla situazione corrente dei dati processati da Dorothy. Generare una quadro completo riguardo alle analisi correnti è necessario per studiare le botnet in quanto si tratta di un fenomeno che muta le sua caratteristiche giornalmente in maniera imprevedibile. Nella preparazione di questa Tesi di Laurea il primo obiettivo è stato quello di studiare lo stato dell’Arte in materia, ed analizzare i risultati proposti dai vari autori. Successivamente a questo è stato possibile tracciare lo schema di una piattaforma ideale per l’analisi automatica delle botnet al quale è seguita la realizzazione di tali specifiche mediante la prima versione di Dorothy. Lo sviluppo di Dorothy è stato fatto seguendo i principi della programmazione modulare, esaltando qualità come semplicità, leggerezza, ed indipendenza di ogni sotto programma. Per questi motivi è stato scelto il linguaggio di scripting BASH, che offre elevate prestazioni, ed un’elevato livello di compatibilità. Inoltre risulta essere un’ottimo collante per la concatenazione di processi automatici eseguiti da altri software basati su piattaforme Unix. Come verrà mostrato nei risultati, Dorothy si è rilevata un’efficiente mezzo autonomo per l’analisi delle botnet, calcolando le risorse a sua disposizione durante il periodo di acquisizione dati/analisi. Il lavoro svolto in questa Tesi di Laurea sarà propedeutico alla fondazione del nuovo capitolo italiano ufficiale del progetto fondato da Lance Spitzner, The Honeynet Project.
Link esterno alla tesi: http://www.honeynet.it/wp-content/uploads/Chapter_Docs/Dorothy/The_Dorothy_Project.pdf
Link esterno al gruppo di ricerca: http://www.honeynet.it
Cosimo Pasquale Ricchiuto (Politecnico di Torino)
"Tirocinio presso SSB Progetti S.r.l.- Analisi e integrazione del software OSSIM "
Link esterno alla tesi: http://pescolusevacanze.altervista.org/monografia_cpr.pdf
"Tirocinio presso SSB Progetti S.r.l.- Analisi e integrazione del software OSSIM "Link esterno alla tesi: http://pescolusevacanze.altervista.org/monografia_cpr.pdf
Cosimo Pasquale Ricchiuto (Politecnico di Torino)
"Tirocinio presso SSB Progetti S.r.l.- Analisi e integrazione del software OSSIM "
(Relatore: Massimo Violante).
Questa tesi ha l’obiettivo principale di fornire una guida all’utilizzo di Ossim, senza tralasciare le dovute premesse teoriche sia riguardo la sicurezza di rete, sia riguardo l’architettura del pacchetto software. La monografia raccoglie quella che è stata l'esperienza di tirocinio svolta presso l'azienda SSB Progetti s.r.l. di Torino.
Link esterno alla tesi: http://pescolusevacanze.altervista.org/monografia_cpr.pdf
"Tirocinio presso SSB Progetti S.r.l.- Analisi e integrazione del software OSSIM "(Relatore: Massimo Violante).
Questa tesi ha l’obiettivo principale di fornire una guida all’utilizzo di Ossim, senza tralasciare le dovute premesse teoriche sia riguardo la sicurezza di rete, sia riguardo l’architettura del pacchetto software. La monografia raccoglie quella che è stata l'esperienza di tirocinio svolta presso l'azienda SSB Progetti s.r.l. di Torino.
Link esterno alla tesi: http://pescolusevacanze.altervista.org/monografia_cpr.pdf
Matteo Signorini (Università degli studi di Roma "Sapienza")
"Aspetti di sicurezza in macchine virtuali:Realizzazione di un prototipo di protezione della integrità del kernel linux su macchina guest."
"Aspetti di sicurezza in macchine virtuali:Realizzazione di un prototipo di protezione della integrità del kernel linux su macchina guest."Matteo Signorini (Università degli studi di Roma "Sapienza")
"Aspetti di sicurezza in macchine virtuali:Realizzazione di un prototipo di protezione della integrità del kernel linux su macchina guest."
(Relatore: Roberto Di Pietro).
In questa tesi viene proposto un originale sistema di protezione dell’integrità del kernel linux su macchine virtuali e ne viene descritta l'implementazione realizzata. Tale sistema, denominato KVMLSP (KVM Linux Security Project) gode, diversamente dalle soluzioni in letteratura, del vantaggio di risiedere interamente lato host, risultando così più isolato e trasparente al guest. Il monitoraggio eseguito da kvmlsp è di tipo asincrono, in grado di rilevare gli attacchi ad oggi conosciuti e con buone potenzialità di rilevare tecniche di attacco ancora sconosciute. Ciò è dovuto ad un sistema di protezione indipendente dalla tecnica di attacco ed incentrato sulle alterazioni provocate al kernel guest. Kvmlsp è altamente configurabile e portabile con un impatto minimo sulle prestazioni del guest. Gli sviluppi futuri sono mirati alla possibilità di integrare il controllo asincrono con un controllo sincrono al fine di aumentare la robustezza e l'efficacia dell'intero sistema di controllo.
"Aspetti di sicurezza in macchine virtuali:Realizzazione di un prototipo di protezione della integrità del kernel linux su macchina guest."(Relatore: Roberto Di Pietro).
In questa tesi viene proposto un originale sistema di protezione dell’integrità del kernel linux su macchine virtuali e ne viene descritta l'implementazione realizzata. Tale sistema, denominato KVMLSP (KVM Linux Security Project) gode, diversamente dalle soluzioni in letteratura, del vantaggio di risiedere interamente lato host, risultando così più isolato e trasparente al guest. Il monitoraggio eseguito da kvmlsp è di tipo asincrono, in grado di rilevare gli attacchi ad oggi conosciuti e con buone potenzialità di rilevare tecniche di attacco ancora sconosciute. Ciò è dovuto ad un sistema di protezione indipendente dalla tecnica di attacco ed incentrato sulle alterazioni provocate al kernel guest. Kvmlsp è altamente configurabile e portabile con un impatto minimo sulle prestazioni del guest. Gli sviluppi futuri sono mirati alla possibilità di integrare il controllo asincrono con un controllo sincrono al fine di aumentare la robustezza e l'efficacia dell'intero sistema di controllo.
Daniele Spaccini (Dipartimento di Informatica - Universita' La Sapienza di Roma)
"Definizione, analisi ed implementazione di meccanismi di autenticazione per dispositivi con risorse limitate"
"Definizione, analisi ed implementazione di meccanismi di autenticazione per dispositivi con risorse limitate"Daniele Spaccini (Dipartimento di Informatica - Universita' La Sapienza di Roma)
"Definizione, analisi ed implementazione di meccanismi di autenticazione per dispositivi con risorse limitate"
(Relatore: Roberto Di Pietro).
Uno dei temi maggiormente affrontati per la sicurezza delle comunicazioni broadcast è l'autenticazione della sorgente: ogni ricevente infatti deve essere in grado di poter verificare l'origine dei dati. Questa tesi ha diversi contributi: inizialmente verranno presentati 3 differenti algoritmi sviluppati recentemente per l'autenticazione della sorgente su reti multicast: PARM, PEAC ed ALPS. Essi costituiscono attualmente lo stato dell'arte per quanto riguarda l'autenticazione su reti multicast. Dopo ciascuna presentazione ne verrà discussa l'implementazione, necessaria per effettuare il confronto tra gli algoritmi dal punto di vista simulativo. Verranno poi introdotti i contributi che sono stati apportati all'algoritmo PEAC per migliorarne la sicurezza e l'efficienza. Infine, verranno confrontati gli algoritmi proposti, in base a diversi parametri di sicurezza, per determinarne le differenze. I test analitici e sperimentali effettuati tra gli algoritmi definiti "lo stato dell'arte" ed i protocolli proposti, dimostrano che questi ultimi costituiscono buone alternative alle soluzioni attuali. Per quanto riguarda la resilienza agli attacchi, nella tesi si assumerà che un attaccante si comporti in accordo al modello proposto da Dolev-Yao. Quindi esso potrà acquisire, inserire, modificare e/o scartare i pacchetti trasmessi dalla sorgente. In particolare, un attaccante potrà: (1) intercettare ed immagazzinare ogni messaggio; (2) scartare messaggi da lui selezionati; (3) introdurre messaggi da lui forgiati all'interno del canale di comunicazione. Questo modello è stato anche utilizzato per implementare un attacco di tipo brute-force ai nuovi algoritmi presentati.
"Definizione, analisi ed implementazione di meccanismi di autenticazione per dispositivi con risorse limitate"(Relatore: Roberto Di Pietro).
Uno dei temi maggiormente affrontati per la sicurezza delle comunicazioni broadcast è l'autenticazione della sorgente: ogni ricevente infatti deve essere in grado di poter verificare l'origine dei dati. Questa tesi ha diversi contributi: inizialmente verranno presentati 3 differenti algoritmi sviluppati recentemente per l'autenticazione della sorgente su reti multicast: PARM, PEAC ed ALPS. Essi costituiscono attualmente lo stato dell'arte per quanto riguarda l'autenticazione su reti multicast. Dopo ciascuna presentazione ne verrà discussa l'implementazione, necessaria per effettuare il confronto tra gli algoritmi dal punto di vista simulativo. Verranno poi introdotti i contributi che sono stati apportati all'algoritmo PEAC per migliorarne la sicurezza e l'efficienza. Infine, verranno confrontati gli algoritmi proposti, in base a diversi parametri di sicurezza, per determinarne le differenze. I test analitici e sperimentali effettuati tra gli algoritmi definiti "lo stato dell'arte" ed i protocolli proposti, dimostrano che questi ultimi costituiscono buone alternative alle soluzioni attuali. Per quanto riguarda la resilienza agli attacchi, nella tesi si assumerà che un attaccante si comporti in accordo al modello proposto da Dolev-Yao. Quindi esso potrà acquisire, inserire, modificare e/o scartare i pacchetti trasmessi dalla sorgente. In particolare, un attaccante potrà: (1) intercettare ed immagazzinare ogni messaggio; (2) scartare messaggi da lui selezionati; (3) introdurre messaggi da lui forgiati all'interno del canale di comunicazione. Questo modello è stato anche utilizzato per implementare un attacco di tipo brute-force ai nuovi algoritmi presentati.
Paolo Tornari (Dipartimento INFOCOM - Sapienza Università di Roma)
"Progetto e sviluppo di un algoritmo di ottimizzazione della lista di policy di sicurezza di packet filtering device, adattivo al traffico"
"Progetto e sviluppo di un algoritmo di ottimizzazione della lista di policy di sicurezza di packet filtering device, adattivo al traffico"Paolo Tornari (Dipartimento INFOCOM - Sapienza Università di Roma)
"Progetto e sviluppo di un algoritmo di ottimizzazione della lista di policy di sicurezza di packet filtering device, adattivo al traffico"
(Relatore: Prof. Baiocchi Andrea).
Questa tesi è il risultato di un'attività svolta presso Elsag Datamat S.p.A. (una società Finmeccanica) nell'ambito di un progetto sviluppato in collaborazione con il Dipartimento INFOCOM della Sapienza, Università di Roma. L'attività svolta nel periodo di tesi ha riguardato l'ideazione e lo sviluppo di un algoritmo di ottimizzazione, conflict-free, delle policy di sicurezza che definiscono il comportamento dei firewalls. L’ottimizzazione è intesa come processo che conduce alla creazione di una nuova lista di regole che, implementata nel dispositivo analizzato, porta alla minimizzazione del tempo di processamento medio dei pacchetti e quindi ad un aumento del throughput del dispositivo stesso. Il tool fornisce un meccanismo di reazione ad attacchi di interruzione del servizio, sia locali (DoS) che distribuiti (DDoS), analizzando in tempo reale il traffico IP processato dai dispositivi di packet filtering ed agendo in controreazione sugli stessi.
"Progetto e sviluppo di un algoritmo di ottimizzazione della lista di policy di sicurezza di packet filtering device, adattivo al traffico"(Relatore: Prof. Baiocchi Andrea).
Questa tesi è il risultato di un'attività svolta presso Elsag Datamat S.p.A. (una società Finmeccanica) nell'ambito di un progetto sviluppato in collaborazione con il Dipartimento INFOCOM della Sapienza, Università di Roma. L'attività svolta nel periodo di tesi ha riguardato l'ideazione e lo sviluppo di un algoritmo di ottimizzazione, conflict-free, delle policy di sicurezza che definiscono il comportamento dei firewalls. L’ottimizzazione è intesa come processo che conduce alla creazione di una nuova lista di regole che, implementata nel dispositivo analizzato, porta alla minimizzazione del tempo di processamento medio dei pacchetti e quindi ad un aumento del throughput del dispositivo stesso. Il tool fornisce un meccanismo di reazione ad attacchi di interruzione del servizio, sia locali (DoS) che distribuiti (DDoS), analizzando in tempo reale il traffico IP processato dai dispositivi di packet filtering ed agendo in controreazione sugli stessi.
Massimo Venuto (DTI Crema/Università degli Studi di Milano)
"LA CRITTOGRAFIA ELLITTICA :IMPLEMENTAZIONE E PERFORMANCE NELLE TRANSAZIONI WEB SICURE"
Link esterno alla tesi: http://www.dti.unimi.it/citrini/Tesi/tesiVenuto.pdf
"LA CRITTOGRAFIA ELLITTICA :IMPLEMENTAZIONE E PERFORMANCE NELLE TRANSAZIONI WEB SICURE"Link esterno alla tesi: http://www.dti.unimi.it/citrini/Tesi/tesiVenuto.pdf
Massimo Venuto (DTI Crema/Università degli Studi di Milano)
"LA CRITTOGRAFIA ELLITTICA :IMPLEMENTAZIONE E PERFORMANCE NELLE TRANSAZIONI WEB SICURE"
(Relatore: Prof.ssa Laura Citrini).
Il progetto intendeva illustrare possibilità, modalità e vantaggi dell’utilizzo della crittografia ellittica come tecnologia per garantire transazioni web sicure. Il lavoro è stato articolato in due sezioni: una teorica e una pratica. La parte teorica evidenzia le strutture algebriche sulle quali si fonda la crittografia ellittica, inoltre vengono indicati i principali standard crittografici e viene illustrata la non trattabilità del problema del logaritmo discreto. La parte pratica è incentrata sulla realizzazione in ambiente open source di una piattaforma di testing per misurare l’efficacia garantita dalla crittografia ellittica rispetto ad altri i protocolli di sicurezza. Dopo aver descritto le caratteristiche di questa implementazione vengono illustrati i test condotti. Da questi si evince come la crittografia ellittica necessiti di un minore bisogno computazionale, a parità di sicurezza, rispetto all’algoritmo RSA. Tale dato induce a ritenere che la crittografia ellittica possa essere una tecnologia particolarmente adatta per realizzazioni su dispositivi quali palmari, smartphone, etc. e in effetti si stanno realizzando microprocessori dedicati ad alta velocità ASIC basati sulla crittografia ellittica per realizzare VPN e Web Server ottimizzati per il B2B. Il progetto si chiude con un rapido accenno alle prospettive future di questo settore di studi, in particolare alle nuove scoperte teoriche di cubiche non di Weierstrass che potrebbero divenire base per strutture algebriche ancor più efficienti.
Link esterno alla tesi: http://www.dti.unimi.it/citrini/Tesi/tesiVenuto.pdf
"LA CRITTOGRAFIA ELLITTICA :IMPLEMENTAZIONE E PERFORMANCE NELLE TRANSAZIONI WEB SICURE"(Relatore: Prof.ssa Laura Citrini).
Il progetto intendeva illustrare possibilità, modalità e vantaggi dell’utilizzo della crittografia ellittica come tecnologia per garantire transazioni web sicure. Il lavoro è stato articolato in due sezioni: una teorica e una pratica. La parte teorica evidenzia le strutture algebriche sulle quali si fonda la crittografia ellittica, inoltre vengono indicati i principali standard crittografici e viene illustrata la non trattabilità del problema del logaritmo discreto. La parte pratica è incentrata sulla realizzazione in ambiente open source di una piattaforma di testing per misurare l’efficacia garantita dalla crittografia ellittica rispetto ad altri i protocolli di sicurezza. Dopo aver descritto le caratteristiche di questa implementazione vengono illustrati i test condotti. Da questi si evince come la crittografia ellittica necessiti di un minore bisogno computazionale, a parità di sicurezza, rispetto all’algoritmo RSA. Tale dato induce a ritenere che la crittografia ellittica possa essere una tecnologia particolarmente adatta per realizzazioni su dispositivi quali palmari, smartphone, etc. e in effetti si stanno realizzando microprocessori dedicati ad alta velocità ASIC basati sulla crittografia ellittica per realizzare VPN e Web Server ottimizzati per il B2B. Il progetto si chiude con un rapido accenno alle prospettive future di questo settore di studi, in particolare alle nuove scoperte teoriche di cubiche non di Weierstrass che potrebbero divenire base per strutture algebriche ancor più efficienti.
Link esterno alla tesi: http://www.dti.unimi.it/citrini/Tesi/tesiVenuto.pdf
Luca Zanetti (Dipartimento di Informatica, Facoltà di Scienze Matematiche Fisiche e Naturali, Università degli Studi di Verona)
"Integrazione di tecniche SMT in un sistema di verifica per applicazioni orientate ai servizi"
Link esterno al gruppo di ricerca: http://www.avantssar.eu/
"Integrazione di tecniche SMT in un sistema di verifica per applicazioni orientate ai servizi"Link esterno al gruppo di ricerca: http://www.avantssar.eu/
Luca Zanetti (Dipartimento di Informatica, Facoltà di Scienze Matematiche Fisiche e Naturali, Università degli Studi di Verona)
"Integrazione di tecniche SMT in un sistema di verifica per applicazioni orientate ai servizi"
(Relatore: Luca Viganò).
Nello sviluppo di Architetture Orientate ai Servizi (SOA) nasce il problema della sicurezza dei servizi, specialmente quelli operanti in contesti delicati come l'E-commerce e l'E-governance. La progettazione e la verifica di tali componenti sono talmente complicate che spesso gravi vulnerabilità rimangono presenti anche dopo estensiva applicazione delle tradizionali tecniche di verifica, quali ad es. l'analisi manuale ed il testing. Ne è prova il fatto che gravi vulnerabilità sono state scoperte nei più noti protocolli web (quali SAML SSO, MS Passport/CardSpace) anche anni dopo la loro pubblicazione, la loro implementazione, o anche il loro utilizzo sul campo. Data la rilevanza applicativa delle applicazioni SOA, lo sviluppo di tecniche per l'analisi automatica della loro sicurezza ha ricevuto e riceve un impulso considerevole dalla comunità scientifica internazionale. Sono state proposte un'ampia varietà di tecniche basate, ad es., su Contraint Solving e il Model Checking simbolico. Sfortunatamente, queste tecniche di analisi formale non tengono in considerazione l'architettura delle applicazioni SOA in cui la sicurezza gioca un ruolo cruciale. Infatti, un'applicazione SOA (come ad esempio un web service) è di solito strutturata su due livelli: il primo, Workflow, che si occupa dei flussi di controllo e di dati, il secondo, opzionale, che descrive le Policy. Al fine di rendere più semplice la formalizzazione di queste applicazioni, c'è il bisogno di sviluppare tecniche di specifica e di analisi in grado di sfruttare questa struttura. Esistono due strade per affrontare il problema: l'utilizzo di tool dedicati o la (ri)modulazione di tool esistenti. E' stata scelta la seconda strada con l'utilizzo degli SMT solver. Il contributo fondamentale di questa tesi è stato quello di analizzare le interazioni tra i due livelli e, dopo lo studio di un framework recentemente proposto in letteratura, di identificare delle procedure per automatizzare l'analisi e di implementarle. Si è quindi progettata e realizzata un'applicazione Java per la validazione dei servizi, WSSMT (Web Service Solver Modulo Theory). WSSMT è stato testato con un caso di studio preso dal progetto europeo AVANTSSAR e ha permesso di correggerne degli errori nella specifica formale e di validarlo.
Link esterno al gruppo di ricerca: http://www.avantssar.eu/
"Integrazione di tecniche SMT in un sistema di verifica per applicazioni orientate ai servizi"(Relatore: Luca Viganò).
Nello sviluppo di Architetture Orientate ai Servizi (SOA) nasce il problema della sicurezza dei servizi, specialmente quelli operanti in contesti delicati come l'E-commerce e l'E-governance. La progettazione e la verifica di tali componenti sono talmente complicate che spesso gravi vulnerabilità rimangono presenti anche dopo estensiva applicazione delle tradizionali tecniche di verifica, quali ad es. l'analisi manuale ed il testing. Ne è prova il fatto che gravi vulnerabilità sono state scoperte nei più noti protocolli web (quali SAML SSO, MS Passport/CardSpace) anche anni dopo la loro pubblicazione, la loro implementazione, o anche il loro utilizzo sul campo. Data la rilevanza applicativa delle applicazioni SOA, lo sviluppo di tecniche per l'analisi automatica della loro sicurezza ha ricevuto e riceve un impulso considerevole dalla comunità scientifica internazionale. Sono state proposte un'ampia varietà di tecniche basate, ad es., su Contraint Solving e il Model Checking simbolico. Sfortunatamente, queste tecniche di analisi formale non tengono in considerazione l'architettura delle applicazioni SOA in cui la sicurezza gioca un ruolo cruciale. Infatti, un'applicazione SOA (come ad esempio un web service) è di solito strutturata su due livelli: il primo, Workflow, che si occupa dei flussi di controllo e di dati, il secondo, opzionale, che descrive le Policy. Al fine di rendere più semplice la formalizzazione di queste applicazioni, c'è il bisogno di sviluppare tecniche di specifica e di analisi in grado di sfruttare questa struttura. Esistono due strade per affrontare il problema: l'utilizzo di tool dedicati o la (ri)modulazione di tool esistenti. E' stata scelta la seconda strada con l'utilizzo degli SMT solver. Il contributo fondamentale di questa tesi è stato quello di analizzare le interazioni tra i due livelli e, dopo lo studio di un framework recentemente proposto in letteratura, di identificare delle procedure per automatizzare l'analisi e di implementarle. Si è quindi progettata e realizzata un'applicazione Java per la validazione dei servizi, WSSMT (Web Service Solver Modulo Theory). WSSMT è stato testato con un caso di studio preso dal progetto europeo AVANTSSAR e ha permesso di correggerne degli errori nella specifica formale e di validarlo.
Link esterno al gruppo di ricerca: http://www.avantssar.eu/
BACHECA TESI EDIZIONI PASSATE
Edizione 2022Edizione 2022
Edizione 2021
Edizione 2020
Edizione 2019
Edizione 2018
Edizione 2017
Edizione 2016
Edizione 2015
Edizione 2014
Edizione 2013
Edizione 2012
Edizione 2011
Edizione 2010
Edizione 2009
Edizione 2008
Edizione 2007
