Computing Information Flow Using Symbolic Model-Checking

International audienceSeveral measures have been proposed in literature for quantifying the information leaked bythe public outputs of a program with secret inputs. We consider the problem of computinginformation leaked by a deterministic or probabilistic program when the measure of informationis based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing thesemeasures is that we need the total number of possible outputs and, for each possible output, thenumber of inputs that lead to it. A direct computation of these quantities is infeasible because ofthe state-explosion problem. We therefore propose symbolic algorithms based on binary decisiondiagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easilyimplemented in any BDD-based model-checking tool that checks for reachability in deterministicnon-recursive programs by computing program summaries. We demonstrate the validity of ourapproach by implementing these algorithms in a tool Moped-QLeak, which is built upon Moped,a model checker for Boolean programs. Finally, we show how this symbolic approach extends toprobabilistic programs