Type-based analysis of security APIs

Una security API è un'interfaccia che regola la comunicazione tra due processi, che vengono eseguiti con diversi livelli di affidabilità, allo scopo di assicurare che sia soddisfatta una determinata proprietà di sicurezza. In questo modo, un sistema potenzialmente non fidato può fruire delle funzionalità offerte da una risorsa sicura senza mettere a rischio la sicurezza dei dati in essa contenuti: la API deve infatti impedire che una delle possibili sequenze di suoi comandi permetta di usare in maniera inappropriata la risorsa fidata. Molto spesso una API di questo tipo viene progettata e sviluppata considerando quella che sarà la sua applicazione più comune e come questa utilizzerà i servizi messi a disposizione. Una mancata visione di insieme dei comandi esposti dalla API apre la strada ad un suo possibile utilizzo malevolo atto a sovvertire la sicurezza dei dati che dovrebbe proteggere. Negli ultimi anni, infatti, sono stati scoperti numerosi attacchi contro le security API esistenti. La tesi propone un'analisi, basata sui sistemi di tipi, per verificare la sicurezza di queste cruciali componenti. L'analisi formale dei linguaggi è, infatti, uno strumento molto potente per dimostrare che un dato programma soddisfa le proprietà di sicurezza richieste. Inoltre, fornisce anche un aiuto agli sviluppatori delle API per capire a fondo le cause delle vulnerabilità che le affliggono e li guida ad una programmazione consapevolmente sicura. Un attaccante che è in grado di osservare differenze nei risultati ottenuti invocando la stessa funzione di una API con diversi parametri di input, può utilizzarle per derivare informazioni sui segreti custoditi nella parte fidata del sistema. Una security API soggetta a questo genere di attacchi può essere resa sicura utilizzando una proprietà di non-interferenza. La tesi estende la teoria esistente nel campo dell'information flow security per analizzare la sicurezza di programmi che fanno uso di primitive crittografiche (sia randomizzate che deterministiche) e applica i risultati ottenuti per studiare la API impiegata per la verifica dei PIN nella rete degli sportelli ATM (bancomat). Utilizzando il sistema di tipi proposto, è stato possibile proporre e verificare una soluzione che rende sicura tale API. Una security API che, come risultato di una inaspettata sequenza di comandi, rivela una informazione che dovrebbe rimanere segreta, può essere invece analizzata con un sistema di tipi atto a controllare che la segretezza dei dati sia preservata durante tutto il tempo di esecuzione dei programmi. La tesi presenta il caso di programmi che offrono servizi per la gestione delle chiavi crittografiche, introducendo un sistema di tipi in grado di ragionare sulla sicurezza dello standard RSA PKCS\#11 e di verificare la correttezza di una nuova patch che lo rende sicuro.