What's the Over/Under? Probabilistic Bounds on Information Leakage

TL;DR

This paper enhances probabilistic information flow analysis by combining sampling and symbolic execution to improve scalability while maintaining precision and soundness in leakage estimation.

Contribution

It introduces a scalable approach that augments existing techniques with sampling and symbolic execution, ensuring no underestimation of information leakage.

Findings

Achieves similar precision to baseline methods

Significantly improves analysis performance

Ensures soundness with no leakage underestimation

Abstract

Quantitative information flow (QIF) is concerned with measuring how much of a secret is leaked to an adversary who observes the result of a computation that uses it. Prior work has shown that QIF techniques based on abstract interpretation with probabilistic polyhedra can be used to analyze the worst-case leakage of a query, on-line, to determine whether that query can be safely answered. While this approach can provide precise estimates, it does not scale well. This paper shows how to solve the scalability problem by augmenting the baseline technique with sampling and symbolic execution. We prove that our approach never underestimates a query's leakage (it is sound), and detailed experimental results show that we can match the precision of the baseline technique but with orders of magnitude better performance.