View this PageEdit this PageUploads to this PageHistory of this PageTop of the SwikiRecent ChangesSearch the SwikiHelp Guide

Automatic Discovery and Quantification of Information Leaks

Andrey Rybalchenko
Max Planck Institute for Software Systems, Saarbruecken, Germany

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
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.