RICERCA ITALIANA     

Programma di ricerca

SOFT - Tecniche formali orientate alla sicurezza

Università di riferimento

Università "Ca' Foscari" di VENEZIA - INFORMATICA - ()

Responsabile dell'Unità di ricerca

Riccardo Focardi

Descrizione

L'unità di Venezia focalizzerà la propria attività sulle linee di ricerca descritte nel seguito. Per ogni linea di ricerca vengono indicati i work-package (WP) del progetto nazionale all'interno dei quali tale ricerca verrà sviluppata.


VE1 - Analisi di protocolli di autenticazione tramite interpretazione astratta e semantiche causali (WP1 e WP4)

L'analisi di protocolli crittografici a livello di linguaggio è strettamente legata alla comprensione di come i vari messaggi cifrati scambiati dalle entità che eseguono il protocollo contribuiscono al raggiungimento delle proprietà di sicurezza attese. Si vuole infatti giudicare la correttezza del protocollo osservandone solamente la sintassi.
In [BCFM07] abbiamo iniziato ad estendere l'approccio basato sui tipi proposto in [BFM07], in modo da separare la parte di interpretazione dei messaggi cifrati dalla parte di analisi. In particolare, i messaggi cifrati vengono univocamente interpretati come sfide o risposte su un calcolo privo di crittografia, la cui semantica tiene conto della segretezza o integrità di tali messaggi. La correttezza del protocollo è a questo punto giudicata in base alla presenza delle necessarie sfide e risposte a prescindere dalla specifica realizzazione crittografica.
Intendiamo portare avanti questo filone di ricerca lavorando su due fronti:
(i) siamo interessati a formalizzare l'astrazione della crittografia sopra menzionata in termini più standard di interpretazione astratta. Questo permetterà di dimostrare risultati generali sulle astrazioni ed avere in modo automatico risultati sulla preservazione delle proprietà di sicurezza tra il calcolo concreto e quello astratto;
(ii) vogliamo dare una nuova semantica causale ai protocolli crittografici, basata su proved transition systems. Tale semantica potrebbe tracciare in modo esplicito la causalità tra sfide, risposte, inizio e fine del protocollo, permettendo di osservare la relazione di causa ed effetto tra la conclusione del protocollo, e quindi l'autenticazione, e la corrispettiva esecuzione del protocollo da parte dell'entità da autenticare. Intendiamo confrontarci con il modello causale ad-hoc da noi proposto in [BCM07].
Questa ricerca darà una migliore comprensione della logica sottostante i diversi protocolli crittografici, una chiara separazione della logica del protocollo dalla sua effettiva implementazione crittografica con conseguente possibilità di integrare all'interno di un linguaggio di programmazione librerie per l'autenticazione sfida-risposta la cui realizzazione crittografica è effettuata dal compilatore in modo trasparente all'utente (vedere anche VE2).

Risultati attesi:

Primo anno
- definizione di un'interpretazione astratta di protocolli crittografici;
- studio di differenti astrazioni e teoremi sulla composizioni delle astrazioni;
Secondo anno
- definizione di una nuova semantica causale, basata su proved transition systems, per tracciare la causalità degli eventi di autenticazione;
- studio di tecniche di analisi e verifica automatica su tale semantica astratta;
- confronto con tecniche esistenti basate su tipi ed effetti e su semantiche causali ad-hoc.


VE2 - Information Flow security di applicazioni distribuite con crittografia (WP2)

Le moderne applicazioni e servizi su rete sono sempre più complessi ed articolati e necessitano di sempre maggiore flessibilità nella programmazione e nella realizzazione di requisiti di sicurezza. L'uso di protocolli preconfezionati a livello di trasporto (come ad esempio SSL) può diventare limitativo e c'è la tendenza a "riprogrammare" i protocolli crittografici a livello applicazione, come accade ad esempio nei servizi Web (e.g., [OASIS]). Questa prassi, oltre a presentare evidenti rischi di introduzione di nuovi errori, rende ancora più complicata l'analisi della sicurezza del codice come evidenziato in [AS05]. Un'applicazione distribuita diviene infatti, dal punto di vista della sicurezza, un insieme di politiche locali connesse da scambi di messaggi cifrati. Se però il programmatore può fare uso incontrollato della crittografia, questa connessione tra le varie parti può creare problemi di sicurezza anche se localmente i vari programmi sono considerati sicuri.
Queste problematiche sono state affrontate, in letteratura, a livello di calcoli di processi, in cui gli unici eventi rilevanti sono l'invio e la ricezione di messaggi. D'altra parte, esiste una approfondita letteratura sullo studio e l'analisi della sicurezza su linguaggi. Un recente lavoro [AHS06] fa un primo passo di integrazione dei due approcci, definendo un semplice linguaggio imperativo con primitive di comunicazione crittografiche, e studiando come una particolare forma di Non-Interferenza possa essere preservata in applicazioni distribuite.
Intendiamo lavorare su due fronti: (i) studieremo estensioni dei risultati di [AHS06] a forme di interferenza più forti (scheduler-independent) e a proprietà diverse, come l'autenticazione, sfruttando sistemi di tipi dinamici nello stile di [BFM07]; (ii) studieremo primitive astratte di comunicazione che permettano di rendere la programmazione il più possibile indipendente dalla realizzazione crittografica. L'idea di fondo è di specificare la proprietà desiderata sulla comunicazione senza indicare uno specifico protocollo crittografico: sarà cura del compilatore o della libreria di risolvere opportunamente le richieste di sicurezza da parte delle applicazioni.
Studiare proprietà dei protocolli e dei programmi in unico framework chiarificherà le relazioni tra le proprietà definite nei due diversi contesti e permetterà di definire librerie per lo sviluppo di applicazioni distribuite. Si lavorerà nella direzione di garantire al programmatore un buon livello di astrazione e trasparenza rispetto alla effettiva realizzazione crittografica.

Risultati attesi:

Primo anno
- definizione di un linguaggio imperativo con primitive di comunicazione crittografiche e studio di semplici sistemi di tipi per proprietà di Non-Inteferenza "forte" (indipendente dallo scheduler)
Secondo anno
- estensione dei risultati del primo anno a proprietà diverse come autenticazione dei messaggi e non ripudiabilità;
- studio di primitive astratte di comunicazione che permettano di rendere la programmazione indipendente dalla realizzazione crittografica.


VE3 - Stepwise refinement di programmi concorrenti sicuri (WP2)

L'utilizzo di raffinamenti successivi per lo sviluppo di sistemi complessi è una tecnica standard di ingegneria del software. Partendo dalla descrizione dei requisiti del sistema, ad ogni passo viene costruita una descrizione più concreta, corretta rispetto alla versione precedente, fino ad ottenere la versione finale implementabile. La correttezza del sistema finale è automaticamente garantita dall'applicazione di operazioni che preservano le proprietà iniziali. In questo progetto ci focalizzeremo su proprietà per linguaggi orientati alla sicurezza, ed analizzeremo varie operazioni di raffinamento quali la specializzazione di componenti astratte, la cancellazione di scelte non-deterministiche e la sostituzione di sottocomponenti. Per ciascuna operazione considereremo diverse proprietà di sicurezza ed identificheremo le condizioni sotto le quali l'operazione e' applicabile. Per ottenere questo risultato intendiamo percorrere la stessa linea seguita nell'ambito delle process algebra in [BFPR03] dove prima viene definito un framework generale per la definizione di proprietà di non interferenza e poi vengono individuate condizioni sufficienti per il loro mantenimento durante i passi di raffinamento.

Risultati attesi:

Primo anno
- sviluppo di un framework generale per la definizione di proprietà di sicurezza per programmi scritti in un linguaggio imperativo con costrutti di parallelismo ed atomicità;
- identificazione di un insieme di operazioni di raffinamento utilizzabili per lo sviluppo di sistemi sicuri.
Secondo anno
- classificazione di insiemi di programmi e proprietà persistenti rispetto alle operazioni considerate.


VE4 - Analisi statica per la sicurezza computazionale di protocolli di autenticazione (WP3)

Intendiamo sviluppare un'analisi statica per verificare autenticazione su protocolli che usano la libreria per operazioni crittografiche di Backes-Pfitzmann-Waidner [BPW03]. La libreria crittografica è dotata di due semantiche, la prima simbolica e la seconda computazionale. È stato dimostrato che, in generale, una proprietà di sicurezza soddisfatta dalla semantica simbolica è soddisfatta anche da quella computazionale. Quindi le prove effettuate sulla semantica simbolica sono automaticamente valide anche sulla reale implementazione crittografica.
Lo sviluppo di tale analisi statica è interessante perché fornirebbe uno strumento semplice e facilmente automatizzabile per la verifica di protocolli sul modello computazionale sopra menzionato; l'analisi, infatti, sarebbe effettuata solamente sul codice del protocollo e sarebbe quindi immune da problemi come l'esplosione dello spazio degli stati. Non siamo a conoscenza di altri risultati simili in letteratura.
Il punto di partenza di questo lavoro è il sistema di tipi per protocolli di autenticazione proposto recentemente da Bugliesi, Focardi e Maffei [BFM07]. Questa tecnica presenta alcuni vantaggi: (i) è al tempo stesso modulare e composizionale, poiché ciascuna componente del protocollo viene analizzata in modo indipendente e l'esecuzione concorrente di protocolli ritenuti sicuri è ancora sicura. Questa proprietà rende il sistema adatto ad analizzare situazioni in cui vengono eseguiti simultaneamente protocolli differenti [M04]; (ii) è completamente automatizzata, grazie ad una procedura di inferenza, e non richiede alcuna familiarità da parte dell'utente con i sistemi di tipi ed effetti [FMP05]; (iii) è generale ed estendibile, ed infatti ha permesso di analizzare diversi protocolli esistenti.
NOTA: Questa ricerca sarà sviluppata in collaborazione con il Computer Science Department della Saarland University di Saarbrücken.

Risultati attesi:

Primo anno
- definizione di un linguaggio per protocolli crittografici con semantica basata sulla libreria crittografica di Backes, Pfitzmann e Waidner;
- sviluppo di un sistema di tipi per verificare autenticazione sul nuovo linguaggio.
Secondo anno:
- estensione ad altre proprietà di sicurezza, come ad esempio la non ripudiabilità;
- estensione ad altre tecniche di analisi, come ad esempio l'interpretazione astratta discussa in VE1.


VE5 - Sicurezza in Java tramite interpretazione astratta (WP2)

L'unità di Venezia ha acquisito una consolidata competenza nell'ambito delle tecniche di interpretazione astratta: sono state studiate alcune tecniche finalizzate ad aumentare la precisione, a ridurre la complessità, e a modularizzare l'analisi, attraverso operatori di raffinamento, di semplificazione, di composizione e scomposizione di domini astratti. Sono stati inoltre studiati alcuni domini astratti specifici per l'analisi di programmi in vari paradigmi di programmazione, con una crescente attenzione a proprietà di sicurezza (information leakage detection).
Una delle caratteristiche dei comuni linguaggi di programmazione che li rende più vulnerabili rispetto a proprietà di sicurezza è la possibilità che essi offrono al programmatore di programmare in multithread, per esempio per eseguire più task allo stesso tempo, per realizzare delle interfacce grafiche complesse o per ottimizzare l'impiego di risorse; inoltre, questo sembra oggi l'unico modo per trarre pieno vantaggio dalle architetture multicore. La ricerca si concentrerà sulla definizione, lo sviluppo e l'implementazione di un'analisi per programmi multithread, basata sulla teoria dell'interpretazione astratta. Il linguaggio di programmazione preso in considerazione sarà (un opportuno sottoinsieme di) Java al livello bytecode, visto il supporto al multithreading integrato all'interno del linguaggio stesso, la sua relativamente semplice semantica e la sua larga diffusione.

Risultati attesi:

Primo anno
- specifica della semantica concreta di un sottoinsieme multithreaded di Java corretta rispetto al Java Memory Model [MAN05], ovvero di un modello matematico molto fedele all'esecuzione di un programma Java multithread.
- sviluppo di una semantica astratta, che sarà abbastanza approssimata per poter essere calcolabile, ma anche abbastanza precisa per provare alcune proprietà di interesse, tra cui il determinismo.
Secondo anno
- prove di correttezza dell'astrazione rispetto alla semantica concreta;
- implementazione di un prototipo di analizzatore astratto e ottimizzazione di tale prototipo.


VE6 - Agenti mobili e metodi formali per il confinamento di codice malevolo (WP1)

Uno degli obiettivi che ci poniamo è quello di studiare come applicare le tecniche "contigue" e "monotone" per l'isolamento del codice malevolo ("intruder") all'interno di diverse topologie di rete. In particolar modo ci interesseremo allo studio di nuovi algoritmi distribuiti che, attraverso l'uso di agenti mobili, siano in grado risolvere, con un numero polinomiale di mosse, il problema dell'isolamento dell'intruder su topologie di reti non ancora considerate. Ci proponiamo inoltre confrontare le formalizzazioni dei vari modelli presenti in letteratura tramite tecniche di interpretazione astratta. L'obiettivo è quello di ottenere risultati generali sui relativi poteri espressivi dei modelli che permettano di capire quali caratteristiche aggiuntive di un modello rendono la computazione strettamente più efficiente. Ad esempio, è noto che, su specifiche topologie, la conoscenza dello stato dei nodi adiacenti permette di migliorare la complessità in numero di mosse di alcuni algoritmi. Un altro esempio classico è il passaggio da modelli asincroni a modelli sincroni, che permette di avere un limite superiore al tempo di migrazione degli agenti. Anche la clonazione di agenti può migliorare le prestazioni di questi algoritmi dando, intuitivamente, più potere di isolamento agli agenti stessi.

Risultati attesi:

Primo anno
- nuovi algoritmi su topologie particolari di reti;
- formalizzazione di un linguaggio per la specifica di agenti mobili.
Secondo anno
- definizione della semantica di tale linguaggio e confronto con i modelli esistenti;
- confronto tra varianti del linguaggio con differenti caratteristiche e primitive.