Laboratori avanzati e Tesi di laurea

Qui descrivo alcuni argomenti generali di mio interesse, su cui è possibile svolgere dei laboratori avanzati o tesi di laurea (triennale o specialistica). Se qualche argomento è di vostro interesse, possiamo fissare un appuntamento per discutere un progetto preciso (la cui disponibilità varia nel tempo).

Regole generali:

  1. I progetti vengono assegnati su base "first-come first-served, con time-out": quando un progetto viene assegnato, si fissa anche una data di consegna (tipicamente dai 2 ai 4 mesi, in proporzione alla difficoltà del progetto); se tale data non è rispettata, l'assegnazione decade e il progetto può essere assegnato ad altri studenti.
  2. In generale, tutti i progetti di laboratorio avanzato possono "evolvere" in una tesi di laurea (triennale o specialistica). Tuttavia il valore in termini di punti (e di conseguenza anche l'impegno necessario) di tali tesi è assai variabile. Pertanto il tipo di progetto che viene assegnato dipende anche dall'eventuale evoluzione dello stesso in una tesi di laurea.
  3. I laboratori avanzati comprendono sempre una rilevante parte di programmazione, anche se non necessariamente in linguaggi tradizionali. Questo vincolo non vale per le tesi di laurea, che, in assenza di parte pratica, possono essere "puramente teoriche" o "compilative".
  4. Tutti i progetti devono essere corredati da una relazione scritta.
  5. In generale, il codice sviluppato viene reso disponibile sotto una licenza open source su questo sito (vedi elenco a lato), per permettere eventuali sviluppi, miglioramenti ed applicazioni ad altre persone interessate.

Potete farvi un'idea degli argomenti anche dall'elenco dei progetti (qui a fianco), e dall'elenco delle ultime tesi di cui sono stato relatore, che è reperibile online, impostando "miculan" nel campo "relatore".

Modelli grafici di sistemi distribuiti e mobili

Recentemente, il nostro gruppo di ricerca sta studiando formalismi grafici per rappresentare sistemi distribuiti e mobili (come p.e., reti di calcolatori, processi, thread, etc). In sintesi, lo stato di un sistema mobile-concorrente può essere descritto come una particolare struttura grafica dove vengono rappresentate contemporaneamente la struttura della rete e le connessioni tra i vari nodi. Tale stato evolve secondo un insieme di regole di riscrittura grafiche.

Il nostro gruppo di ricerca ha avviato una implementazione di questo formalismo grafico; sono già state realizzate le strutture dati base, con alcune operazioni fondamentali, una interfaccia testuale (compilatore e decompilatore) e un visualizzatore grafico. Su questa base ci sono molti possibili sviluppi per laboratori avanzati: implementare una interfacce grafiche "mouse-oriented", implementare funzionalità per ora descritte solo sulla carta, sviluppare specifiche applicazioni, testing…

È richiesta una certa attitudine alla programmazione, meglio se funzionale (ma non necessariamente).

Logiche di Hoare per thread concorrenti in Isabelle

Recentemente è stata introdotta una nuova famiglia di Logiche di Hoare per la verifica di programmi paralleli, più agevoli e flessibili dei metodi di Owiki-Gries, e alternativi al rely-guarantee. In particolare abbiamo sviluppato un modello semantico, e la sua logica di Hoare, corrispondente ai thread dinamici con eccezioni, conforme al modello Posix implementato in linguaggi comuni come C, Java, etc.

In questo progetto si propone di continuare la ricerca in questa direzione, ad esempio lavorando sull'implementazione della logica di Hoare nel proof assistant Isabelle/HOL, o sviluppando semplici esempi di applicazione di tale logica.

È preferibile aver seguito il corso di Metodi Formali per l'Informatica 1, e conoscere le basi di Logica.

Formalizzazione di protocolli e sistemi concorrenti

Protocolli e sistemi concorrenti possono essere formalizzati anche usando formalismi "logici", come ad esempio Isabelle, Coq, e il recente CELF.

In particolare, si vuole studiare l'applicazione di quest'ultimo formalismo a protocolli di sicurezza, allo scopo di verificare formalmente proprietà di sicurezza di tali protocolli.

È richiesta una certa attitudine alla programmazione, possibilmente logico-funzionale, e qualche rudimento di logica.

Verifica automatica di protocolli di sicurezza

In anni recenti sono stati sviluppati diversi tool per la verifica automatica di proprietà di protocolli di sicurezza. Due esempi molto interessanti sono AVISPA e ProVerif.

Si propone di utilizzare questi strumenti per la verifica di proprietà di qualche protocollo; questo consiste nel rappresentare un protocollo nel formalismo proprio di uno di questi tool, e di impiegare il tool per la verifica delle proprietà rilevanti. Ad esempio, in un recente laboratorio abbiamo formalizzato il protocollo di single-sign in di Google, verificando l'esistenza del bug recentemente scoperto.

È consigliata una minima conoscenza dei linguaggi logici.

Utilizzo di smartcard per l'autenticazione forte presso siti web

La Regione FVG, come altre regioni italiane, ha distribuito a tutti i cittadini del FVG una tessera contenente una chiave privata RSA, e il relativo certificato, abilitata all'autenticazione forte. Al momento si può impiegare tale tessera per autenticarsi solo presso il sito web della regione, ma nulla vieta di utilizzare tale tessera presso altri siti; infatti, in un laboratorio precedente abbiamo sviluppato una versione di OpenCMS (un CMS che gira sotto TomCat) a cui ci si autentica usando tale smartcard.

Si vuole implementare questo meccanismo anche per siti web senza application servers, ad esempio quelli basati su linguaggi di scripting semplici come PHP o Python. Un'altra interessante possibilità è di studiare l'uso della smartcard all'interno del protocollo di single-sign on SAML, che, come indicato dallo CNIPA, dovrebbe diventare lo standard ufficiale per l'inte(g)razione tra pubbliche amministrazioni, cittadini e aziende.

È richiesta un po' di dimestichezza con Apache, e di qualche linguaggio di programmazione server-side (PHP, Python…), per configurare e produrre un sistema di prova. E di possedere la smartcard regionale e relativo lettore USB, ovviamente.

Utilizzo di smartcard per l'autenticazione su workstation

(Collegato al discorso precedente) Sempre usando la smartcard regionale, si vuole implementarne l'utilizzo per il login su PC / Mac. Più precisamente, si vuole definire chiaramente come integrare l'autenticazione mediante smartcard regionale nel processo di autenticazione e login su una workstation. Per le macchine Unix/Linux tale integrazione è già stata realizzata in un laboratorio precedente, sviluppando un opportuno plugin di PAM. Rimane da fare lo stesso lavoro per le macchine Windows e Mac OS X.

È richiesta un po' di dimestichezza con l'amministrazione del sistema operativo in esame, ed eventualmente del linguaggio C (se dovesse essere necessario mettere mano ai plugin). E di possedere la smartcard regionale e relativo lettore USB, ovviamente.

Utilizzo di smartcard per la firma e i timbri digitali

(Collegato al discorso precedente) Sempre usando la smartcard regionale, si vuole implementare tecniche di timbri digitali, ossia meccanismi di autenticazione di documenti stampati. Un modo che viene spesso usato (p.e. nei documenti dell'ACI e del PRA) è di aggiungere un codice a barre bidimensionale contenente l'informazione crittografica necessaria alla verifica del documento. Questa aggiunta può essere realizzato "a valle" del documento (p.e. aggiungere il timbro ad un PDF o altro formato riconosciuto legalmente), o "a monte", ossia nel momento in cui il documento viene prodotto. Con questo laboratorio si vuole implementare uno dei due, anche se entrambi gli approcci sono validi e hanno utilizzi diversi.

È richiesta un po' di dimestichezza con la programmazione C/Java. È consigliato, ma non strettamente necessario, possedere la smartcard regionale e relativo lettore USB.