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. Importante si rivela, 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 complementare è, invece, quello di modellare e verificare i requisiti di sicurezza fin dalla specifica di un sistema software, al fine di ridurre al minimo le vulnerabilità sul prodotto finale. L'adozione di tecniche formali può quindi giocare un ruolo molto importante per individuare possibili problemi di sicurezza fin dalle prime fasi di sviluppo e progettazione, per capirne a fondo le cause e per rimuoverli prima che altre scelte progettuali ci costringano a "inventare" rimedi a posteriori, non sempre possibili e soddisfacenti. L'interesse nei metodi formali per la sicurezza è comprovato da una comunità internazionale sempre più attiva, e dal numero crescente di nuovi workshop e
conferenze internazionali su tale tema. Lo scopo di questo progetto è di creare un consorzio formato da 4 università già attive nel campo dei metodi formali per la sicurezza, dell'interpretazione astratta e della verifica di programmi, e focalizzare le proprie energie su obiettivi comuni di ricerca. Si intende operare a largo spettro su diverse problematiche di sicurezza, focalizzando principalmente l'attenzione su tecniche di verifica statiche a livello di linguaggio, che permettano di comprendere e verificare la sicurezza a partire dalla specifica o dal codice di un programma, senza la necessità di analizzarne l'esecuzione. Riteniamo, infatti, che questo approccio sia particolarmente promettente, sia perché si presta ad essere automatizzato tramite algoritmi di verifica efficienti sia per la migliore comprensione degli obiettivi e dei meccanismi di sicurezza che esso fornisce già a livello di specifica o di programmazione. Ci occuperemo sia di proprietà di "alto livello", come il controllo dei flussi di informazione, l'autenticazione e il controllo degli accessi, sia su proprietà di livello più "basso", come il buffer overflow, gli errori nella formattazione di stringhe ed altri errori relativi all'allocazione e deallocazione della memoria, proprietà alla radice di molte vulnerabilità di sistemi software reali.