RICERCA ITALIANA     

Programma di ricerca

SOFT - Tecniche formali orientate alla sicurezza

Università di riferimento

Università degli Studi di VERONA - INFORMATICA - ()

Responsabile dell'Unità di ricerca

Luca Viganò

Descrizione

Allo scopo di affrontare il complesso problema dell’analisi degli aspetti di sicurezza e di “trust” dei servizi e del modo in cui questi interagiscono in reti distribuite, dinamiche, e orientate ai servizi, svilupperemo una panoplia di metodologie e tecnologie. Procederemo attraverso approcci paralleli ma connessi, che possono essere ripartiti su 3 diversi “workpackage”: Sicurezza delle Reti di Comunicazione (WP1), Sicurezza a Livello Applicazione (WP2), e Aspetti Quantitativi della Sicurezza (WP3).


WP1: Sicurezza delle Reti di Comunicazione

WP1.1 Trust establishment nelle reti ad-hoc

La nozione di trust in reti ad-hoc e' un'area nuova e stimolante [Gli04,PM06]. L'assenza di una infrastruttua di rete fissa, la mobilita' dei nodi, il limitato raggio d'azione della trasmissione, la condivisione del medium, e la vulnerabilita' fisica dei dispositivi rappresentano alcune delle peculiarita' delle reti ad-hoc che hanno una pesante ricaduta nella progettazione di uno schema di trust.

E' importante distinguere tra due tipi di reti ad-hoc.

(1) Le reti ad-hoc in ambienti ostili, dove la presenza di uno "strong attacker" e' altamente probabile. In questi casi i dispositivi vengono "pre-caricati" con appropriate chiavi crittografiche in accordo col ruolo ricoperto all'interno della rete. Queste chiavi hanno lo scopo di proteggere la comunicazione tra i dispositivi stessi. Fintantoche' un nodo non risulti compromesso e' ragionevole aspettarsi un'alta cooperazione all'interno della rete.
In queste reti quello che viene comunemente chiamato "trust evidence" ha vita breve. Infatti, la sicurezza di un nodo mobile puo' dipendere dalla sua dislocazione; cosa che non puo' essere determinata a priori. Per esempio, la cattura di un nodo da parte di un avversario e' un evento altamente probabile in uno scenario militare. Le relazioni di trust che coinvolgano un nodo catturato devono essere cosi' invalidate e nuova "trust evidence" dovra' essere raccolta per garantire la connettivita' all'interno della rete.
Le sfide maggiori nel campo della sicurezza di tali reti riguarda il routing sicuro, la prevenzione dell'analisi del traffico di comunicazione, e la resistenza di un nodo catturato al "reverse engineering" e la determinazione delle proprie chiavi crittografiche.

(2) Nelle reti ad-hoc auto-organizzate non esiste alcuna authority che si prenda cura della rete, neppure in fase di inizializzazione. La rete e' quindi perfettamente peer-to-peer ed i nodi devono stabilire autonomamente come rendere sicura la comunicazione. Questo tipo di reti si basano su una relazione di trust un po' naive in cui ci si fida del nodo spazialmente vicino. Tali relazioni di trust originano, si sviluppano, e terminano a run-time e di solito hanno vita breve. Poiche' basate sulla cooperazione tra nodi, queste relazioni di trust sono fortemente esposte ad attacchi.

Non vi e' dubbio che il primo tipo di reti viste, in cui vi e' una pre-configurazione dei nodi, siano piu' facili da trattare. D'altro canto, a nostro avviso, queste assunzioni sono in qualche modo in contraddizione con la natura delle reti ad-hoc, la cui formazione dovrebbe essere improvvisata e spontanea. La determinazione del trust puo' essere dovuta ad esperienze precedenti avute con un determinato nodo oppure dipendere da raccomandazioni da parte di nodi in cui si ripone fiducia. Il trust e' comunque un concetto legato al passare del tempo: puo' crescere e diminuire in un certo periodo di tempo.

L'obiettivo del nostro lavoro e' duplice: da un lato vorremmo sviluppare modelli formali per il trust in accordo con le costrizioni delle reti ad-hoc; dall'altro vorremmo integrare questi modelli in un calcolo di processi per reti ad-hoc sviluppando una teoria appropriata per provare formalmente proprieta' di sicurezza.


WP1.2 Analisi simbolica di protocolli per la sicurezza informatica

Contribuiremo allo sviluppo di una logica temporale per agenti comunicanti che fornisca un linguaggio intuitivo ed allo stesso tempo espressivo per formalizzare proprieta' locali (“agent-specific”) e globali (“system-wide”) di sistemi distribuiti. Questa logica puo’ essere usata sia per l’analisi oggetto di protocolli di sicurezza, cioe' per ragionare su protocolli e loro proprieta', sia per dimostrare meta-proprieta' di vari modelli di protocollo, e mostrare cosi’ la correttezza di varie tecniche di modellizzazione e semplificazione fondamentali per lo sviluppo di strumenti di analisi di protocolli. Queste analisi saranno “simboliche” in quanto astrarremo dalle concrete proprieta’ della crittografia (che invece considereremo in WP3), e saranno sviluppate in un tool chiamato AVISPA [AVISPA]. AVISPA e' un tool integrato per la validazione automatica di protocolli di sicurezza ed applicazioni per sistemi distribuiti, ed e' stato utilizzato con successo su diversi protocolli industriali (IKE, SET, etc.) in corso di standardizzazione da parte di enti di standardizzazione quali IETF, ITU, e W3C. AVISPA puo' essere sensibilmente migliorato, specialmente per quanto riguarda le tecniche formali su cui si basa. Ad esempio, l'estensione di queste tecniche formali con linguaggi piu' naturali per modellare proprieta' di sicurezza renderebbe il tool di piu' facile comprensione ad utenti non esperti. Inoltre abbiamo iniziato a studiare la possibile integrazione in AVISPA di tecniche di riduzione e semplificazione ispirate dalla riduzione di ordine parziale ed alla interpretazione astratta. Queste tecniche, insieme ad altre tecniche di astrazione, forniranno le basi per l'applicazione di AVISPA all'analisi formale ed automatica di proprieta' di sicurezza per Web services e piu' in generale nell'area dell' "Service-Oriented Computing", che considereremo in WP2.1.



WP2: Sicurezza a Livello Applicazione

WP2.1 Analisi formale di servizi per la sicurezza

Mentre AVISPA e altri approcci simili (quali [BLA01,RSGLR00]) sono stati utilizzati per validare diversi protocolli di livello industriale per la sicurezza e hanno fornito un supporto per il miglioramento della sicurezza dei sistemi software, il problema della validazione formale della sicurezza del “Service-Oriented Computing” e` tuttora ben aldila’ di cio’ che e’ possibile allo stato dell’arte, nonostante qualche promettente risultato preliminare, quali [BMPV06,SAMOA]. Nell’ambito del “Service-Oriented Computing”, i servizi di sicurezza vengono sempre piu' separati dai sistemi e le applicazioni che li impiegano. Tuttavia, a seconda della loro funzionalita', e del contesto di utilizzo, nuove ed elusive forme di interferenza possono emergere nella composizione di sistemi. Si noti che poiche' la composizionalita' e l'integrazione sono alla base di "Service-Oriented Computing", invece di una semplice combinazione di servizi di sicurezza abbiamo bisogno di validare sia i servizi di sicurezza sia la composizione sicura di servizi in infrastrutture modulari di sicurezza. Utilizzeremo il tool AVISPA e le sue tecniche di analisi come punto di partenza per lo sviluppo di linguaggi e metodi formali basati su “abstract model-checking” per la specifica formale di servizi di sicurezza, insieme alla loro analisi formale e validazione composizionale automatiche. In questa ricerca il bilanciamento tra efficienza e preservazione forte nei sistemi approssimati e’ essenziale. Questo permettera di modellare e ragionare su proprieta' e servizi di sicurezza, sia a livello di rete sia a livello di applicazione, includendo non solo "authentication" e "secrecy", ma anche "authorization", controllo degli accessi, “policies”, “trust” e "identity management" e cosi` via, oltre a nuovi modelli dell’attaccante quali quelli considerati in [HDMV05,HDMVB06].


WP2.2 Modelli e metodi per la verifica di non-interferenza

In questo workpackage siamo interessati a studiare i problemi di trasformazione del codice con particolare riferimento a modelli e metodi per la verifica di non-interferenza in presenza di attaccanti attivi, su sistemi di calcolo probabilistici e su basi di dati. L'idea di fondo e' quella di vedere l'interpretazione astratta e la non-interferenza astratta come schema unificante per esprimere sia i modelli di attacco al sistema (attivo attraverso malware o passivo attraverso osservazione semantica) che il tipo di informazione nascosta (e.g., nei dati protetti) e come questa evolve durante la computazione (information-flow analysis). L'obiettivo e' quello di derivare una teoria unificante basata su interpretazione astratta per derivare in un unico schema concettuale algoritmi efficaci per proteggere il codice ed i dati e verificarne la sicurezza.

Siamo interessati alla definizione di una metodologia generale per la derivazione sistematica di trasformatori di domini astratti finalizzati alla trasformazione del codice per renderlo piu` sicuro rispetto a processi di reverse engineering. L'idea principale consiste nell'uso dello stesso framework di interpretazione astratta, portato pero' all'ordine superiore: l'oggetto del discorso sono ora i domini invece delle descrizioni di stato dei programmi. L'uso dell'interpretazione astratta sui tipi superiori, ovvero sui domini astratti e sulle loro trasformazioni invece che sui soli dati dei programmi, mostrera' il potenziale dei metodi dell'interpretazione astratta per la completa progettazione di analizzatori versatili di programmi, ovvero parametrici sulle proprieta' che essi vogliono indurre o preservare a meno dell'approssimazione. Questi strumenti permetteranno di arrivare alla caratterizzazione di un framework nel quale e' possibile derivare operazioni di trasformazione di programmi guidate da proprieta' che si vogliono o non si vogliono proteggere.

La nozione di 'Non-Interferenza Astratta' presentata in [GM04] e' generale e teoricamente applicabile ad ogni problema di sicurezza sui linguaggi e sui modelli di calcolo per i quali sia possibile definire una semantica formale. Uno degli aspetti piu' interessanti della nozione di Non-Interferenza Astratta e' il fatto di essere una nozione semantica: cio' significa che attraverso il raffinamento della semantica e' possibile raffinare la nozione di `segretezza' considerata. In particolare questo permette di rivelare `covert channels' [SM03] dovuti a tempi diversi di terminazione delle computazioni e canali probabilistici dovuti a diverse probabilita' di computazione. Innanzittutto abbiamo pianificato l'estensione della Non-Interferenza Astratta allo scopo di trattare i covert channels probabilistici. Riteniamo che cio' sia possibile tramite la definizione della Non-Interferenza Astratta in termini di domini astratti probabilistici. Un problema leggermente piu' complesso che ci poniamo come obiettivo consiste nell'estendere tale nozione per certificare proprieta' di sicurezza anche in presenza di attaccanti attivi, ovvero attaccanti capaci non solo di osservare, ma anche di modificare la computazione di un sistema. La nostra idea e' quella di modellare attaccanti attivi come trasformatori semantici di programmi, ovvero trasformatori di domini, e usare il framework di trasformazione dei programmi di [CC02] per modellare e caratterizzare il piu' potente attaccante attivo innocuo. Il problema di proteggere l'informazione privata e' particolarmente rilevante anche nel contesto delle basi di dati, dove attraverso `query' che riguardano solo l'informazione pubblica e' possibile dedurre informazioni sui dati sensibili. Quindi, siamo interessati all'uso della nozione di non-interferenza astratta per indebolire le politiche di sicurezza usate per proteggere le basi di dati, permettendo dunque il flusso di aspetti non sensibili dei dati privati.


WP3: Aspetti Quantitativi della Sicurezza

L’obiettivo di questo work package è lo studio di un modello che serva per l’analisi gerarchica e composizionale di protocolli complessi, che fornisca una base comune all’analisi di protocolli nei modelli puramente simbolici/computazionali o ibridi, e che permetta lo studio della correttezza dell’approccio simbolico rispetto all’approccio computazionale. Il punto di partenza sarà il lavoro sulle relazioni di simulazione approssimate di Segala e Turrini. In questo contesto intendiamo:

- Raffinare la nozione di simulazione approssimata introdotta da Segala e Turrini per renderla più generale e adatta all'analisi di un'ampia gamma di protocolli. La relazione studiata finora non tiene conto di eventuali azioni invisibili (le cosiddette simulazioni deboli) e non è adatta ad analizzare astrazioni in cui più passi di computazione sono inglobati in un solo passo.

- Studiare le relazioni che sussistono tra simulazioni approssimate e inclusioni di linguaggi approssimate. Spesso, infatti, le proprietà di sicurezza di un sistema possono essere espresse in termini di inclusione approssimata di linguaggi, così come in ambiente distribuito l'inclusione di linguaggi è spesso sufficiente per l'analisi di un sistema. E' utile dunque poter vedere le simulazioni approssimate come metodo di dimostrazione corretto per le inclusioni di linguaggio approssimate.

- Studiare le relazioni che sussistono tra simulazioni approssimate e
metriche. Esiste infatti una vasta letteratura sullo studio di metriche per sistemi probabilistici. I protocolli crittografici sono una delle applicazioni usate a supporto dello studio delle metriche, sebbene non esistono casi di studio precisi. Ci si chiede dunque se esistono metriche indotte da simulazioni approssimate e come queste metriche si legano alla letteratura esistente.

- Studiare l'impatto del nondeterminismo nello studio di simulazioni approssimate. Il nondeterminismo è un elemento di notevole disturbo e il tipico approccio per gestirlo è quello di eliminarlo. Tuttavia l'eliminazione brutale nel nondeterminismo può nascondere attacchi pericolosi. La disponibilità di un modello quale i Probabilistic Automata in cui il nondeterminismo coesiste con gli aspetti più computazionali permette di valutare in maniera rigorosa quali sono le modalità di eliminazione del nondeterminismo e quali sono le relative conseguenze. Un approccio tipico è quello di restringere le capacità di uno schedulatore nella risoluzione del nondeterminismo, e.g. [CCKLLPS06,CP07,GRS07], ma questo richiede di comprendere come le simulazioni approssimate possono essere adattate a nuovi scenari con nondeterminismo ristretto.

- Valutare gli studi sui modelli mediante casi di studio che allo stesso tempo possono fornire utili linee guida. L'effettiva analisi di protocolli permette di individuare gli aspetti critici che devono essere gestiti dalle tecniche di dimostrazione che stiamo cercando. Tra i casi di studio che intendiamo considerare ci sono l'analisi rigorosa della correttezza della Crypto Library di Backes, Pfitzmann, Waidner [BPW03], dove sospettiamo che le simulazioni approssimate possono aiutare a ridurre l'analisi globale della probabilità di raggiungere un "error set" all'analisi della probabilità di raggiungere un error set in un solo passo di computazione, e lo studio di proprietà di soundness del modello simbolico rispetto al modello computazionale, e.g. [AR02,MW04,CKKW06]. Quest'ultimo caso di studio è motivato dal fatto che le relazioni di simulazione permettono di stabilire corrispondenze tra computazioni concrete e computazioni simboliche, che i lavori in letteratura si basano sullo stabilire simili corrispondenze, e che l'aspetto più debole delle dimostrazioni esistenti è proprio nella dimostrazione di esistenza di una corrispondenza tra le computazioni.