Information flow analysis by abstract interpretation

Abstract

Protecting the confidentiality of information stored in a computer system or transmitted over a public network is a relevant problem in computer security. The goal of this thesis is to provide both theoretical and experimental results towards the design of an information flow analysis for the automatic verification of absence of sensitive information leakage. Our approach is based on Abstract Interpretation, a theory of sound approximation of program semantics. We track the dependencies among program's variables using propositional formulae, namely the Pos domain. We study the main ways to improve the accuracy (by combination of abstract domains) and the efficiency (by combination of widening and narrowing operators) of the analysis. The reduced product of the logical domain Pos and suitable numerical domains yields to an analysis strictly more accurate with respect to the ones already in the literature. The modular construction of our analysis allows to deal with the trade-off between efficiency and accuracy by tuning the granularity of the abstraction and the complexity of the abstract operators. Finally, we introduce Sails, a new information flow analysis tool for mainstream languages like Java, that does not require any manual annotation. Sails combines the information leakage analysis with different heap abstractions, inferring information leakage over programs dealing with complex data structures too. We applied Sails to the analysis of the SecuriBench-micro suite and the preliminary experimental results outline the effectiveness of our approach.

Proteggere la segretezza delle informazioni nei sistemi informatici o all’interno di reti pubbliche `e uno dei principali problemi riguardanti la sicurezza informatica. L’obiettivo di questa tesi è fornire sia risultati teorici che sperimentali attraverso la progettazione di un’analisi di flussi di informazioni volta a verificare che i dati sensibili rimangano tali e non vengano resi pubblici. Il nostro approccio si fonda sull’Interpretazione Astratta, una teoria riguardante l’approssimazione della semantica dei programmi. Tracciamo le dipendenze tra le variabili attraverso formule proposizionali, in particolare usando il dominio Pos. Analizziamo i principali metodi per incrementare la precisione (tramite la combinazione di domini astratti) e l’efficienza (tramite l’utilizzo degli operatori di widening and narrowing) dell’analisi. Il prodotto ridotto tra il dominio logico Pos ed opportuni domini numerici fornisce un analisi più accurata rispetto quelle presenti in letteratura. La costruzione modulare della nostra analisi permette di gestire al meglio il trade-off tra efficienza e precisione regolando la granularità dell’astrazione e la complessità degli operatori astratti. In fine, introduciamo Sails, un nuovo strumento per l’analisi di flussi di informazioni per linguaggi tradizionali come Java, che non richiede nessuna annotazione manuale. Sails combina l’analisi dei flussi con differenti astrazioni dell’heap, inferendo i flussi anche su programmi che utilizzano strutture dati complesse. Abbiamo poi analizzato con Sails la suite SecuriBench-micro ottenendo dei risultati preliminari che hanno confermato l’efficacia del nostro approccio.

Protéger la confidentialité de l’information numérique stockée ou en transfert sur des réseaux publics est un problème récurrent dans le domaine de la sécurité informatique. Le but de cette thèse est de fournir des résultats théoriques et expérimentaux sur une analyse de flue permettant la vérification automatique de l’absence de fuite possible d’information sensible. Notre approche est basée sur la théorie de l’Interprétation Abstraite et consiste à manipuler une approximation de la sémantique des programmes. Nous détectons les différentes dépendances entre les variables d’un programme en utilisant des formules propositionnelles avec notamment le domaine Pos. Nous étudions les principales façon d’améliorer la précision (en combinant des domaines abstraits) et l’efficacité (en associant des opérateurs d’élargissement et de rétrécissement) de l’analyse. Le produit réduit du domaine logique Pos et d’un domaine numérique choisi permet une analyse strictement plus précise que celles précédemment présentent dans la littérature. La construction modulaire de notre analyse permet de choisir un bon compromis entre efficacité et précision en faisant varier la granularité de l’abstraction et la complexité des opérateurs abstraits. Pour finir, nous introduisons Sails une nouvelle analyse de flue destinée à des langages de haut niveau sans annotation tel que Java. Sails combine une analyse de fuite possible d’information à différentes abstraction de la mémoire (du tas), ce qui lui permet d’inférer des résultats sur des programmes manipulant des structures complexes. De premiers résultats expérimentaux permettent de pointer l’efficacité de notre approche en appliquant Sails à l’analyse de SecuriBench-micro.