Automatic Discovery and Quantification of Information Leaks
Andrey Rybalchenko
Max Planck Institute for Software Systems, Saarbruecken, Germany
http://www.mpi-sws.org/~rybal/
Information-flow analysis is a powerful technique for reasoning about
the sensitive information exposed by a program during its execution.
We present the first automatic method for information-flow analysis
that discovers what information is leaked and computes its
comprehensive quantitative interpretation. The leaked information is
characterized by an equivalence relation on secret artifacts, and is
represented by a logical assertion over the corresponding program
variables. Our measurement procedure computes the number of discovered
equivalence classes and their sizes. This provides a basis for
computing a set of quantitative properties, which includes all
established information-theoretic measures in quantitative
information-flow.
Our method exploits an inherent connection between formal models of
qualitative information-flow and program verification techniques. We
provide an implementation of our method that builds upon existing tools
for program verification and information-theoretic analysis. Our
experimental evaluation indicates the practical applicability of the
presented method.
Joint work with Boris Koepf and Michael Backes.