Abstract Model Counting: A Novel Approach for Quantification of Information Leaks
View/ Open
Pagination
283 - 292 (9)
Publisher
Publisher URL
ISBN-13
978-1-4503-2800-5
DOI
10.1145/2590296.2590328
Metadata
Show full item recordAbstract
We present a novel method for Quantitative Information Flow analysis. We show how the problem of computing information leakage can be viewed as an extension of the Satisfiability Modulo Theories (SMT) problem. This view enables us to develop a framework for QIF analysis based on the framework DPLL(T) used in SMT solvers. We then show that the methodology of Symbolic Execution (SE) also fits our framework. Based on these ideas, we build two QIF analysis tools: the first one employs CBMC, a bounded model checker for ANSI C, and the second one is built on top of Symbolic PathFinder, a Symbolic Executor for Java. We use these tools to quantify leaks in industrial code such as C programs from the Linux kernel, a Java tax program from the European project HATS, and anonymity protocols