Language-based information flow security has been longly studied during the last decades. Proving that a program enforces noninterference has been the goal of several static analyses. Nevertheless, despite this deep and extensive work, its practical applications have been relatively poor. Usually these approaches work on an ad-hoc programming language, and they do not support mainstream languages. This means that one should completely rewrite a program in order to apply them to some existing code. In this paper, we introduce Sails, a new tool that combines Sample, a generic static analyzer, and an existing information leakage analysis. This tool does not require to modify the original language, since it works with mainstream languages like Java, and it does not require any manual annotation. Sails can combine the information leakage analysis with different heap abstractions, inferring information leakage over programs dealing with complex data structures. We applied Sails to the analysis of the SecuriBench-micro suite. The experimental results show the effectiveness of our approach.
SAILS: Static Analysis of Information Leakage with Sample
ZANIOLI, Matteo;FERRARA P.;CORTESI, Agostino
2012-01-01
Abstract
Language-based information flow security has been longly studied during the last decades. Proving that a program enforces noninterference has been the goal of several static analyses. Nevertheless, despite this deep and extensive work, its practical applications have been relatively poor. Usually these approaches work on an ad-hoc programming language, and they do not support mainstream languages. This means that one should completely rewrite a program in order to apply them to some existing code. In this paper, we introduce Sails, a new tool that combines Sample, a generic static analyzer, and an existing information leakage analysis. This tool does not require to modify the original language, since it works with mainstream languages like Java, and it does not require any manual annotation. Sails can combine the information leakage analysis with different heap abstractions, inferring information leakage over programs dealing with complex data structures. We applied Sails to the analysis of the SecuriBench-micro suite. The experimental results show the effectiveness of our approach.File | Dimensione | Formato | |
---|---|---|---|
SAC2012_zanioli.pdf
non disponibili
Tipologia:
Documento in Post-print
Licenza:
Accesso chiuso-personale
Dimensione
519.23 kB
Formato
Adobe PDF
|
519.23 kB | Adobe PDF | Visualizza/Apri |
I documenti in ARCA sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.