Verso la validazione automatica della sicurezza delle architetture orientate ai servizi

AVANTSSAR (Automated Validation of Trust and Security of
Service-Oriented Architectures) e` un progetto STREP triennale da me
coordinato nell'ambito del Settimo Programma Quadro della Commissione
Europea.
Lo scopo di questo seminario e` duplice: sia illustrare i principali
risultati conseguiti nella prima meta` di vita di AVANTSSAR sia
presentare i piu` significativi risultati di ricerca che ho ottenuto
nei miei primi 3 anni qui a Verona.
Dopo una breve introduzione ai problemi di sicurezza che si presentano
nelle architetture orientate ai servizi, illustrero` alcuni casi di
studio (quali Single-Sign-On SSO e Car Registration Office) che
dimostrano la necessita` di avere a disposizione una tecnologia per la
specifica formale e la validazione automatica di questo tipo di
problemi. Descrivero` quindi diversi metodi di analisi formale che ho
contribuito a sviluppare e implementare, e la loro applicazione a
questi casi di studio. In particolare, presentero` le tecniche che
stanno alla base di uno strumento automatico, chiamato Open-source
Fixed-point Model Checker OFMC, per l'analisi simbolica di protocolli
per la sicurezza, mostrando, inoltre, come sia possibile creare e
combinare canali di comunicazione sicuri sui quali gli utenti
trasmettono messaggi in maniera esplicita oppure anonima.