eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2014-12-12
505
516
10.4230/LIPIcs.FSTTCS.2014.505
article
Computing Information Flow Using Symbolic Model-Checking
Chadha, Rohit
Mathur, Umang
Schwoon, Stefan
Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret inputs. We consider the problem of computing information leaked by a deterministic or probabilistic program when the measure of information is based on (a) min-entropy and (b) Shannon entropy. The key challenge in computing these measures is that we need the total number of possible outputs and, for each possible output, the number of inputs that lead to it. A direct computation of these quantities is infeasible because of the state-explosion problem. We therefore propose symbolic algorithms based on binary decision diagrams (BDDs). The advantage of our approach is that these symbolic algorithms can be easily implemented in any BDD-based model-checking tool that checks for reachability in deterministic non-recursive programs by computing program summaries. We demonstrate the validity of our approach 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 to probabilistic programs.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol029-fsttcs2014/LIPIcs.FSTTCS.2014.505/LIPIcs.FSTTCS.2014.505.pdf
Information leakage
Min Entropy
Shannon Entropy
Abstract decision diagrams
Program summaries