Article. What i write

Lo sviluppo dei servizi web, negli ultimi anni, si è concentrato sull’integrazione e il riutilizzo delle risorse e dei servizi distribuiti in rete. Questa impostazione progettuale è testimoniata dall’avvento delle Service Oriented Architecture (SOA), adatte a garantire l’interoperabilità tra molteplici sistemi software, scritti in diversi linguaggi di programmazione, ed implementati su differenti piattaforme hardware. I servizi, resi disponibili da tali sistemi, possono essere facilmente combinati e integrati tra di loro per formarne altri più complessi.

Contestualmente alla diffusione di sistemi software distribuiti, è maturata l’esigenza di disporre di meccanismi di autenticazione unica (Single Sign-On, SSO) per il controllo dell’accesso a più risorse indipendenti, ma unificate sotto uno stesso dominio applicativo.

Il Single Sign-On, mediante un server di autenticazione centralizzato, semplifica notevolmente la gestione degli accessi ai diversi servizi e permette, allo sviluppatore ed all’utente finale, di risparmiare tempo e di non doversi più preoccupare della gestione di numerose combinazioni e policy di credenziali (username e password).

In questo scenario il servizio di autenticazione centralizzato diventa particolarmente critico dal punto di vista dell’affidabilità, p.e. la mancata disponibilità del servizio impedirebbe l’accesso a tutte le risorse appartenenti ad un dato dominio, e della sicurezza, in quanto la conseguenza negativa derivante dalla compromissione delle credenziali dell’utente verrebbe amplificato, in quanto il SSO consente l’accesso a molteplici risorse.

Di conseguenza, i sistemi di Single Sign-On sono soggetti ad attacchi volti principalmente all’accesso illegittimo di risorse e servizi, ovvero all’impedimento della fruizione.

È ben noto, tuttavia, che la progettazione di protocolli di autenticazione affidabili e sicuri, a dispetto della loro apparente semplicità, è un’attività complessa e soggetta ad errori. Diversi protocolli di Single Sign-On si sono rivelati vulnerabili anche dopo anni dalla loro implementazione e pubblicazione (p.e. Kerberos versione 3 e Kerberos versione 4, e più recentemente la prima implementazione del protocollo di autenticazione di Google, basato su SAML SSO).

Talvolta gli attacchi sono resi possibili da dettagli trascurati in fase di progetto. Allo scopo di ridurre al minimo le vulnerabilità dei sistemi di autenticazione, si sta diffondendo l’uso di tecniche di verifica formale della specifica astratta dei protocolli. La comunità internazionale di ricerca nel campo dei metodi formali ha recentemente proposto diversi strumenti automatici a supporto di tale approccio. Tra i tool più maturi AVISPA è uno strumento integrato per la verifica automatica di proprietà di sicurezza di protocolli e applicazioni. Il tool fornisce il linguaggio HLPSL (High Level Protocol Specification Language) per la specifica dei protocolli ed integra diversi moduli back-end di verifica che implementano varie tecniche di analisi formale.

Lo scopo di questo lavoro è l’analisi formale con AVISPA di OpenID Connect 1.0, uno dei più recenti protocolli di Single Sign-On rilasciato nella versione standard il 24 febbraio 2014.

OpenID Connect 1.0 è un semplice “identity layer”, basato sul protocollo OAuth 2.0, che permette ai Client di verificare l'identità dell’End-User attraverso l’autenticazione eseguita da un Authorization Server, nonché di ottenere informazioni di base dell’End-User stesso.

OpenID Connect consente a qualsiasi tipo di Client, compresi i client Web- based, mobile e JavaScript, di richiedere e ricevere informazioni sulle sessioni autenticate e gli utenti finali. La specifica della suite è estensibile, permettendo ai partecipanti di utilizzare le funzioni opzionali come la crittografia dei dati d’identità, la scoperta dei fornitori di OpenID e la gestione della sessione. Essendo un sistema SSO recente è possibile che presenti delle vulnerabilità ancora sconosciute.

Il lavoro è strutturato come segue. Nel Capitolo 1 verrà presentato AVISPA: dopo una breve descrizione comprensiva d’esempi del linguaggio HLPSL, saranno illustrate le proprietà dei back-end attualmente integrati. Il Capitolo 2 offrirà una presentazione informale di OpenID Connect. Il lavoro di analisi del protocollo sarà illustrato in dettaglio nel Capitolo 3. In primo luogo verrà introdotta una formalizzazione in notazione Alice-Bob del protocollo di OpenID Connect. Successivamente sarà fornita la specifica HLPSL corrispondente, sulla quale verrà condotta l’analisi automatica di diverse proprietà di sicurezza. Il protocollo nella sua formulazione base, come si vedrà, è vulnerabile all’intercettazione delle informazioni di autenticazione di sessione. Pertanto, alla luce delle considerazioni sulla sicurezza, verrà proposta una soluzione arricchita per rimuovere il bug rilevato. Infine, nel ultimo Capitolo saranno esposte le conclusioni ed alcune considerazioni in merito ai possibili sviluppi futuri del lavoro presentato.