RICERCA ITALIANA     

Programma di ricerca

SOFT - Tecniche formali orientate alla sicurezza

Università di riferimento

Università degli Studi di PISA - INFORMATICA - ()

Responsabile dell'Unità di ricerca

Chiara Bodei

Descrizione

L’unità di ricerca di Pisa sarà coinvolta nei workpakages 1, 2, 3 e 4.

WP1
1) Una metodologia basata sulla semantica per l’analisi e la verifica di protocolli di sicurezza
La nostra metodologia si basa sull’analisi di Flusso di Controllo (CFA), una tecnica statica che costruisce un modello del protocollo, approssimandone il comportamento. In relazione alle proprietà considerate, vengono selezionati e tracciati staticamente dei valori specifici. Il loro controllo permette di verificare possibili violazioni di proprietà a tempo di esecuzione. Si possono isolare e raccogliere delle informazioni specifiche, se presenti, corrispondenti alla violazione di una proprietà. Le informazioni raccolte agiscono cioè come marker per possibili problemi di sicurezza. Le proprietà analizzate sono spesso abbastanza semplici, tuttavia la loro violazione è il sintomo che proprietà come segretezza e autenticazione possono essere altrettanto violate.

Mentre le proprietà considerate variano, non altrettanto fa la parte centrale della CFA. Cambiano solo i valori di interesse tracciati per testare possibili violazioni. Questo costituisce uno dei principali vantaggi della nostra metodologia: una singola analisi basta per una varietà di proprietà: dato un protocollo, ispezioni diverse delle risultanti approssimazioni permettono di controllare proprietà diverse tra loro, senza bisogno di ripetere l’analisi ogni volta.

Finora, abbiamo applicato la CFA a LySa, per verificare svariate proprietà di sicurezza, come ad esempio l’autenticazione di messaggi e la segretezza [BBDNN05], quelle relative alla “freshness” (garanzia che alcuni dati sono stati appena generati) [GBDN07], e agli attacchi basati sulla violazione di tipo [BDGB07].

Un’interessante linea di ricerca consiste nello sviluppo uteriore dell’approccio usato in [BDGB07]. Lì si applica la nostra metodologia ad un’estensione di LySa, per scoprire possibili attacchi basati sulla violazione semplice di tipo (che avvengono quando chi riceve un messaggio confonde un campo con un altro, ad es. accettando un nonce al posto di una chiave). LySa è stata estesa con speciali etichette o “tag” che rappresentano i tipi attesi dei termini. L’analisi controlla staticamente se i dati ricevuti siano del tipo richiesto dall’etichetta.

Da questo punto di vista, la nostra metodologia agisce in maniera descrittiva, descrivendo quali violazioni di tipo sono possibili. Nello stesso contesto, può anche essere usata in modo prescrittivo. Infatti si può imporre semanticamente che i dati vengano accettati solo se del tipo atteso. A questo punto, l’analisi può controllare se gli errori di tipo sono ancora possibili. Incorporare le etichette nei messaggi a tempo di esecuzione comporta l’utilizzo extra e magari non necessario sia di potere di calcolo che di banda di trasmissione. Questo può essere particolarmente gravoso quando le risorse sono limitate come nei PDA, cellulari, portatili, etc. Usare le etichette staticamente può al contrario dare indicazioni sul loro uso ottimale, a tempo di esecuzione.
Sono noti molti modi di assegnare etichette che possiamo usare in modo simile, come annotare ciascun messaggio e suo componente con il suo tipo, come suggerito in [Car94] per affrontare i “replay attacks”. Le informazioni di tipo da includere comprendono un identificatore per (1) il protocollo, (2) la sessione del protocollo, (3) il passo del protocollo, (4) il sottocomponente del messaggio, (5) il tipo di ogni componente.
Interessante anche l’etichettamento in [BFM04] che descrive come i componenti di un messaggio contribuiscano al raggiungimento dell’autenticazione, memorizzando il ruolo voluto per ogni componente.

Lo sviluppo della nostra metodologia segue lo stesso schema. Dapprima scegliamo dei valori di interesse, quindi scegliamo una particolare proprietà dinamica di sicurezza. Alla fine, definiamo un test statico che implica la proprietà dinamica. Questo può richiedere alcune estensioni, che però non hanno effetto sui passi precedenti. Questo ci spinge a considerare la possibilità di studiare una meta-struttura per una piattaforma dell’analisi indipendente dalle proprietà, allo scopo di rendere sistematici gli opportuni aggiustamenti, nel momento in cui si affrontano altri problemi o proprietà.

Un’estensione naturale del nostro approccio alla convalida di protocolli consiste nello studio dei sistemi multi-protocollo. In questo contesto, possono essere eseguiti concorrentemente più protocolli e uno stesso agente può eseguirne più di uno. Gli usuali problemi di sicurezza sono di conseguenza più difficili da affrontare, a causa delle possibili e indesiderate interazioni tra le varie esecuzioni e i vari agenti. Inoltre, le garanzie di sicurezza per un protocollo in isolamento possono non essere le mantenute nel caso ci siano vari protocolli in esecuzione sulla rete.


WP1.2: Raffinamento per tematiche relative alle sessioni
I linguaggi di specifica ad alto livello consentono di specificare i sistemi distribuiti in modo semplice, nascondendo parte dei dettagli implementativi. Tuttavia, proprio per questo è possibile che da una specifica sicura ad alto livello si ricavi un'implementazione insicura, ad es. perché nel modello astratto si assumevano implicitamente alcune proprietà. Per studiare questi problemi, dobbiamo studiare tecniche per il raffinamento delle specifiche di alto livello in quelle corrispondenti di basso livello, come per esempio, il tradurre primitive per le sessioni nei relativi protocolli. Studieremo il rapporto tra i livelli di specifica, in modo da capire quali proprietà vengono preservate dai raffinamenti e quali no.

Svilupperemo tecniche per la verifica di specifiche ad alto livello, che lavorano sulle primitive per le sessioni, e a basso livello, che lavorano sugli effettivi protocolli che implementano tali primitive. Dove le tecniche di verifica mostrino la correttezza solo nel caso di alto livello, indagheremo per studiare se la proprietà studiata si è persa nel raffinamento. In caso contrario, potremo tentare di migliorare la verifica a basso livello. Sviluppare uno strumento automatico di verifica potrebbe essere utile.

Inoltre, affronteremo il problema di stabilire la sicurezza dei protocolli con un'alta affidabilità. In particolare, vorremmo estendere le attuali tecniche di verifica in modo che, quando un protocollo viene ritenuto sicuro, si produca una qualche giustificazione per la sua sicurezza. Idealmente, si produrrebbe una vera e propria dimostrazione di sicurezza in modo automatico. Questo è utile perché tali dimostrazioni si possono controllare indipendentemente con un piccolo programma di verifica fidato. In tal caso, si avrebbe una grande affidabilità sulla effettiva sicurezza del protocollo, visto che una verifica indipendente diminuirebbe l'impatto di eventuali bug nell'implementazione della tecnica di verifica, di solito piuttosto complessa.

3) WP1.3: Verifica di protocolli di sicurezza visti come sistemi aperti
I modelli per protocolli di sicurezza basati su calcoli di processi possono facilmente essere estesi con primitive linguistiche che permettano una più chiara formalizzazione di aspetti rilevanti per la sicurezza in uno stile orientato ai sistemi aperti. Vari aspetti, come le capacità di interconnessione dei principali e la condivisione di chiavi prevista, possono essere convenientemente modellati in termini della negoziazione dinamica in un ambiente aperto fatta dai partecipanti al protocollo. Questi aspetti, invece, richiedono una codifica manuale esplicita e ad-hoc secondo varie delle proposte esistenti. Questi calcoli verranno quindi dotati di semantiche simboliche, estese per trattare la specifica, eventualmente incompleta, dell'ambiente di esecuzione.
Si tenterà una formalizzazione delle proprietà di interesse e di altre, riguardanti la composizione sicura in sistemi aperti. La classificazione di proprietà risulta un interessante problema ancora aperto.

Si ritiene che l'uso di semantiche simboliche possa facilitare lo sviluppo di metodi di verifica effettivi e il trattamento dei problemi di incompletezza tipici della verifica di proprietà di sicurezza. L'espressività degli approcci dinamico e statico verrà confrontata nel contesto formale proposto, si confronteranno, ad es. le tecniche che "astrattamente" simulano il comportamento dinamico del sistema (ad. es. symbolic model checking) con quelle che fanno staticamente astrazioni sulla specifica del sistema (ad es. analisi di flusso di controllo). Un possible risultato è l'integrazione delle metodologie di verifica.


WP2
WP2.1: Composizione sicura di servizi
I meccanismi di autenticazione non sono sufficienti a garantire la sicurezza nel paradigma del Service-Oriented Computing. Anche nel caso che i protocolli di sicurezza adoperati siano sicuri, la sicurezza di un sistema distribuito può essere violata a causa di codice mobile (malware), o per via di errori di programmazione contenuti in servizi altrimenti ritenuti affidabili, o a causa di comportamenti inattesi ed indesiderati che si ottengono componendo i servizi (es. il trapelare non voluto di informazioni segrete). In tutti questi casi, la sicurezza si può recuperare con tecniche basate sui linguaggi. In particolare, siamo interessati a primitive linguistiche e ad analisi statiche per la protezione sia dei clienti che dei servizi.

La primitive linguistiche che riteniamo più promettenti per la sicurezza sono le politiche locali e la “chiamata per contratto”. Al fine di garantire la sicurezza di un'applicazione, è necessario che queste primitive vengano studiate ai vari stadi di sviluppo del software, dall'analisi dei requisiti, alla progettazione, sino all'implementazione del sistema. La chiamata per contratto prevede che la selezione dei servizi sia basata sulle proprietà di cui essi godono - piuttosto che sull'identità del produttore del servizio, come accade attualmente. Questo ci consente di ridurre la base affidabile di computazione, ovvero quell'insieme di componenti hardware/software, il cui comportamento scorretto renderebbe insicuro il sistema. Infatti, con questo meccanismo, è necessaria l’affidabilità della solo entità che certifica i servizi, e non della miriade di entità che li mettono a disposizione. Un ulteriore passo verso la sicurezza consiste nel dimostrare formalmente, ad es. con analisi statiche, la correttezza dell'entità di certificazione.

Intendiamo inoltre sviluppare il meccanismo di chiamata per contratto, considerando anche altre proprietà di sicurezza (es. information-flow) e aspetti non-funzionali (es. transazioni, qualità del servizio). Vorremmo ad es. scartare un servizio che può lasciar trapelare dati privati del cliente.

Un altro problema è come orchestrare un'applicazione basata su servizi, garantendo che non si abortisca la sua esecuzione a causa di azioni che tentano di violare la sicurezza. Questo problema di pianificazione consiste nel selezionare dalla rete quei servizi che svolgono il compito richiesto, rispettando al contempo i vincoli di sicurezza imposti. Quei servizi che soddisfano localmente la proprietà richiesta non sempre sono buoni candidati, dato che il loro comportamento potrebbe invalidare la sicurezza dell'intera composizione.
Una prima soluzione a questo problema è in [BDF06b], e sfrutta una combinazione di sistemi di tipo/effetto e model-checking. In [BDFZ07a] la proposta viene estesa considerando un modello di calcolo con scenari dinamici, dove i servizi possono essere pubblicati dinamicamente e divenire temporaneamente non disponibili. Nel contempo, puntiamo ad un’orchestrazione efficiente e incrementale. Infine in [BDFZ07b] si considerano le stesse problematiche nel contesto della progettazione del software per il Service-Oriented Computing, proponendo un modello grafico per il design di servizi sicuri.
Un'altra direzione di ricerca consiste nel trattare la composizione di servizi insieme ai protocolli per la sicurezza e alle "trust relationships" (ad es. il servizio A si fida del servizio B). Questo permetterebbe ad es. di garantire che un servizio certificato non cambi il proprio codice a tempo di esecuzione.

WP3:
WP3.1:Verso aspetti più concreti (collegato anche con il WP1)
Di solito, la specifica di protocolli viene data ad un livello molto alto di astrazione e molti aspetti implementativi, come ad esempio quelli crittografici, sono perduti. Ci sono situazioni in cui questa visione astratta non si rivela completamente adeguata. Ad alto livello, un messaggio all’interno di un protocollo si compone di campi: ogni campo rappresenta un certo valore, come il nome di un agente, un nonce, o una chiave. Un’algebra di processo può facimente modellare una tale struttura. Tuttavia, ad un livello più concreto, un messagio non è nient’altro che una mera sequenza di bit. In questa visione, chi riceve un messaggio deve decidere come interpretare la stringa di bit, cioè come decomporre la stringa in sottostringhe da associare ai campi attesi del messaggio. Il messaggio arriva infatti senza alcuna indicazione sulla sua arità e sui tipi dei suoi componenti. Un intruso può approfittare di questa fonte di ambiguità per organizzare un attacco basato su violazioni di tipo.
Abbiamo già visto sopra come si possono trattare le violazioni semplici di tipo, usando l’etichettamento. Le violazioni complesse di tipo si hanno invece quando una concatenazione di campi viene scambiata per un singolo campo. Questo livello di granularità non è facile da cogliere per un calcolo di processo standard, in cui i termini sintattici sono usati per modellare astrattamente un messagio, con l’ipotesi che i messaggi vengano interpretati correttamente. Dobbiamo quindi estendere la nostra metodologia per avvicinarci maggiormente all’implementazione concreta, e così affrontare gli attacchi basati sulle violazioni complesse di tipo. In questo caso, nel contesto di LySa, vorremmo modellare i campi di un messaggio di un protocollo ad un livello di astrazione sufficiente per modellare formalmente le possibili confusioni di tipo.

WP4
WP4.1: Catturare aspetti qualitativi
Ragionare in termini di causalità tra eventi può essere utile per la formalizzazione di varie proprietà di sicurezza (vedi ad es. [FHG98,P99,CW01]). Da questo punto di vista sembra chiaro che la teoria della concorrenza e i suoi modelli abbiano molto da offrire all’analisi per la sicurezza.
Estensione dei transition systems, i Proved transition systems [DP92,DP99] rappresentano modelli capaci di catturare la causalità. Li possiamo immaginare come una sorta di rappresentazione compatta delle computazioni, in grado di contenere tutta l’informazione rilevante che si può codificare. Le transizioni sono decorate con etichette che codificano le dimostrazioni, ovvero i passi necessari nella deduzione dell’azione appena eseguita. Ispezionando tali etichette, generate automaticamente da una semantica operazionale arricchita, è possible inferire le dipendenze causali, rappresentate con un insieme di riferimenti alle transizioni precedenti. Come punto di partenza per dare a LySa una semantica causale, si può considerare la semantica arricchita data in [BetAl05].

Prevediamo anche di sperimentare una formalizzazione logica, usando la Distributed State Temporal Logic (DSTL) [MSS04]. Tale formalismo permette mettere in relazione proprietà che valgono in componenti distinte, in un contesto asincrono.
In passato DSTL è stata usata con successo per specificare e verificare applicazioni in cui le componenti avevano svariati requisiti di sicurezza [MS04]. Inoltre la logica include un operatore primitivo per specificare eventi: rendendo possibile mescolare dunque condizioni ed eventi nelle formule che definiscono la specifica del sistema.
La capacità di usere esplicitamente gli eventi aumenta la capacità espressiva e la semplicità delle specifiche logiche, e sembra essere particolarmente adeguata per descrivere proprietà di sicurezza.