Pescara

La proposta di ricerca dell'unità d Pescara (unità 4) ha le basi sulle conoscenze già acquisite dai componenti dell'unità nei campi dei vincoli soft, dell'astrazione e della concorrenza. L'attività da una parte mirerà ad estendere il formalismo dei vincoli soft e dall'altra parte studierà possibili utilizzi di vincoli soft con astrazione e concorrenza per lo studio di sistemi e applicazioni.

Stefano Bistarelli
responsabile scientifico unità
Dip. di Scienze
Università degli Studi "G.d'Annunzio"
bista(at)sci.unich.it
Meo Maria Chiara
Dip. di Scienze
Università degli Studi "G.d'Annunzio"
meo(at)sci.unich.it
Amato Gianluca
Dip. di Scienze
Università degli Studi "G.d'Annunzio"
amato(at)sci.unich.it
Fioravanti Fabio
Dip. di Scienze
Università degli Studi "G.d'Annunzio"
fioravanti(at)sci.unich.it

Dottorandi

Gubiani Donatella
Dip. di Scienze
Università degli Studi "G.d'Annunzio"
gubiani(at)sci.unich.it
Peretti Pamela
Dip. di Scienze
Università degli Studi "G.d'Annunzio"
peretti(at)sci.unich.it
Santini Francesco
IMT MT Lucca Institute for Advanced Studies
francesco.santini(at)imtlucca.it

Personale non strutturato

Trubitsyna Irina
DEIS
Università della Calabria
irina(at)deis.unical.it

Tecniche di Astrazione, Concorrenza e Vincoli Soft per Sicurezza Informatica e studio di Sistemi Informatici

La proposta di ricerca ha come scopo lo studio di sistemi ed applicazioni nei campi della sicurezza informatica, e nell’analisi e valutazione del rischio in sicurezza. Ci proponiamo più in dettaglio i seguenti obiettivi:

Estensione del framework dei Vincoli Soft
Il framework dei vincoli basati su semiring (semiring-based CSP (SCSP)) è capace di rappresentare molte classi di vincoli soft (fuzzy, pesati, probabilistici, multicriteria, ...), a seconda del significato dato ai valori associati ad ogni tupla (interpretati come livelli di preferenza, di importanza o costi). I vincoli soft basati su semiring sono così chiamati perchè basati proprio su una sottostante struttura di semiring che definisce l’insieme delle preferenze, l’ordinamento tra queste e la modalità di combinarle. Questo concetto è molto generale e può essere istanziato al fine di ottenere molte delle classi di vincoli soft già proposte, i loro algoritmi di risoluzione e anche di nuovi.
Tuttavia, il framework, pur ricco, non è sufficiente quando deve essere rappresentato non solo ciò che l’utente desidera ma anche ciò che non desidera. Inoltre il framework necessita ancora molto studio riguardo agli algoritmi risolutivi.
Risultati attesi:
Ci si propone di arricchire la struttura di semiring sia dal punto di vista dell’insieme di preferenze (in modo da rappresentare non solo valori positivi per ciò che l’utente desidera ma anche negativi per ciò che l’utente non desidera), che dal punto di vista degli operatori.
In particolare saranno introdotti altri operatori (con semantica in qualche modo opposta agli operatori “+” e “x”) che saranno utili per introdurre l’uso dì vincoli soft in nuovi ambiti applicativi. Un ambito di particolare interesse sembra quello dei Data Base a vincoli. Qui un operatore opposto al “+” sembra necessario per estendere al caso soft la nozione di differenza insiemistica.
Ci si propone anche di studiare e modificare vari algoritmi risolutivi usati nel caso dei vincoli classici e verificare la loro applicazione nel caso di vincoli soft.

+ torna su
Vincoli Soft per l’analisi di sistemi con sicurezza multilivello
La sicurezza di una rete è basata non solo sulla sicurezza delle sue componenti e delle interconnessione dirette tra loro, ma anche sulla potenziale possibilità che i sistemi possono avere di interoperare indirettamente attraverso le connessioni di rete. Tale possibilità può infatti potenzialmente creare dei “cascading path” che violano la sicurezza dei sistemi attraverso le connessioni di rete. In è mostrato come la programmazione con vincoli fornisce un approccio naturale per esprimere i vincoli necessari per assicurare la sicurezza multilivello attraverso la rete. In particolare i vincoli soft possono essere usati per evidenziare ed eliminare i cascading path nella rete che violano la sicurezza.
L’approccio con vincoli soft sembra fornire un avanzamento rispetto alle tecniche usate per risolvere questo problema. La ricerca attualmente studia come evidenziare i “cascading paths” e come eliminarli riconfigurando la rete. Se evidenziare il problema può essere fatto facilmente, l’eliminazione delle vuulnerabilità eliminando il minimo numero di connessioni e’ un problema NP-completo.
Usando la programmazione con vincoli soft e’ possibile evidenziare l’insieme di tutti i cascading path e quindi ottenere una soluzione minimale (anche se non ottima) in tempo polinomiale.
Risultati attesi
Il modello a vincoli può fornire una descizione naturale di una arbitraria rete a sicurezza multilivello. Ogni soluzione del modello rappresenta un cascading path nella rete fornendo molte più informazioni sulle vulnerabilità degli approcci classici e fornendo informazioni per la loro eliminazione.
Usando un modello a vincoli possiamo utilizzare le tecniche risolutive sviluppate in questo campo per trovare l’insieme dei cascading path con uno sforzo ragionevole, e quindi eliminare il problema in tempo polinomiale.
Ci proponiamo di applicare la tecnologia a vincoli ad alcuni casi reali, iniziando alcune collaborazioni con società interessate. Siamo in trattativa per collaborazioni su questi argomenti.

+ torna su
Analisi Quantitativa di Politiche di Integrità
Una politica di integrità definisce le situazioni in cui le modifiche alle informazioni sono autorizzate e attuate dai meccanismi di sicurezza del sistema. In complessi sistemi applicativi è però possibile che una politica di integrità sia specificata in maniera non corretta e, come conseguenza, un utente sia autorizzato a modificare informazioni che possono portare ad una inattesa compromissione del sistema. In [6, 7] è stata proposta una tecnica quantitativa scalabile che usa la risoluzione di vincoli per modellare ed analizzare l'efficacia delle politiche di integrità di un sistema applicativo.
Risultati attesi
Piuttosto che tentare di modellare il comportamento completo del sistema e dell'infrastruttura, nell'approccio basato su vincoli, solo quei componenti che sono considerati rilevanti per la politica di sicurezza hanno bisogno di essere modellati imponendo dei vincoli sulle parti del sistema rilevanti per la sicurezza. In questa maniera è possibile risolvere la consistenza delle politiche di sicurezza come un problema di soddisfazione di vincoli. Inoltre, usando vincoli soft diventa possibile effettuare un'analisi quantitativa delle policy.
Un'analisi quantitativa fornisce una misura a grana fine di quanto sia sicuro un sistema, piuttosto che utilizzare una misura grossolana (vero/falso) fornita dai convenzionali vincoli 'crisp'.

+ torna su
Analisi Quantitativa di Protocolli di Sicurezza
I protocolli di sicurezza prescrivono la maniera in cui i soggetti remoti presenti su una rete di computer devono interagire per ottenere specifici obiettivi di sicurezza. Un obiettivo principale dei protocolli è la confidenzialità, che garantisce che un messaggio rimane incomprensibile a soggetti "maliziosi". Un altro obiettivo cruciale è l'autenticazione, che garantisce la partecipazione di un soggetto ad una sessione di protocollo. Questi obiettivi sono formalizzati con una semplice alternativa si/no nella letteratura esistente. In questa maniera è possibile solo affermare se una chiave è confidenziale oppure no, o se un soggetto si autentica con un altro oppure no.
D'altro canto, l'esperienza mostra che la sicurezza nel mondo reale è basata su livelli di sicurezza piuttosto che su garanzie categoriche e definitive di sicurezza. In particolare, i livelli di sicurezza caratterizzano gli obiettivi di confidenzialità e di autenticazione di un protocollo. In riferimento al primo di questi obiettivi, ricordiamo che messaggi diversi richiedono specifici livelli di protezione contro la divulgazione [21].
Ad esempio, una password di un utente richiede un livello di protezione maggiore di una chiave di sessione, che viene usata per una sola sessione di protocollo. Intuitivamente, una password dovrebbe essere "più confidenziale" di una chiave di sessione. Inoltre, un attacco alla confidenzialità basato su criptoanalisi online non dovrebbe essere imputato al design del protocollo. E' abbastanza sorprendente che gli obiettivi di confidenzialità e di autenticazione di un protocollo siano formalizzati con una semplice alternativa si/no nella letteratura esistente.
Risultati attesi
La motivazione della nostra ricerca è lo sviluppo di una nozione quantitativa degli obiettivi di sicurezza (confidenzialità, autenticazione, delega, ecc.). Ci proponiamo inoltre di estendere il nucleo esistente [3, 2], e di dimostrare la validità della nostra idea su protocolli largamente diffusi (come abbiamo fatto per Kerberos, ad esempio). In Kerberos, la nostra analisi preliminare del protocollo evidenzia il fatto che la perdita di una chiave di autorizzazione sarebbe più grave della perdita di una chiave di servizio, e che l'autenticazione del responder con l'initiator è più debole dell'autenticazione dell'initiator con il responder.
Il prossimo passo sarà la meccanizzazione del framework. Infatti, poiché abbiamo a che fare esclusivamente con quantità illimitate ma finite, il framework può essere automatizzato utilizzando il model checking.

+ torna su
Verifica di Protocolli di Sicurezza
Ci si propone di studiare i vantaggi e gli svantaggi derivanti dall’applicazione di tecniche basate sulla programmazione logica con vincoli all’analisi, la specifica, la verifica e l’attuazione di proprietà di sicurezza in sistemi multiagente.
Particolare attenzione sarà posta sulla specifica e sullo studio di politiche di autorizzazione in ambienti distribuiti attraverso l’uso dei vincoli.
Risultati attesi
Ci si propone di ottenere risultati teorici e sperimentali riguardo l’uso della programmazione logica con vincoli come framework per la costruzione e la validazione di modelli di autorizzazione distribuiti in sistemi multiagente.
In particolare, concentreremo la nostra attenzione sui problemi che nascono dalla composizione e dall’interoperabilita’ tra politiche di autorizzazione appartenenti ad organizzazioni diverse.

+ torna su
Completezza dei domini astratti per la verifica di protocolli di sicurezza
Un protocollo di sicurezza ([36]) è un metodo per trasmettere informazioni attraverso la rete. Il ruolo principale dei protocolli di sicurezza è di garantire l’autenticità e la segretezza della comunicazione.
Altre proprietà richieste possono riguardare il riconoscimento o l’integrità del sistema. I metodi comunemente utilizzati per analizzare le proprietà di sicurezza sono basati sul controllo del flusso di informazione. L’idea è di partizionare l’informazione in classi di sicurezza e di garantire che non vi siano flussi di informazione tra le varie classi. Questo problema viene tipicamente risolto fissando una logica particolare o un type system, oppure utilizzando tecniche di model checking basate sulla semantica operazionale.
Risultati attesi
Noi vogliamo fornire delle tecniche formali per la progettazione sistematica di domini astratti orientati alle proprietà di sicurezza, e quindi di rendere applicabili le tecniche di trasformazione dei domini [32] all’analisi dei protocolli di comunicazione. Le tecniche di trasformazione dinamica del dominio di analisi giocano un ruolo chiave nel caso delle proprietà di sicurezza, dove non è sufficiente dimostrare che il sistema soddisfi una certa specifica (correttezza dell’analisi) bensì deve essere garantito che il protocollo resista agli attacchi. La novità introdotta è l’inferenza attiva dell’ambiente circostante, che rende necessario l’utilizzo di tecniche dinamiche di modifica dell’analisi, in accordo all’evoluzione dell’ambiente. Si intendono quindi definire ed implementare delle operazioni di trasformazione dei domini (raffinamenti e semplificatori) per la progettazione di analisi ottimali (con il migliore tradeoff tra la complessità computazionale e la precisione dell’analisi). Esempi di analisi ottimali basate su varie logiche sono gi state considerate in molte applicazioni dell’interpretazione astratta (vedi, ad esempio, [37, 38]).
La stessa idea può essere estesa all’analisi di sicurezza, sfruttando le strutture logiche alla base delle specifiche dei protocolli.

+ torna su
Metodologia di analisi uniforme
Le metodologie utilizzate per analizzare i protocolli di sicurezza e le politiche di integrità sono differenti ma strettamente correlate. Da una parte c'à la nozione di "ambiente" dentro la quale la politica viene implementata, dall'altra c'è l'attaccante che mira a violare il protocollo. L'idea base da usare per integrare i due approcci è quella di considerare, in entrambi i framework, la nozione di "modello ideale" che rappresenta la corretta configurazione della politica e la corretta esecuzione del protocollo. Si tratterà poi di confrontare la poltica e la "implementazione" del protocollo con tale modello.
Risultati attesi
Abbiamo in mente di sviluppare un approccio uniforme allo studio degli attacchi ai protocolli di sicurezza e dei bug sulle politiche di integrità. Pensiamo anche di svuluppare una implementaione che sarà utile per controllare automaticamente protocolli e politiche rispetto a questa nuova nozione di sicurezza. Pensiamo di partire da una lista di protocolli di sicurezza e da un insieme di politiche, da utilizzare come test per la nostra teoria.
E` importante sottolineare che la metodologia proposta potrebbe riconoscere nuovi bug, e dare una misura a bug o attacchi già noti.
In particolare, le nozioni di “attack detection”, “attack suspicion” e “attack retaliation” saranno studiate in dettaglio.

+ torna su
Analisi di rischi di sicurezza e tradeoff tra privacy ed efficienza
Una importante nuova area di ricerca è collegata alla analisi di rischio di sicurezza. Pensiamo di usare i vincoli soft per rappresentare le attività che necessitano di protezione e le minacce che potrebbero causare dei danni.
L'uso di vincoli soft è necessario per rappresentare il "costo" associato a ogni specifica minaccia o attività. Inoltre, la probabilità delle varie minacce deve essere presa in considerazione. Una volta che il sistema è stato modellato, la nozione di tradeoff [15,10] potrebbe essere usata per modificare parzialmente la configurazione del sistema.
Un'altra preoccupazione è la privacy. Durante l'esecuzione, un agente potrebbe non voler rivelare troppa informazione. Pertanto, si viene a creare un tradeoff, potenzialmente importante, tra la tutela della privacy e il potenziamento dell'efficienza della ricerca. In questo lavoro, mostriamo come misure quantitative della perdita di privacy posso essere fatto all'interno del framework del soddisfacimento di vincoli distribuito.
Risultati attesi
Vogliamo mostrare come gli agenti posso fare inferenze sui problemi o sottoproblemi di altri agenti a partire da comunicazioni che non trasportano nessuna informazione privata in maniera esplicita. Ciò può avvenite usando dei ragionamenti basati su vincoli, in un framework costituito da un CSP ordinario, che è noto solo parzialmente, e un sistema di CSP ombra che rappresentano varie forme di conoscenza probabilistica. Questo tipo di ragionamento, combinato con l'elaborazione della consistenza degli archi, può velocizzare la ricerca sotto condizioni di comunicazione limitata, allo stesso tempo compromettendo la tutela della privacy. In alcuni casi, un piccola quantità di informazione privata è richiesta per migliorare l'efficienza della ricerca; con l'uso di euristiche più sofisticate, la ricerca può essere migliorata anche sotto condizioni di comunicazione minimale. Allo stesso tempo, questi metodi consentono, talvolta, di inferire informazioni nascoste, sollevando nuove problematiche riguardanti la privacy.
In quest'area pensiamo di intraprendere una notevole mole di lavoro. Vorremmo creare un modello per rappresentare sia informazione di sicurezza che aspetti economici (tipicamente il costo della minaccia e il costo delle patch o delle contromisure di sicurezza). In questo contesto, la teoria della probabilità e la teoria delle possibilità saranno usate per trattare il problema dell'incertezza.

+ torna su

PROGETTO DELL'UNITÀ DI RICERCA - Modello B

RENDICONTO DELL'UNITÀ DI RICERCA - Modello C