Qualche giorno fa è rimbalzata per la rete la notizia che l’Università di Genova ha scoperto ed aiutato a correggere una falla nel protocollo di autenticazione dei servizi di Google. La notizia ha una portata tale che Google stessa ha aggiunto il gruppo di ricercatori alla propria “thank you page“, quindi per approfondire abbiamo raggiunto Alessandro Armando, ingegnere elettronico, docente di intelligenza artificiale e sicurezza informatica e coordinatore del laboratorio di IA nell’ateneo genovese.
Professore, il progetto all’interno del quale è stata fatta la scoperta si chiama Avantssar, di cosa si tratta?
Avantssar ha l’obiettivo di arrivare a una specifica formale per un sistema di validazione automatizzata delle architetture di sicurezza, da integrare in un tool che si chiamerà Avantssar Validation Platform. È un progetto cofinanziato dall’Unione Europea cui l’università di Genova partecipa tramite il proprio laboratorio di intelligenza artificiale e che annovera tra i partner anche grandi nomi dell’industria informatica, come Ibm, Sap e Siemens.
Perché Google? è stato un caso o una prova deliberata?
Entrambe. Uno dei casi studio proposti alla UE quando presentammo il progetto era l’analisi degli standard Oasis, in particolare della sua implementazione Saml. Questo standard di autenticazione è attualmente implementato anche da alcuni dei partner del progetto. Abbiamo analizzato per mesi il Single Sign On nelle implementazioni Oasis e non abbiamo rilevato nulla da segnalare, fino a quando non ci siamo imbattuti nella versione che Google utilizza in Google Apps, che è leggermente differente dallo standard dettato dal consorzio. Google stessa fornisce un prototipo della sua versione per facilitarne l’adozione da parte dei clienti, l’abbiamo studiata e data in pasto al nostro tool e così abbiamo scoperto la vulnerabilità.
In cosa consisteva la vulnerabilità?
Nel fatto che all’interno di uno dei messaggi scambiati durante l’autenticazione venivano inviati due campi in meno di quanti la parte serverside si aspettasse di ricevere, ma che comunque questo non generava nessun tipo di errore, e anzi costituiva proprio un punto debole dell’intero sistema.
Avete suggerito cosa modificare nel codice?
No, noi abbiamo segnalato loro il problema, perché comunque la parte serverside la conosce solo Google, dopodiché hanno fatto delle modifiche e hanno pubblicato una versione temporanea, chiedendoci di rianalizzare la falla, che a quel punto risultava corretta. Soltanto allora la modifica è andata in produzione e la notizia è stata comunicata.
Ha detto che Oasis era solo il primo dei casi studio che avete in programma…
Si, questo significa che da qui al 2010, anno in cui il progetto finirà, potremmo nuovamente trovarci di fronte a problemi di questo tipo con altri standard di protocolli Single Sign On e altre implementazioni. Obiettivo del progetto è anche quello di dialogare con i consorzi di standardizzazione per portare loro i risultati delle analisi e aiutarli ad evitare errori nelle specifiche future. Trovare altri bachi sarebbe comunque un modo per affinare il nostro tool di verifica.
Che tipo di strumento è questo tool per la verifica automatizzata?
È la descrizione matematica di una macchina a stati finiti e rappresenta fedelmente il protocollo di autenticazione. Per assicurarsi che il protocollo sia esente da problemi è necessario analizzare tutti gli stati, ma il numero di essi è tuttavia altissimo (l’ordine di grandezza è superiore a 10 alla 300), per cui è necessaria una intelligenza artificiale avanzata che effettui l’analisi sistematica di tutti questi stati. Il tool impiega qualche decina di minuti per svolgere il proprio compito, mentre ci vogliono interi mesi/uomo per scrivere il modello, anche se nella realtà il tool stesso aiuta a costruirlo.
Quali sono i limiti degli strumenti di verifica automatica e la loro affidabilità?
Più è grande l’applicazione e più è grande la richiesta di risorse, per cui modelli molto molto complessi potrebbero eccedere la nostra capacità di calcolo. La vera difficoltà del progetto tuttavia è la scrittura del modello formale da utilizzare nel tool, nonostante l’aiuto fornito dal tool, come dicevo prima. Però se il modello è corretto, l’affidabilità è molto alta.
