RICERCA ITALIANA     

SOFT - Tecniche formali orientate alla sicurezza

Università "Ca' Foscari" di Venezia

Abstract

La sicurezza dei sistemi software è una questione cruciale in un mondo sempre più permeato dall'Information Technology. Il numero di servizi, accessibili via reti di natura telematica, che aiutano ad affrontare attività quotidiane va aumentando, come testimoniato dal sempre crescente numero di espressioni come e-banking, e-commerce ed e-government, ove il prefisso 'e' ne sostanzia la dimensione elettronica. Tali servizi richiedono sia lo scambio di informazioni confidenziali che la condivisione di risorse computazionali e presentano forti requisiti di sicurezza, data la grande rilevanza delle informazioni trattate e il contesto fortemente distribuito e insicuro, quale è Internet, in cui esse tipicamente operano. Si rivela importante, ad esempio, stabilire l'autenticità dei messaggi scambiati, la loro segretezza, le identità delle parti in causa, e anche avere garanzie che le diverse componenti del sistema interagiscano correttamente, senza violare le proprietà desiderate.
D'altra parte autorevoli enti, come il CERT della Carnegie Mellon University, riportano un numero sempre crescente di segnalazioni relative alla vulnerabilità dei sistemi informatici, spesso dovute a problemi nella progettazione e realizzazione del software. La soluzione tipica è quella di riparare tali "falle" rendendone più difficile l'utilizzo da parte degli attaccanti, ma questo approccio non va certamente alla radice del problema. Un approccio >>>

Coordinatore Scientifico del Programma di Ricerca

Riccardo Focardi Università "Ca' Foscari" di VENEZIA

Obiettivo del Programma di Ricerca

La sicurezza dell'informazione è un tema sempre più attuale e rilevante, dato il crescente utilizzo di elaboratori e di reti per applicazioni critiche quali il commercio elettronico, l'home banking, l'acquisto di beni digitali e la fruizione, in genere, di servizi in linea. Diventa quindi sempre più importante capire a fondo i requisiti di sicurezza delle attuali applicazioni distribuite, e studiare metodi per la verifica automatica di tali requisiti.
Lo scopo principale del progetto SOFT è lo studio dei fondamenti della sicurezza informatica e lo sviluppo di metodi formali per la specifica e verifica di proprietà di sicurezza di programmi, sistemi e reti di elaboratori. SOFT comprende 3 Università con 11 ricercatori permanenti, 10 tra dottorandi, assegnisti e post-doc, 2 ricercatori di un ateneo estero e 2 contratti di 6-8 mesi specificatamente richiesti sul programma di ricerca, per un totale di 25 ricercatori. Le unità di ricerca sono caratterizzate da forti competenze su metodi formali per la sicurezza, analisi statica, interpretazione astratta, verifica di proprietà di programmi e semantica della concorrenza. La presenza, inoltre, di due ricercatori della Saarland University di Saarbrücken, e di un dottorando in co-tutela con la Ecole Polytechnique di Palaiseau dimostrano un'apertura verso importanti gruppi di ricerca europei nel settore.
Intendiamo operare a largo spettro su diverse problematiche di sicurezza lavorando sia su propriet >>>

Risultati parziali attesi

Indichiamo, nel seguito, i principali risultati attesi per ogni work-package. Tali risultati sono volutamente molto specifici in modo da poter essere verificati, e costituiranno, quindi, lo strumento primario per la valutazione dell'avvenuto raggiungimento degli obiettivi del progetto. L'interesse per l'avanzamento della conoscenza è stato illustrato in modo estensivo nelle sezioni 12 e 13.

Risultati attesi WP1

Fase 1
- nuovi modelli formali per il trust nelle reti ad-hoc ed integrazione di tali modelli in calcoli di processi.
Fase 2
- una nuova logica temporale per esprimere proprietà di sicurezza di agenti comunicanti.
Fase 3
- definizione di un'interpretazione astratta di protocolli di autenticazione sfida-risposta;
- definizione di nuove analisi control-flow per protocolli di sicurezza;
- estensione del tool presentato in [BBDNN05] alle nuove analisi control-flow;
- utilizzo di tecniche simboliche e di raffinamento per la verifica di proprietà di sicurezza;
- estensione di AVISPA alla logica descritta in fase 2;
- studio di altre possibili estensioni di AVISPA a tecniche sviluppate in questo WP.


Risultati attesi WP2

Fase 1
- definizione di linguaggi imperativi orientati alla sicurezza con primitive di comunicazione crittografiche;
- nuove primitive astratte di comunicazione che permettano di rendere la >>>

Durata

24 mesi

Base di partenza scientifica nazionale o internazionale

Il progetto SOFT si occuperà di diverse tematiche relative ai metodi formali per la sicurezza che introduciamo, nel seguito, menzionando per ognuna di esse i principali risultati presenti in letteratura. Per facilitare la connessione con gli obiettivi del progetto, le tematiche sono state raggruppate in base all'attinenza con i quattro work-package.

- Sicurezza delle Reti di Comunicazione

I protocolli crittografici sono uno degli strumenti fondamentali per garantire sicurezza sulle reti di elaboratori. Nel momento in cui la rete di comunicazione è di grandi dimensioni, e quindi non controllabile localmente, risulta infatti necessario proteggere le informazioni in transito sulla rete tramite tecniche crittografiche. Nonostante le ridottissime dimensioni del codice, tali protocolli sono spesso soggetti ad attacchi in grado di sovvertire la logica del protocollo invalidandone le proprietà di sicurezza attese, senza necessariamente attaccare i sottostanti meccanismi crittografici. Esiste una sconfinata letteratura sull'analisi e verifica di protocolli crittografici, ma solo un piccolo sottoinsieme di tali lavori è basato sull'analisi statica (language-based). In [A99,AB05], ad esempio, viene studiata la segretezza dell'informazione e in [BBDNN05, BFM07, GJ04] l'autenticazione tramite sistemi di tipi e analisi control-flow. Intendiamo approfondire lo studio di tali tecniche focalizzando l'attenzione >>>