Combining symbolic and numerical domains for information leakage analysis

We introduce an abstract domain for information-flow analysis of software. The proposal combines variable dependency analysis with numerical abstractions, yielding to accuracy and efficiency improvements. We apply the full power of the proposal to the case of database query languages as well. Finally, we present an implementation of the analysis, called Sails, as an instance of a generic static analyzer. Keeping the modular construction of the analysis, the tool allows one to tune the granularity of heap analysis and to choose the numerical domain involved in the reduced product. This way the user can tune the information leakage analysis at dierent levels of precision and efficiency